"S59"(_,_) - successor

Add a Description to S59

Related Assertions

A155: ∀x: ∃y: greater than_S51, (y, x)∧ prime_S52, (y)∧ prime_S52, (+_F53(y, 2))
A156: ∀x: TPC_S49, (x)⇔ A155, (x)
A158: ∀x: TPC_S49, (x)⇒ Independent of ZFC_S54, (x)
A170: ℕ_S58, (1)
A171: ∀x: ℕ_S58, (x)⇒ ℕ_S58, (successor_F59(x))
A177: ∀x: ∀y: successor_S59, (y, x)⇔ y=+_F53(x, 1)
A178: ∀x: successor_S59, (0, x)⇒ ¬ℕ_S58, (x)
A179: ∀x: ∀y: successor_F59(x)=successor_F59(y)⇒ x=y
A182: ∀x: subset_S60, (x, ℕ_F58)∧ member_S61, (1, x)∧ ∀y: member_S61, (y, x)⇒ member_S61, (successor_F59(y), x)
A188: ∀x: ∀y: subset_S60, (x, y)⇔ ∀z: member_S61, (z, x)⇒ member_S61, (z, y)
A190: ∀x: A170, (x)⇒ Peano Axioms_S62, (x)
A210: ℕ_S58, (0)
A218: ∀x: ℕ_S58, (x)⇒ sum of numbers from 1 to x_F67(x)=÷_F68(×_F69(x, successor_F59(x)), 2)

No comments yet.