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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | peano3 | |- ( A e. _om -> suc A =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nsuceq0 | |- suc A =/= (/) |
|
| 2 | 1 | a1i | |- ( A e. _om -> suc A =/= (/) ) |