Theorem peano2nn0 12468

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  1c1 11030   + caddc 11032  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-nn 12166  df-n0 12429

This theorem is referenced by:  nn0split  13588  fzonn0p1p1  13690  leexp2r  14127  expnbnd  14185  facdiv  14240  facwordi  14242  faclbnd  14243  faclbnd2  14244  faclbnd3  14245  faclbnd6  14252  bcnp1n  14267  bcp1m1  14273  bcpasc  14274  hashfz  14380  hashf1  14410  hashdifsnp1  14459  fi1uzind  14460  brfi1indALT  14463  pfxccatpfx2  14690  pfxccat3a  14691  swrds2  14893  iseraltlem2  15636  bcxmas  15791  climcndslem1  15805  climcnds  15807  pwdif  15824  geolim  15826  geo2sum  15829  mertenslem1  15840  mertenslem2  15841  mertens  15842  risefacp1  15985  fallfacp1  15986  binomfallfaclem1  15995  binomfallfaclem2  15996  fsumkthpow  16012  efcllem  16033  eftlub  16067  efsep  16068  effsumlt  16069  ruclem9  16196  nn0ob  16344  nn0oddm1d2  16345  pwp1fsum  16351  bitsp1  16391  sadcp1  16415  smuval2  16442  smu01lem  16445  smup1  16449  nn0seqcvgd  16530  algcvg  16536  nonsq  16720  iserodd  16797  pcprendvds  16802  pcpremul  16805  pcdvdsb  16831  4sqlem11  16917  vdwapun  16936  vdwlem1  16943  vdwlem9  16951  ramub1  16990  ramcl  16991  prmop1  17000  sylow1lem3  19566  efgsfo  19705  efgred  19714  telgsums  19959  telgsum  19960  srgbinomlem3  20200  srgbinomlem4  20201  assamulgscmlem2  21875  psdmplcl  22150  psdadd  22151  psdvsca  22152  psdmul  22154  chfacffsupp  22839  chfacfscmulfsupp  22842  chfacfscmulgsum  22843  chfacfpmmulfsupp  22846  chfacfpmmulgsum  22847  cpnord  25920  ply1divex  26120  fta1glem1  26151  fta1glem2  26152  fta1g  26153  plyco0  26175  plyaddlem1  26196  plymullem1  26197  plyco  26224  dvply1  26268  dvply2g  26269  aaliou3lem8  26329  aaliou3lem9  26334  dvtaylp  26353  dvradcnv  26404  pserdvlem2  26411  advlogexp  26637  atantayl3  26921  leibpi  26924  log2cnv  26926  ftalem4  27057  ftalem5  27058  perfectlem1  27210  bcp1ctr  27260  2lgslem3d1  27384  dchrisum0flblem1  27489  ostth2lem2  27615  ostth2lem3  27616  crctcshwlkn0lem7  29902  wwlksnred  29978  wwlksnext  29979  wwlksnextbi  29980  wwlksnredwwlkn  29981  wwlksnredwwlkn0  29982  wwlksnextproplem1  29995  wwlksnextproplem2  29996  wwlksnextproplem3  29997  rusgrnumwwlks  30063  clwwlkf  30135  clwwlknonex2lem2  30196  eupth2lems  30326  eucrct2eupth  30333  numclwlk2lem2f  30465  nndiffz1  32878  nn0diffz0  32886  2exple2exp  32937  gsummoncoe1fz  33681  esplyindfv  33760  vietalem  33763  nn0constr  33945  subfacval2  35415  erdsze2lem1  35431  bccolsum  35967  fwddifnp1  36393  knoppndvlem6  36823  poimirlem17  38004  heiborlem3  38180  heiborlem4  38181  heiborlem6  38183  facp2  42628  sqn5i  42762  sumcubes  42790  2rexfrabdioph  43241  elnn0rabdioph  43248  dvdsrabdioph  43255  jm2.17a  43405  jm2.17b  43406  expdiophlem1  43466  expdiophlem2  43467  hbt  43575  cotrclrcl  44186  k0004ss3  44597  bccp1k  44785  binomcxplemnn0  44793  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnmul  46386  stoweidlem17  46460  wallispilem1  46508  stirlinglem5  46521  etransclem23  46700  etransclem46  46723  etransclem48  46725  fmtnoge3  48008  fmtnorec1  48015  sqrtpwpw2p  48016  fmtnosqrt  48017  fmtnorec2lem  48020  fmtnorec3  48026  fmtnoprmfac1  48043  fmtnoprmfac2lem1  48044  fmtnofac1  48048  flsqrt  48071  perfectALTVlem1  48212  isubgr3stgrlem2  48458  nn0eo  49019  fllog2  49059  dignnld  49094  0dig2nn0o  49104  dignn0ehalf  49108  dignn0flhalf  49109  nn0sumshdiglemA  49110  itcovalsuc  49158  ackvalsuc1mpt  49169  ackval1  49172  ackval2  49173  ackval3  49174  ackendofnn0  49175  ackval0val  49177  ackvalsucsucval  49179  aacllem  50291