Theorem peano2nn0 12443

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7353  1c1 11029   + caddc 11031  ℕ₀cn0 12403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-nn 12148  df-n0 12404

This theorem is referenced by:  nn0split  13565  fzonn0p1p1  13666  leexp2r  14100  expnbnd  14158  facdiv  14213  facwordi  14215  faclbnd  14216  faclbnd2  14217  faclbnd3  14218  faclbnd6  14225  bcnp1n  14240  bcp1m1  14246  bcpasc  14247  hashfz  14353  hashf1  14383  hashdifsnp1  14432  fi1uzind  14433  brfi1indALT  14436  pfxccatpfx2  14662  pfxccat3a  14663  swrds2  14866  iseraltlem2  15609  bcxmas  15761  climcndslem1  15775  climcnds  15777  pwdif  15794  geolim  15796  geo2sum  15799  mertenslem1  15810  mertenslem2  15811  mertens  15812  risefacp1  15955  fallfacp1  15956  binomfallfaclem1  15965  binomfallfaclem2  15966  fsumkthpow  15982  efcllem  16003  eftlub  16037  efsep  16038  effsumlt  16039  ruclem9  16166  nn0ob  16314  nn0oddm1d2  16315  pwp1fsum  16321  bitsp1  16361  sadcp1  16385  smuval2  16412  smu01lem  16415  smup1  16419  nn0seqcvgd  16500  algcvg  16506  nonsq  16689  iserodd  16766  pcprendvds  16771  pcpremul  16774  pcdvdsb  16800  4sqlem11  16886  vdwapun  16905  vdwlem1  16912  vdwlem9  16920  ramub1  16959  ramcl  16960  prmop1  16969  sylow1lem3  19498  efgsfo  19637  efgred  19646  telgsums  19891  telgsum  19892  srgbinomlem3  20132  srgbinomlem4  20133  assamulgscmlem2  21826  psdmplcl  22066  psdadd  22067  psdvsca  22068  psdmul  22070  chfacffsupp  22760  chfacfscmulfsupp  22763  chfacfscmulgsum  22764  chfacfpmmulfsupp  22767  chfacfpmmulgsum  22768  cpnord  25854  ply1divex  26059  fta1glem1  26090  fta1glem2  26091  fta1g  26092  plyco0  26114  plyaddlem1  26135  plymullem1  26136  plyco  26163  dvply1  26208  dvply2g  26209  dvply2gOLD  26210  aaliou3lem8  26270  aaliou3lem9  26275  dvtaylp  26295  dvradcnv  26347  pserdvlem2  26355  advlogexp  26581  atantayl3  26866  leibpi  26869  log2cnv  26871  ftalem4  27003  ftalem5  27004  perfectlem1  27157  bcp1ctr  27207  2lgslem3d1  27331  dchrisum0flblem1  27436  ostth2lem2  27562  ostth2lem3  27563  crctcshwlkn0lem7  29780  wwlksnred  29856  wwlksnext  29857  wwlksnextbi  29858  wwlksnredwwlkn  29859  wwlksnredwwlkn0  29860  wwlksnextproplem1  29873  wwlksnextproplem2  29874  wwlksnextproplem3  29875  rusgrnumwwlks  29938  clwwlkf  30010  clwwlknonex2lem2  30071  eupth2lems  30201  eucrct2eupth  30208  numclwlk2lem2f  30340  nndiffz1  32748  2exple2exp  32809  nn0constr  33747  subfacval2  35179  erdsze2lem1  35195  bccolsum  35731  fwddifnp1  36158  knoppndvlem6  36510  poimirlem17  37636  heiborlem3  37812  heiborlem4  37813  heiborlem6  37815  facp2  42136  sqn5i  42278  sumcubes  42306  2rexfrabdioph  42789  elnn0rabdioph  42796  dvdsrabdioph  42803  jm2.17a  42953  jm2.17b  42954  expdiophlem1  43014  expdiophlem2  43015  hbt  43123  cotrclrcl  43735  k0004ss3  44146  bccp1k  44334  binomcxplemnn0  44342  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  dvnmul  45944  stoweidlem17  46018  wallispilem1  46066  stirlinglem5  46079  etransclem23  46258  etransclem46  46281  etransclem48  46283  fmtnoge3  47534  fmtnorec1  47541  sqrtpwpw2p  47542  fmtnosqrt  47543  fmtnorec2lem  47546  fmtnorec3  47552  fmtnoprmfac1  47569  fmtnoprmfac2lem1  47570  fmtnofac1  47574  flsqrt  47597  perfectALTVlem1  47725  isubgr3stgrlem2  47971  nn0eo  48533  fllog2  48573  dignnld  48608  0dig2nn0o  48618  dignn0ehalf  48622  dignn0flhalf  48623  nn0sumshdiglemA  48624  itcovalsuc  48672  ackvalsuc1mpt  48683  ackval1  48686  ackval2  48687  ackval3  48688  ackendofnn0  48689  ackval0val  48691  ackvalsucsucval  48693  aacllem  49806