Theorem peano2nn0 12416

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 12392	. 2 ⊢ 1 ∈ ℕ0
2		nn0addcl 12411	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
3	1, 2	mpan2 691	1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7341  1c1 11002   + caddc 11004  ℕ₀cn0 12376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-ltxr 11146  df-nn 12121  df-n0 12377

This theorem is referenced by:  nn0split  13538  fzonn0p1p1  13639  leexp2r  14076  expnbnd  14134  facdiv  14189  facwordi  14191  faclbnd  14192  faclbnd2  14193  faclbnd3  14194  faclbnd6  14201  bcnp1n  14216  bcp1m1  14222  bcpasc  14223  hashfz  14329  hashf1  14359  hashdifsnp1  14408  fi1uzind  14409  brfi1indALT  14412  pfxccatpfx2  14639  pfxccat3a  14640  swrds2  14842  iseraltlem2  15585  bcxmas  15737  climcndslem1  15751  climcnds  15753  pwdif  15770  geolim  15772  geo2sum  15775  mertenslem1  15786  mertenslem2  15787  mertens  15788  risefacp1  15931  fallfacp1  15932  binomfallfaclem1  15941  binomfallfaclem2  15942  fsumkthpow  15958  efcllem  15979  eftlub  16013  efsep  16014  effsumlt  16015  ruclem9  16142  nn0ob  16290  nn0oddm1d2  16291  pwp1fsum  16297  bitsp1  16337  sadcp1  16361  smuval2  16388  smu01lem  16391  smup1  16395  nn0seqcvgd  16476  algcvg  16482  nonsq  16665  iserodd  16742  pcprendvds  16747  pcpremul  16750  pcdvdsb  16776  4sqlem11  16862  vdwapun  16881  vdwlem1  16888  vdwlem9  16896  ramub1  16935  ramcl  16936  prmop1  16945  sylow1lem3  19507  efgsfo  19646  efgred  19655  telgsums  19900  telgsum  19901  srgbinomlem3  20141  srgbinomlem4  20142  assamulgscmlem2  21832  psdmplcl  22072  psdadd  22073  psdvsca  22074  psdmul  22076  chfacffsupp  22766  chfacfscmulfsupp  22769  chfacfscmulgsum  22770  chfacfpmmulfsupp  22773  chfacfpmmulgsum  22774  cpnord  25859  ply1divex  26064  fta1glem1  26095  fta1glem2  26096  fta1g  26097  plyco0  26119  plyaddlem1  26140  plymullem1  26141  plyco  26168  dvply1  26213  dvply2g  26214  dvply2gOLD  26215  aaliou3lem8  26275  aaliou3lem9  26280  dvtaylp  26300  dvradcnv  26352  pserdvlem2  26360  advlogexp  26586  atantayl3  26871  leibpi  26874  log2cnv  26876  ftalem4  27008  ftalem5  27009  perfectlem1  27162  bcp1ctr  27212  2lgslem3d1  27336  dchrisum0flblem1  27441  ostth2lem2  27567  ostth2lem3  27568  crctcshwlkn0lem7  29789  wwlksnred  29865  wwlksnext  29866  wwlksnextbi  29867  wwlksnredwwlkn  29868  wwlksnredwwlkn0  29869  wwlksnextproplem1  29882  wwlksnextproplem2  29883  wwlksnextproplem3  29884  rusgrnumwwlks  29947  clwwlkf  30019  clwwlknonex2lem2  30080  eupth2lems  30210  eucrct2eupth  30217  numclwlk2lem2f  30349  nndiffz1  32761  2exple2exp  32820  nn0constr  33766  subfacval2  35223  erdsze2lem1  35239  bccolsum  35775  fwddifnp1  36199  knoppndvlem6  36551  poimirlem17  37677  heiborlem3  37853  heiborlem4  37854  heiborlem6  37856  facp2  42176  sqn5i  42318  sumcubes  42346  2rexfrabdioph  42829  elnn0rabdioph  42836  dvdsrabdioph  42843  jm2.17a  42993  jm2.17b  42994  expdiophlem1  43054  expdiophlem2  43055  hbt  43163  cotrclrcl  43775  k0004ss3  44186  bccp1k  44374  binomcxplemnn0  44382  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  dvnmul  45981  stoweidlem17  46055  wallispilem1  46103  stirlinglem5  46116  etransclem23  46295  etransclem46  46318  etransclem48  46320  fmtnoge3  47561  fmtnorec1  47568  sqrtpwpw2p  47569  fmtnosqrt  47570  fmtnorec2lem  47573  fmtnorec3  47579  fmtnoprmfac1  47596  fmtnoprmfac2lem1  47597  fmtnofac1  47601  flsqrt  47624  perfectALTVlem1  47752  isubgr3stgrlem2  47998  nn0eo  48560  fllog2  48600  dignnld  48635  0dig2nn0o  48645  dignn0ehalf  48649  dignn0flhalf  48650  nn0sumshdiglemA  48651  itcovalsuc  48699  ackvalsuc1mpt  48710  ackval1  48713  ackval2  48714  ackval3  48715  ackendofnn0  48716  ackval0val  48718  ackvalsucsucval  48720  aacllem  49833