Theorem peano2nn0 12453

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7368  1c1 11039   + caddc 11041  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-nn 12158  df-n0 12414

This theorem is referenced by:  nn0split  13571  fzonn0p1p1  13672  leexp2r  14109  expnbnd  14167  facdiv  14222  facwordi  14224  faclbnd  14225  faclbnd2  14226  faclbnd3  14227  faclbnd6  14234  bcnp1n  14249  bcp1m1  14255  bcpasc  14256  hashfz  14362  hashf1  14392  hashdifsnp1  14441  fi1uzind  14442  brfi1indALT  14445  pfxccatpfx2  14672  pfxccat3a  14673  swrds2  14875  iseraltlem2  15618  bcxmas  15770  climcndslem1  15784  climcnds  15786  pwdif  15803  geolim  15805  geo2sum  15808  mertenslem1  15819  mertenslem2  15820  mertens  15821  risefacp1  15964  fallfacp1  15965  binomfallfaclem1  15974  binomfallfaclem2  15975  fsumkthpow  15991  efcllem  16012  eftlub  16046  efsep  16047  effsumlt  16048  ruclem9  16175  nn0ob  16323  nn0oddm1d2  16324  pwp1fsum  16330  bitsp1  16370  sadcp1  16394  smuval2  16421  smu01lem  16424  smup1  16428  nn0seqcvgd  16509  algcvg  16515  nonsq  16698  iserodd  16775  pcprendvds  16780  pcpremul  16783  pcdvdsb  16809  4sqlem11  16895  vdwapun  16914  vdwlem1  16921  vdwlem9  16929  ramub1  16968  ramcl  16969  prmop1  16978  sylow1lem3  19541  efgsfo  19680  efgred  19689  telgsums  19934  telgsum  19935  srgbinomlem3  20175  srgbinomlem4  20176  assamulgscmlem2  21868  psdmplcl  22117  psdadd  22118  psdvsca  22119  psdmul  22121  chfacffsupp  22812  chfacfscmulfsupp  22815  chfacfscmulgsum  22816  chfacfpmmulfsupp  22819  chfacfpmmulgsum  22820  cpnord  25905  ply1divex  26110  fta1glem1  26141  fta1glem2  26142  fta1g  26143  plyco0  26165  plyaddlem1  26186  plymullem1  26187  plyco  26214  dvply1  26259  dvply2g  26260  dvply2gOLD  26261  aaliou3lem8  26321  aaliou3lem9  26326  dvtaylp  26346  dvradcnv  26398  pserdvlem2  26406  advlogexp  26632  atantayl3  26917  leibpi  26920  log2cnv  26922  ftalem4  27054  ftalem5  27055  perfectlem1  27208  bcp1ctr  27258  2lgslem3d1  27382  dchrisum0flblem1  27487  ostth2lem2  27613  ostth2lem3  27614  crctcshwlkn0lem7  29901  wwlksnred  29977  wwlksnext  29978  wwlksnextbi  29979  wwlksnredwwlkn  29980  wwlksnredwwlkn0  29981  wwlksnextproplem1  29994  wwlksnextproplem2  29995  wwlksnextproplem3  29996  rusgrnumwwlks  30062  clwwlkf  30134  clwwlknonex2lem2  30195  eupth2lems  30325  eucrct2eupth  30332  numclwlk2lem2f  30464  nndiffz1  32877  nn0diffz0  32885  2exple2exp  32937  gsummoncoe1fz  33691  esplyindfv  33753  vietalem  33756  nn0constr  33939  subfacval2  35403  erdsze2lem1  35419  bccolsum  35955  fwddifnp1  36381  knoppndvlem6  36739  poimirlem17  37888  heiborlem3  38064  heiborlem4  38065  heiborlem6  38067  facp2  42513  sqn5i  42655  sumcubes  42683  2rexfrabdioph  43153  elnn0rabdioph  43160  dvdsrabdioph  43167  jm2.17a  43317  jm2.17b  43318  expdiophlem1  43378  expdiophlem2  43379  hbt  43487  cotrclrcl  44098  k0004ss3  44509  bccp1k  44697  binomcxplemnn0  44705  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnmul  46301  stoweidlem17  46375  wallispilem1  46423  stirlinglem5  46436  etransclem23  46615  etransclem46  46638  etransclem48  46640  fmtnoge3  47890  fmtnorec1  47897  sqrtpwpw2p  47898  fmtnosqrt  47899  fmtnorec2lem  47902  fmtnorec3  47908  fmtnoprmfac1  47925  fmtnoprmfac2lem1  47926  fmtnofac1  47930  flsqrt  47953  perfectALTVlem1  48081  isubgr3stgrlem2  48327  nn0eo  48888  fllog2  48928  dignnld  48963  0dig2nn0o  48973  dignn0ehalf  48977  dignn0flhalf  48978  nn0sumshdiglemA  48979  itcovalsuc  49027  ackvalsuc1mpt  49038  ackval1  49041  ackval2  49042  ackval3  49043  ackendofnn0  49044  ackval0val  49046  ackvalsucsucval  49048  aacllem  50160