Theorem peano1 3234

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 3234 through peano5 3238 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity.

Assertion

Ref	Expression
peano1	|- (/) e. om

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		limom 3230	. 2 |- Lim om
2		0ellim 3032	. 2 |- (Lim om -> (/) e. om)
3	1, 2	ax-mp 7	1 |- (/) e. om

Syntax hints:   e. wcel 991  (/)c0 2330  Lim wlim 2973  omcom 3215

This theorem is referenced by:  fr0g 4248  nnmcl 4365  nnecl 4366  nnmsucr 4375  1onn 4388  nneob 4390  snfi 4568  0sdom1dom 4662  infn0 4670  unblem2 4678  unfilem3 4687  unifi 4692  inf0 4742  infeq5 4757  axinf2 4760  dfom3 4767  noinfep 4777  trcl 4782  cardlim 4992  alephgeom 5023  alephfplem4 5040  mulclpi 5166  1lt2pi 5177  om2uzrani 6653  uzrdginii 6657  cardfz 6661  emfin 10732  top2usne 10840

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 995  ax-gen 996  ax-8 997  ax-10 999  ax-11 1000  ax-12 1001  ax-13 1002  ax-14 1003  ax-17 1004  ax-4 1006  ax-5o 1008  ax-6o 1011  ax-9o 1156  ax-10o 1174  ax-16 1244  ax-11o 1252  ax-ext 1498  ax-sep 2773  ax-nul 2780  ax-pow 2813  ax-pr 2851  ax-un 3086

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 779  df-3an 780  df-ex 1014  df-sb 1206  df-eu 1419  df-mo 1420  df-clab 1504  df-cleq 1509  df-clel 1512  df-ne 1628  df-ral 1693  df-rex 1694  df-v 1856  df-dif 2099  df-un 2100  df-in 2101  df-ss 2103  df-nul 2331  df-pw 2454  df-sn 2465  df-pr 2466  df-tp 2468  df-op 2469  df-uni 2565  df-br 2688  df-opab 2736  df-tr 2750  df-eprel 2906  df-po 2914  df-so 2926  df-fr 2944  df-we 2959  df-ord 2975  df-on 2976  df-lim 2977  df-suc 2978  df-om 3216

Copyright terms: Public domain