HomeRelated theorems
Unicode version
| Home |
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 3112 through peano5 3116 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 3109 |
. 2
 | |
| 2 | 0ellim 2994 |
. 2
   | |
| 3 | 1, 2 | ax-mp 7 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wcel 1105 c0 2251 wlim 2912 com 3094 |
| This theorem is referenced by: fr0t 3891 nnmcl 4168 nnecl 4169 nnmsucr 4178 1onn 4191 nneob 4193 snfi 4367 0sdom1dom 4456 infn0 4464 unblem2 4470 unfilem3 4478 unifi 4484 inf0 4530 infeq5 4545 axinf2 4548 dfom3 4554 noinfep 4564 trcl 4569 cardlim 4774 alephgeom 4805 alephfplem4 4822 mulclpi 4944 1lt2pi 4955 om2uzran 6188 uzrdgini 6191 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-4 951 ax-5 952 ax-6 953 ax-7 954 ax-gen 955 ax-8 1101 ax-9 1102 ax-10 1103 ax-12 1104 ax-13 1107 ax-14 1108 ax-11 1180 ax-17 1190 ax-16 1194 ax-11o 1202 ax-ext 1436 ax-sep 2671 ax-nul 2678 ax-pow 2710 ax-pr 2747 ax-un 2830 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 773 df-3an 774 df-ex 957 df-sb 1155 df-eu 1359 df-mo 1360 df-clab 1441 df-cleq 1446 df-clel 1449 df-ne 1563 df-ral 1625 df-rex 1626 df-v 1787 df-dif 2020 df-un 2021 df-in 2022 df-ss 2024 df-nul 2252 df-pw 2373 df-sn 2383 df-pr 2384 df-tp 2386 df-op 2387 df-uni 2472 df-br 2588 df-opab 2635 df-tr 2649 df-eprel 2794 df-po 2804 df-so 2814 df-fr 2880 df-we 2897 df-ord 2914 df-on 2915 df-lim 2916 df-suc 2917 df-om 3095 |