Theorem peano2nn0 12432

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7355  1c1 11018   + caddc 11020  ℕ₀cn0 12392

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-ltxr 11162  df-nn 12137  df-n0 12393

This theorem is referenced by:  nn0split  13550  fzonn0p1p1  13651  leexp2r  14088  expnbnd  14146  facdiv  14201  facwordi  14203  faclbnd  14204  faclbnd2  14205  faclbnd3  14206  faclbnd6  14213  bcnp1n  14228  bcp1m1  14234  bcpasc  14235  hashfz  14341  hashf1  14371  hashdifsnp1  14420  fi1uzind  14421  brfi1indALT  14424  pfxccatpfx2  14651  pfxccat3a  14652  swrds2  14854  iseraltlem2  15597  bcxmas  15749  climcndslem1  15763  climcnds  15765  pwdif  15782  geolim  15784  geo2sum  15787  mertenslem1  15798  mertenslem2  15799  mertens  15800  risefacp1  15943  fallfacp1  15944  binomfallfaclem1  15953  binomfallfaclem2  15954  fsumkthpow  15970  efcllem  15991  eftlub  16025  efsep  16026  effsumlt  16027  ruclem9  16154  nn0ob  16302  nn0oddm1d2  16303  pwp1fsum  16309  bitsp1  16349  sadcp1  16373  smuval2  16400  smu01lem  16403  smup1  16407  nn0seqcvgd  16488  algcvg  16494  nonsq  16677  iserodd  16754  pcprendvds  16759  pcpremul  16762  pcdvdsb  16788  4sqlem11  16874  vdwapun  16893  vdwlem1  16900  vdwlem9  16908  ramub1  16947  ramcl  16948  prmop1  16957  sylow1lem3  19520  efgsfo  19659  efgred  19668  telgsums  19913  telgsum  19914  srgbinomlem3  20154  srgbinomlem4  20155  assamulgscmlem2  21847  psdmplcl  22096  psdadd  22097  psdvsca  22098  psdmul  22100  chfacffsupp  22791  chfacfscmulfsupp  22794  chfacfscmulgsum  22795  chfacfpmmulfsupp  22798  chfacfpmmulgsum  22799  cpnord  25884  ply1divex  26089  fta1glem1  26120  fta1glem2  26121  fta1g  26122  plyco0  26144  plyaddlem1  26165  plymullem1  26166  plyco  26193  dvply1  26238  dvply2g  26239  dvply2gOLD  26240  aaliou3lem8  26300  aaliou3lem9  26305  dvtaylp  26325  dvradcnv  26377  pserdvlem2  26385  advlogexp  26611  atantayl3  26896  leibpi  26899  log2cnv  26901  ftalem4  27033  ftalem5  27034  perfectlem1  27187  bcp1ctr  27237  2lgslem3d1  27361  dchrisum0flblem1  27466  ostth2lem2  27592  ostth2lem3  27593  crctcshwlkn0lem7  29815  wwlksnred  29891  wwlksnext  29892  wwlksnextbi  29893  wwlksnredwwlkn  29894  wwlksnredwwlkn0  29895  wwlksnextproplem1  29908  wwlksnextproplem2  29909  wwlksnextproplem3  29910  rusgrnumwwlks  29976  clwwlkf  30048  clwwlknonex2lem2  30109  eupth2lems  30239  eucrct2eupth  30246  numclwlk2lem2f  30378  nndiffz1  32794  nn0diffz0  32802  2exple2exp  32854  gsummoncoe1fz  33607  esplyindfv  33660  vietalem  33663  nn0constr  33846  subfacval2  35303  erdsze2lem1  35319  bccolsum  35855  fwddifnp1  36281  knoppndvlem6  36633  poimirlem17  37750  heiborlem3  37926  heiborlem4  37927  heiborlem6  37929  facp2  42309  sqn5i  42455  sumcubes  42483  2rexfrabdioph  42953  elnn0rabdioph  42960  dvdsrabdioph  42967  jm2.17a  43117  jm2.17b  43118  expdiophlem1  43178  expdiophlem2  43179  hbt  43287  cotrclrcl  43899  k0004ss3  44310  bccp1k  44498  binomcxplemnn0  44506  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  dvnmul  46103  stoweidlem17  46177  wallispilem1  46225  stirlinglem5  46238  etransclem23  46417  etransclem46  46440  etransclem48  46442  fmtnoge3  47692  fmtnorec1  47699  sqrtpwpw2p  47700  fmtnosqrt  47701  fmtnorec2lem  47704  fmtnorec3  47710  fmtnoprmfac1  47727  fmtnoprmfac2lem1  47728  fmtnofac1  47732  flsqrt  47755  perfectALTVlem1  47883  isubgr3stgrlem2  48129  nn0eo  48690  fllog2  48730  dignnld  48765  0dig2nn0o  48775  dignn0ehalf  48779  dignn0flhalf  48780  nn0sumshdiglemA  48781  itcovalsuc  48829  ackvalsuc1mpt  48840  ackval1  48843  ackval2  48844  ackval3  48845  ackendofnn0  48846  ackval0val  48848  ackvalsucsucval  48850  aacllem  49962