| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Zero is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 3155 through peano5 3159 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. |
| Ref | Expression |
|---|---|
| peano1 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | limom 3152 |
. 2
| |
| 2 | 0ellim 3037 |
. 2
| |
| 3 | 1, 2 | ax-mp 7 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: fr0t 3958 nnmcl 4236 nnecl 4237 nnmsucr 4246 1onn 4259 nneob 4261 snfi 4438 snfiOLD 4439 0sdom1dom 4530 infn0 4542 unblem2 4552 unfilem3 4562 unifiOLD 4570 inf0 4615 infeq5 4630 axinf2 4633 dfom3 4639 noinfep 4650 trcl 4655 cardlim 4862 alephgeom 4893 alephfplem4 4910 mulclpi 5033 1lt2pi 5044 om2uzran 6301 uzrdgini 6304 emfin 10466 top2usne 10535 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-ral 1652 df-rex 1653 df-v 1815 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-nul 2284 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-om 3138 |