Theorem peano2nn0 12515

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

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 7391  1c1 11068   + caddc 11070  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-ltxr 11215  df-nn 12205  df-n0 12476

This theorem is referenced by:  nn0split  13642  fzonn0p1p1  13744  leexp2r  14181  expnbnd  14239  facdiv  14294  facwordi  14296  faclbnd  14297  faclbnd2  14298  faclbnd3  14299  faclbnd6  14306  bcnp1n  14321  bcp1m1  14327  bcpasc  14328  hashfz  14434  hashf1  14464  hashdifsnp1  14513  fi1uzind  14514  brfi1indALT  14517  pfxccatpfx2  14744  pfxccat3a  14745  swrds2  14947  iseraltlem2  15701  bcxmas  15856  climcndslem1  15870  climcnds  15872  pwdif  15889  geolim  15891  geo2sum  15894  mertenslem1  15905  mertenslem2  15906  mertens  15907  risefacp1  16050  fallfacp1  16051  binomfallfaclem1  16060  binomfallfaclem2  16061  fsumkthpow  16077  efcllem  16098  eftlub  16132  efsep  16133  effsumlt  16134  ruclem9  16261  nn0ob  16409  nn0oddm1d2  16410  pwp1fsum  16416  bitsp1  16456  sadcp1  16480  smuval2  16507  smu01lem  16510  smup1  16514  nn0seqcvgd  16595  algcvg  16601  nonsq  16785  iserodd  16862  pcprendvds  16867  pcpremul  16870  pcdvdsb  16896  4sqlem11  16982  vdwapun  17001  vdwlem1  17008  vdwlem9  17016  ramub1  17055  ramcl  17056  prmop1  17065  sylow1lem3  19631  efgsfo  19770  efgred  19779  telgsums  20024  telgsum  20025  srgbinomlem3  20265  srgbinomlem4  20266  assamulgscmlem2  21940  psdmplcl  22215  psdadd  22216  psdvsca  22217  psdmul  22219  chfacffsupp  22904  chfacfscmulfsupp  22907  chfacfscmulgsum  22908  chfacfpmmulfsupp  22911  chfacfpmmulgsum  22912  cpnord  25985  ply1divex  26185  fta1glem1  26216  fta1glem2  26217  fta1g  26218  plyco0  26240  plyaddlem1  26261  plymullem1  26262  plyco  26289  dvply1  26336  dvply2g  26337  aaliou3lem8  26397  aaliou3lem9  26402  dvtaylp  26421  dvradcnv  26472  pserdvlem2  26479  advlogexp  26708  atantayl3  26992  leibpi  26995  log2cnv  26997  ftalem4  27128  ftalem5  27129  perfectlem1  27281  bcp1ctr  27331  2lgslem3d1  27455  dchrisum0flblem1  27560  ostth2lem2  27686  ostth2lem3  27687  crctcshwlkn0lem7  29973  wwlksnred  30049  wwlksnext  30050  wwlksnextbi  30051  wwlksnredwwlkn  30052  wwlksnredwwlkn0  30053  wwlksnextproplem1  30066  wwlksnextproplem2  30067  wwlksnextproplem3  30068  rusgrnumwwlks  30134  clwwlkf  30206  clwwlknonex2lem2  30267  eupth2lems  30397  eucrct2eupth  30404  numclwlk2lem2f  30536  nndiffz1  32949  nn0diffz0  32957  2exple2exp  32997  gsummoncoe1fz  33755  esplyindfv  33834  vietalem  33837  nn0constr  34019  subfacval2  35498  erdsze2lem1  35514  bccolsum  36050  fwddifnp1  36476  knoppndvlem6  36916  poimirlem17  38097  heiborlem3  38273  heiborlem4  38274  heiborlem6  38276  facp2  42721  sqn5i  42855  sumcubes  42883  2rexfrabdioph  43334  elnn0rabdioph  43341  dvdsrabdioph  43348  jm2.17a  43498  jm2.17b  43499  expdiophlem1  43559  expdiophlem2  43560  hbt  43668  cotrclrcl  44279  k0004ss3  44690  bccp1k  44878  binomcxplemnn0  44886  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  dvnmul  46478  stoweidlem17  46552  wallispilem1  46600  stirlinglem5  46613  etransclem23  46792  etransclem46  46815  etransclem48  46817  fmtnoge3  48100  fmtnorec1  48107  sqrtpwpw2p  48108  fmtnosqrt  48109  fmtnorec2lem  48112  fmtnorec3  48118  fmtnoprmfac1  48135  fmtnoprmfac2lem1  48136  fmtnofac1  48140  flsqrt  48163  perfectALTVlem1  48304  isubgr3stgrlem2  48550  nn0eo  49111  fllog2  49151  dignnld  49186  0dig2nn0o  49196  dignn0ehalf  49200  dignn0flhalf  49201  nn0sumshdiglemA  49202  itcovalsuc  49250  ackvalsuc1mpt  49261  ackval1  49264  ackval2  49265  ackval3  49266  ackendofnn0  49267  ackval0val  49269  ackvalsucsucval  49271  aacllem  50383