Theorem peano2nn0 12458

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  1c1 11045   + caddc 11047  ℕ₀cn0 12418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189  df-nn 12163  df-n0 12419

This theorem is referenced by:  nn0split  13580  fzonn0p1p1  13681  leexp2r  14115  expnbnd  14173  facdiv  14228  facwordi  14230  faclbnd  14231  faclbnd2  14232  faclbnd3  14233  faclbnd6  14240  bcnp1n  14255  bcp1m1  14261  bcpasc  14262  hashfz  14368  hashf1  14398  hashdifsnp1  14447  fi1uzind  14448  brfi1indALT  14451  pfxccatpfx2  14678  pfxccat3a  14679  swrds2  14882  iseraltlem2  15625  bcxmas  15777  climcndslem1  15791  climcnds  15793  pwdif  15810  geolim  15812  geo2sum  15815  mertenslem1  15826  mertenslem2  15827  mertens  15828  risefacp1  15971  fallfacp1  15972  binomfallfaclem1  15981  binomfallfaclem2  15982  fsumkthpow  15998  efcllem  16019  eftlub  16053  efsep  16054  effsumlt  16055  ruclem9  16182  nn0ob  16330  nn0oddm1d2  16331  pwp1fsum  16337  bitsp1  16377  sadcp1  16401  smuval2  16428  smu01lem  16431  smup1  16435  nn0seqcvgd  16516  algcvg  16522  nonsq  16705  iserodd  16782  pcprendvds  16787  pcpremul  16790  pcdvdsb  16816  4sqlem11  16902  vdwapun  16921  vdwlem1  16928  vdwlem9  16936  ramub1  16975  ramcl  16976  prmop1  16985  sylow1lem3  19506  efgsfo  19645  efgred  19654  telgsums  19899  telgsum  19900  srgbinomlem3  20113  srgbinomlem4  20114  assamulgscmlem2  21785  psdmplcl  22025  psdadd  22026  psdvsca  22027  psdmul  22029  chfacffsupp  22719  chfacfscmulfsupp  22722  chfacfscmulgsum  22723  chfacfpmmulfsupp  22726  chfacfpmmulgsum  22727  cpnord  25813  ply1divex  26018  fta1glem1  26049  fta1glem2  26050  fta1g  26051  plyco0  26073  plyaddlem1  26094  plymullem1  26095  plyco  26122  dvply1  26167  dvply2g  26168  dvply2gOLD  26169  aaliou3lem8  26229  aaliou3lem9  26234  dvtaylp  26254  dvradcnv  26306  pserdvlem2  26314  advlogexp  26540  atantayl3  26825  leibpi  26828  log2cnv  26830  ftalem4  26962  ftalem5  26963  perfectlem1  27116  bcp1ctr  27166  2lgslem3d1  27290  dchrisum0flblem1  27395  ostth2lem2  27521  ostth2lem3  27522  crctcshwlkn0lem7  29719  wwlksnred  29795  wwlksnext  29796  wwlksnextbi  29797  wwlksnredwwlkn  29798  wwlksnredwwlkn0  29799  wwlksnextproplem1  29812  wwlksnextproplem2  29813  wwlksnextproplem3  29814  rusgrnumwwlks  29877  clwwlkf  29949  clwwlknonex2lem2  30010  eupth2lems  30140  eucrct2eupth  30147  numclwlk2lem2f  30279  nndiffz1  32682  2exple2exp  32743  nn0constr  33724  subfacval2  35147  erdsze2lem1  35163  bccolsum  35699  fwddifnp1  36126  knoppndvlem6  36478  poimirlem17  37604  heiborlem3  37780  heiborlem4  37781  heiborlem6  37783  facp2  42104  sqn5i  42246  sumcubes  42274  2rexfrabdioph  42757  elnn0rabdioph  42764  dvdsrabdioph  42771  jm2.17a  42922  jm2.17b  42923  expdiophlem1  42983  expdiophlem2  42984  hbt  43092  cotrclrcl  43704  k0004ss3  44115  bccp1k  44303  binomcxplemnn0  44311  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnmul  45914  stoweidlem17  45988  wallispilem1  46036  stirlinglem5  46049  etransclem23  46228  etransclem46  46251  etransclem48  46253  fmtnoge3  47504  fmtnorec1  47511  sqrtpwpw2p  47512  fmtnosqrt  47513  fmtnorec2lem  47516  fmtnorec3  47522  fmtnoprmfac1  47539  fmtnoprmfac2lem1  47540  fmtnofac1  47544  flsqrt  47567  perfectALTVlem1  47695  isubgr3stgrlem2  47939  nn0eo  48490  fllog2  48530  dignnld  48565  0dig2nn0o  48575  dignn0ehalf  48579  dignn0flhalf  48580  nn0sumshdiglemA  48581  itcovalsuc  48629  ackvalsuc1mpt  48640  ackval1  48643  ackval2  48644  ackval3  48645  ackendofnn0  48646  ackval0val  48648  ackvalsucsucval  48650  aacllem  49763