Theorem peano2nn0 12545

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

Assertion

Ref	Expression
peano2nn0	⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Proof of Theorem peano2nn0

Step	Hyp	Ref	Expression
1		1nn0 12521	. 2 ⊢ 1 ∈ ℕ0
2		nn0addcl 12540	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
3	1, 2	mpan2 689	1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7419  1c1 11141   + caddc 11143  ℕ₀cn0 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-ltxr 11285  df-nn 12246  df-n0 12506

This theorem is referenced by:  nn0split  13651  fzonn0p1p1  13746  leexp2r  14174  expnbnd  14230  facdiv  14282  facwordi  14284  faclbnd  14285  faclbnd2  14286  faclbnd3  14287  faclbnd6  14294  bcnp1n  14309  bcp1m1  14315  bcpasc  14316  hashfz  14422  hashf1  14454  hashdifsnp1  14493  fi1uzind  14494  brfi1indALT  14497  pfxccatpfx2  14723  pfxccat3a  14724  swrds2  14927  iseraltlem2  15665  bcxmas  15817  climcndslem1  15831  climcnds  15833  pwdif  15850  geolim  15852  geo2sum  15855  mertenslem1  15866  mertenslem2  15867  mertens  15868  risefacp1  16009  fallfacp1  16010  binomfallfaclem1  16019  binomfallfaclem2  16020  fsumkthpow  16036  efcllem  16057  eftlub  16089  efsep  16090  effsumlt  16091  ruclem9  16218  nn0ob  16364  nn0oddm1d2  16365  pwp1fsum  16371  bitsp1  16409  sadcp1  16433  smuval2  16460  smu01lem  16463  smup1  16467  nn0seqcvgd  16544  algcvg  16550  nonsq  16734  iserodd  16807  pcprendvds  16812  pcpremul  16815  pcdvdsb  16841  4sqlem11  16927  vdwapun  16946  vdwlem1  16953  vdwlem9  16961  ramub1  17000  ramcl  17001  prmop1  17010  decexp2  17047  sylow1lem3  19567  efgsfo  19706  efgred  19715  telgsums  19960  telgsum  19961  srgbinomlem3  20180  srgbinomlem4  20181  assamulgscmlem2  21850  psdmplcl  22109  psdadd  22110  psdvsca  22111  psdmul  22113  chfacffsupp  22802  chfacfscmulfsupp  22805  chfacfscmulgsum  22806  chfacfpmmulfsupp  22809  chfacfpmmulgsum  22810  cpnord  25909  ply1divex  26117  fta1glem1  26147  fta1glem2  26148  fta1g  26149  plyco0  26171  plyaddlem1  26192  plymullem1  26193  plyco  26220  dvply1  26263  dvply2g  26264  dvply2gOLD  26265  aaliou3lem8  26325  aaliou3lem9  26330  dvtaylp  26350  dvradcnv  26402  pserdvlem2  26410  advlogexp  26634  atantayl3  26916  leibpi  26919  log2cnv  26921  ftalem4  27053  ftalem5  27054  perfectlem1  27207  bcp1ctr  27257  2lgslem3d1  27381  dchrisum0flblem1  27486  ostth2lem2  27612  ostth2lem3  27613  crctcshwlkn0lem7  29699  wwlksnred  29775  wwlksnext  29776  wwlksnextbi  29777  wwlksnredwwlkn  29778  wwlksnredwwlkn0  29779  wwlksnextproplem1  29792  wwlksnextproplem2  29793  wwlksnextproplem3  29794  rusgrnumwwlks  29857  clwwlkf  29929  clwwlknonex2lem2  29990  eupth2lems  30120  eucrct2eupth  30127  numclwlk2lem2f  30259  nndiffz1  32636  subfacval2  34928  erdsze2lem1  34944  bccolsum  35464  fwddifnp1  35892  knoppndvlem6  36123  poimirlem17  37241  heiborlem3  37417  heiborlem4  37418  heiborlem6  37420  facp2  41746  fac2xp3  41825  sqn5i  41994  sumcubes  42008  2rexfrabdioph  42358  elnn0rabdioph  42365  dvdsrabdioph  42372  jm2.17a  42523  jm2.17b  42524  expdiophlem1  42584  expdiophlem2  42585  hbt  42696  cotrclrcl  43314  k0004ss3  43725  bccp1k  43920  binomcxplemnn0  43928  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  dvnmul  45469  stoweidlem17  45543  wallispilem1  45591  stirlinglem5  45604  etransclem23  45783  etransclem46  45806  etransclem48  45808  fmtnoge3  47007  fmtnorec1  47014  sqrtpwpw2p  47015  fmtnosqrt  47016  fmtnorec2lem  47019  fmtnorec3  47025  fmtnoprmfac1  47042  fmtnoprmfac2lem1  47043  fmtnofac1  47047  flsqrt  47070  perfectALTVlem1  47198  nn0eo  47787  fllog2  47827  dignnld  47862  0dig2nn0o  47872  dignn0ehalf  47876  dignn0flhalf  47877  nn0sumshdiglemA  47878  itcovalsuc  47926  ackvalsuc1mpt  47937  ackval1  47940  ackval2  47941  ackval3  47942  ackendofnn0  47943  ackval0val  47945  ackvalsucsucval  47947  aacllem  48420