Theorem peano2nn0 11333

Description: Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
peano2nn0	|- ( N e. NN0 -> ( N + 1 ) e. NN0 )

Proof of Theorem peano2nn0

Step	Hyp	Ref	Expression
1		1nn0 11308	. 2 |- 1 e. NN0
2		nn0addcl 11328	. 2 |- ( ( N e. NN0 /\ 1 e. NN0 ) -> ( N + 1 ) e. NN0 )
3	1, 2	mpan2 707	1 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1990  (class class class)co 6650   1c1 9937   + caddc 9939   NN0cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079  df-nn 11021  df-n0 11293

This theorem is referenced by:  nn0split  12454  fzonn0p1p1  12546  elfzom1p1elfzo  12547  leexp2r  12918  expnbnd  12993  facdiv  13074  facwordi  13076  faclbnd  13077  faclbnd2  13078  faclbnd3  13079  faclbnd6  13086  bcnp1n  13101  bcp1m1  13107  bcpasc  13108  hashfz  13214  hashf1  13241  brfi1indlem  13278  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrds2  13685  iseraltlem2  14413  bcxmas  14567  climcndslem1  14581  climcnds  14583  geolim  14601  geo2sum  14604  mertenslem1  14616  mertenslem2  14617  mertens  14618  risefacp1  14760  fallfacp1  14761  binomfallfaclem1  14770  binomfallfaclem2  14771  fsumkthpow  14787  efcllem  14808  eftlub  14839  efsep  14840  effsumlt  14841  ruclem9  14967  nn0ob  15100  nn0oddm1d2  15101  pwp1fsum  15114  bitsp1  15153  sadcp1  15177  smuval2  15204  smu01lem  15207  smup1  15211  nn0seqcvgd  15283  algcvg  15289  nonsq  15467  iserodd  15540  pcprendvds  15545  pcpremul  15548  pcdvdsb  15573  4sqlem11  15659  vdwapun  15678  vdwlem1  15685  vdwlem9  15693  ramub1  15732  ramcl  15733  prmop1  15742  decexp2  15779  sylow1lem3  18015  efgsfo  18152  efgred  18161  telgsums  18390  telgsum  18391  srgbinomlem3  18542  srgbinomlem4  18543  assamulgscmlem2  19349  chfacffsupp  20661  chfacfscmulfsupp  20664  chfacfscmulgsum  20665  chfacfpmmulfsupp  20668  chfacfpmmulgsum  20669  cpnord  23698  ply1divex  23896  fta1glem1  23925  fta1glem2  23926  fta1g  23927  plyco0  23948  plyaddlem1  23969  plymullem1  23970  plyco  23997  dvply1  24039  dvply2g  24040  aaliou3lem8  24100  aaliou3lem9  24105  dvtaylp  24124  dvradcnv  24175  pserdvlem2  24182  advlogexp  24401  atantayl3  24666  leibpi  24669  log2cnv  24671  ftalem4  24802  ftalem5  24803  perfectlem1  24954  bcp1ctr  25004  2lgslem3d1  25128  dchrisum0flblem1  25197  ostth2lem2  25323  ostth2lem3  25324  crctcshwlkn0lem7  26708  wwlksnred  26787  wwlksnext  26788  wwlksnextbi  26789  wwlksnredwwlkn  26790  wwlksnredwwlkn0  26791  wwlksnfi  26801  wwlksnextproplem1  26804  wwlksnextproplem2  26805  wwlksnextproplem3  26806  rusgrnumwwlks  26869  clwwlksf  26915  eupth2lems  27098  eucrct2eupth  27105  numclwwlkovf2exlem2  27212  numclwlk2lem2f  27236  nndiffz1  29548  subfacval2  31169  erdsze2lem1  31185  bccolsum  31625  fwddifnp1  32272  knoppndvlem6  32508  poimirlem17  33426  heiborlem3  33612  heiborlem4  33613  heiborlem6  33615  2rexfrabdioph  37360  elnn0rabdioph  37367  dvdsrabdioph  37374  jm2.17a  37527  jm2.17b  37528  expdiophlem1  37588  expdiophlem2  37589  hbt  37700  cotrclrcl  38034  k0004ss3  38451  bccp1k  38540  binomcxplemnn0  38548  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmul  40158  stoweidlem17  40234  wallispilem1  40282  stirlinglem5  40295  etransclem23  40474  etransclem46  40497  etransclem48  40499  pfxccatpfx2  41428  pfxccat3a  41429  fmtnoge3  41442  fmtnorec1  41449  sqrtpwpw2p  41450  fmtnosqrt  41451  fmtnorec2lem  41454  fmtnorec3  41460  fmtnoprmfac1  41477  fmtnoprmfac2lem1  41478  fmtnofac1  41482  pwdif  41501  flsqrt  41508  perfectALTVlem1  41630  nn0eo  42322  fllog2  42362  dignnld  42397  0dig2nn0o  42407  dignn0ehalf  42411  dignn0flhalf  42412  nn0sumshdiglemA  42413  aacllem  42547