Theorem peano2nn0 12203

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7255  1c1 10803   + caddc 10805  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-nn 11904  df-n0 12164

This theorem is referenced by:  nn0split  13300  fzonn0p1p1  13394  leexp2r  13820  expnbnd  13875  facdiv  13929  facwordi  13931  faclbnd  13932  faclbnd2  13933  faclbnd3  13934  faclbnd6  13941  bcnp1n  13956  bcp1m1  13962  bcpasc  13963  hashfz  14070  hashf1  14099  hashdifsnp1  14138  fi1uzind  14139  brfi1indALT  14142  pfxccatpfx2  14378  pfxccat3a  14379  swrds2  14581  iseraltlem2  15322  bcxmas  15475  climcndslem1  15489  climcnds  15491  pwdif  15508  geolim  15510  geo2sum  15513  mertenslem1  15524  mertenslem2  15525  mertens  15526  risefacp1  15667  fallfacp1  15668  binomfallfaclem1  15677  binomfallfaclem2  15678  fsumkthpow  15694  efcllem  15715  eftlub  15746  efsep  15747  effsumlt  15748  ruclem9  15875  nn0ob  16021  nn0oddm1d2  16022  pwp1fsum  16028  bitsp1  16066  sadcp1  16090  smuval2  16117  smu01lem  16120  smup1  16124  nn0seqcvgd  16203  algcvg  16209  nonsq  16391  iserodd  16464  pcprendvds  16469  pcpremul  16472  pcdvdsb  16498  4sqlem11  16584  vdwapun  16603  vdwlem1  16610  vdwlem9  16618  ramub1  16657  ramcl  16658  prmop1  16667  decexp2  16704  sylow1lem3  19120  efgsfo  19260  efgred  19269  telgsums  19509  telgsum  19510  srgbinomlem3  19693  srgbinomlem4  19694  assamulgscmlem2  21014  chfacffsupp  21913  chfacfscmulfsupp  21916  chfacfscmulgsum  21917  chfacfpmmulfsupp  21920  chfacfpmmulgsum  21921  cpnord  25004  ply1divex  25206  fta1glem1  25235  fta1glem2  25236  fta1g  25237  plyco0  25258  plyaddlem1  25279  plymullem1  25280  plyco  25307  dvply1  25349  dvply2g  25350  aaliou3lem8  25410  aaliou3lem9  25415  dvtaylp  25434  dvradcnv  25485  pserdvlem2  25492  advlogexp  25715  atantayl3  25994  leibpi  25997  log2cnv  25999  ftalem4  26130  ftalem5  26131  perfectlem1  26282  bcp1ctr  26332  2lgslem3d1  26456  dchrisum0flblem1  26561  ostth2lem2  26687  ostth2lem3  26688  crctcshwlkn0lem7  28082  wwlksnred  28158  wwlksnext  28159  wwlksnextbi  28160  wwlksnredwwlkn  28161  wwlksnredwwlkn0  28162  wwlksnextproplem1  28175  wwlksnextproplem2  28176  wwlksnextproplem3  28177  rusgrnumwwlks  28240  clwwlkf  28312  clwwlknonex2lem2  28373  eupth2lems  28503  eucrct2eupth  28510  numclwlk2lem2f  28642  nndiffz1  31009  subfacval2  33049  erdsze2lem1  33065  bccolsum  33611  fwddifnp1  34394  knoppndvlem6  34624  poimirlem17  35721  heiborlem3  35898  heiborlem4  35899  heiborlem6  35901  facp2  40027  fac2xp3  40088  sqn5i  40234  2rexfrabdioph  40534  elnn0rabdioph  40541  dvdsrabdioph  40548  jm2.17a  40698  jm2.17b  40699  expdiophlem1  40759  expdiophlem2  40760  hbt  40871  cotrclrcl  41239  k0004ss3  41652  bccp1k  41848  binomcxplemnn0  41856  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  stoweidlem17  43448  wallispilem1  43496  stirlinglem5  43509  etransclem23  43688  etransclem46  43711  etransclem48  43713  fmtnoge3  44870  fmtnorec1  44877  sqrtpwpw2p  44878  fmtnosqrt  44879  fmtnorec2lem  44882  fmtnorec3  44888  fmtnoprmfac1  44905  fmtnoprmfac2lem1  44906  fmtnofac1  44910  flsqrt  44933  perfectALTVlem1  45061  nn0eo  45762  fllog2  45802  dignnld  45837  0dig2nn0o  45847  dignn0ehalf  45851  dignn0flhalf  45852  nn0sumshdiglemA  45853  itcovalsuc  45901  ackvalsuc1mpt  45912  ackval1  45915  ackval2  45916  ackval3  45917  ackendofnn0  45918  ackval0val  45920  ackvalsucsucval  45922  aacllem  46391