Theorem peano2nn0 12514

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7411  1c1 11113   + caddc 11115  ℕ₀cn0 12474

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-ltxr 11255  df-nn 12215  df-n0 12475

This theorem is referenced by:  nn0split  13618  fzonn0p1p1  13713  leexp2r  14141  expnbnd  14197  facdiv  14249  facwordi  14251  faclbnd  14252  faclbnd2  14253  faclbnd3  14254  faclbnd6  14261  bcnp1n  14276  bcp1m1  14282  bcpasc  14283  hashfz  14389  hashf1  14420  hashdifsnp1  14459  fi1uzind  14460  brfi1indALT  14463  pfxccatpfx2  14689  pfxccat3a  14690  swrds2  14893  iseraltlem2  15631  bcxmas  15783  climcndslem1  15797  climcnds  15799  pwdif  15816  geolim  15818  geo2sum  15821  mertenslem1  15832  mertenslem2  15833  mertens  15834  risefacp1  15975  fallfacp1  15976  binomfallfaclem1  15985  binomfallfaclem2  15986  fsumkthpow  16002  efcllem  16023  eftlub  16054  efsep  16055  effsumlt  16056  ruclem9  16183  nn0ob  16329  nn0oddm1d2  16330  pwp1fsum  16336  bitsp1  16374  sadcp1  16398  smuval2  16425  smu01lem  16428  smup1  16432  nn0seqcvgd  16509  algcvg  16515  nonsq  16697  iserodd  16770  pcprendvds  16775  pcpremul  16778  pcdvdsb  16804  4sqlem11  16890  vdwapun  16909  vdwlem1  16916  vdwlem9  16924  ramub1  16963  ramcl  16964  prmop1  16973  decexp2  17010  sylow1lem3  19470  efgsfo  19609  efgred  19618  telgsums  19863  telgsum  19864  srgbinomlem3  20053  srgbinomlem4  20054  assamulgscmlem2  21460  chfacffsupp  22365  chfacfscmulfsupp  22368  chfacfscmulgsum  22369  chfacfpmmulfsupp  22372  chfacfpmmulgsum  22373  cpnord  25459  ply1divex  25661  fta1glem1  25690  fta1glem2  25691  fta1g  25692  plyco0  25713  plyaddlem1  25734  plymullem1  25735  plyco  25762  dvply1  25804  dvply2g  25805  aaliou3lem8  25865  aaliou3lem9  25870  dvtaylp  25889  dvradcnv  25940  pserdvlem2  25947  advlogexp  26170  atantayl3  26451  leibpi  26454  log2cnv  26456  ftalem4  26587  ftalem5  26588  perfectlem1  26739  bcp1ctr  26789  2lgslem3d1  26913  dchrisum0flblem1  27018  ostth2lem2  27144  ostth2lem3  27145  crctcshwlkn0lem7  29108  wwlksnred  29184  wwlksnext  29185  wwlksnextbi  29186  wwlksnredwwlkn  29187  wwlksnredwwlkn0  29188  wwlksnextproplem1  29201  wwlksnextproplem2  29202  wwlksnextproplem3  29203  rusgrnumwwlks  29266  clwwlkf  29338  clwwlknonex2lem2  29399  eupth2lems  29529  eucrct2eupth  29536  numclwlk2lem2f  29668  nndiffz1  32035  subfacval2  34247  erdsze2lem1  34263  bccolsum  34778  fwddifnp1  35206  knoppndvlem6  35479  poimirlem17  36591  heiborlem3  36767  heiborlem4  36768  heiborlem6  36770  facp2  41045  fac2xp3  41106  sqn5i  41279  sumcubes  41293  2rexfrabdioph  41616  elnn0rabdioph  41623  dvdsrabdioph  41630  jm2.17a  41781  jm2.17b  41782  expdiophlem1  41842  expdiophlem2  41843  hbt  41954  cotrclrcl  42575  k0004ss3  42986  bccp1k  43182  binomcxplemnn0  43190  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  dvnmul  44738  stoweidlem17  44812  wallispilem1  44860  stirlinglem5  44873  etransclem23  45052  etransclem46  45075  etransclem48  45077  fmtnoge3  46277  fmtnorec1  46284  sqrtpwpw2p  46285  fmtnosqrt  46286  fmtnorec2lem  46289  fmtnorec3  46295  fmtnoprmfac1  46312  fmtnoprmfac2lem1  46313  fmtnofac1  46317  flsqrt  46340  perfectALTVlem1  46468  nn0eo  47292  fllog2  47332  dignnld  47367  0dig2nn0o  47377  dignn0ehalf  47381  dignn0flhalf  47382  nn0sumshdiglemA  47383  itcovalsuc  47431  ackvalsuc1mpt  47442  ackval1  47445  ackval2  47446  ackval3  47447  ackendofnn0  47448  ackval0val  47450  ackvalsucsucval  47452  aacllem  47926