Description: The successor of any natural number is not zero. One of Peano's five postulates for arithmetic. Proposition 7.30(3) of TakeutiZaring p. 42. (Contributed by NM, 3-Sep-2003) Avoid ax-nul . (Revised by Umit Teoman Dogan, 10-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | peano3 | |- ( A e. _om -> suc A =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sucidg | |- ( A e. _om -> A e. suc A ) |
|
| 2 | 1 | ne0d | |- ( A e. _om -> suc A =/= (/) ) |