Theorem peano2nn0 12593

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  1c1 11185   + caddc 11187  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-nn 12294  df-n0 12554

This theorem is referenced by:  nn0split  13700  fzonn0p1p1  13795  leexp2r  14224  expnbnd  14281  facdiv  14336  facwordi  14338  faclbnd  14339  faclbnd2  14340  faclbnd3  14341  faclbnd6  14348  bcnp1n  14363  bcp1m1  14369  bcpasc  14370  hashfz  14476  hashf1  14506  hashdifsnp1  14555  fi1uzind  14556  brfi1indALT  14559  pfxccatpfx2  14785  pfxccat3a  14786  swrds2  14989  iseraltlem2  15731  bcxmas  15883  climcndslem1  15897  climcnds  15899  pwdif  15916  geolim  15918  geo2sum  15921  mertenslem1  15932  mertenslem2  15933  mertens  15934  risefacp1  16077  fallfacp1  16078  binomfallfaclem1  16087  binomfallfaclem2  16088  fsumkthpow  16104  efcllem  16125  eftlub  16157  efsep  16158  effsumlt  16159  ruclem9  16286  nn0ob  16432  nn0oddm1d2  16433  pwp1fsum  16439  bitsp1  16477  sadcp1  16501  smuval2  16528  smu01lem  16531  smup1  16535  nn0seqcvgd  16617  algcvg  16623  nonsq  16806  iserodd  16882  pcprendvds  16887  pcpremul  16890  pcdvdsb  16916  4sqlem11  17002  vdwapun  17021  vdwlem1  17028  vdwlem9  17036  ramub1  17075  ramcl  17076  prmop1  17085  decexp2  17122  sylow1lem3  19642  efgsfo  19781  efgred  19790  telgsums  20035  telgsum  20036  srgbinomlem3  20255  srgbinomlem4  20256  assamulgscmlem2  21943  psdmplcl  22189  psdadd  22190  psdvsca  22191  psdmul  22193  chfacffsupp  22883  chfacfscmulfsupp  22886  chfacfscmulgsum  22887  chfacfpmmulfsupp  22890  chfacfpmmulgsum  22891  cpnord  25991  ply1divex  26196  fta1glem1  26227  fta1glem2  26228  fta1g  26229  plyco0  26251  plyaddlem1  26272  plymullem1  26273  plyco  26300  dvply1  26343  dvply2g  26344  dvply2gOLD  26345  aaliou3lem8  26405  aaliou3lem9  26410  dvtaylp  26430  dvradcnv  26482  pserdvlem2  26490  advlogexp  26715  atantayl3  27000  leibpi  27003  log2cnv  27005  ftalem4  27137  ftalem5  27138  perfectlem1  27291  bcp1ctr  27341  2lgslem3d1  27465  dchrisum0flblem1  27570  ostth2lem2  27696  ostth2lem3  27697  crctcshwlkn0lem7  29849  wwlksnred  29925  wwlksnext  29926  wwlksnextbi  29927  wwlksnredwwlkn  29928  wwlksnredwwlkn0  29929  wwlksnextproplem1  29942  wwlksnextproplem2  29943  wwlksnextproplem3  29944  rusgrnumwwlks  30007  clwwlkf  30079  clwwlknonex2lem2  30140  eupth2lems  30270  eucrct2eupth  30277  numclwlk2lem2f  30409  nndiffz1  32791  subfacval2  35155  erdsze2lem1  35171  bccolsum  35701  fwddifnp1  36129  knoppndvlem6  36483  poimirlem17  37597  heiborlem3  37773  heiborlem4  37774  heiborlem6  37776  facp2  42100  fac2xp3  42196  sqn5i  42274  sumcubes  42301  2rexfrabdioph  42752  elnn0rabdioph  42759  dvdsrabdioph  42766  jm2.17a  42917  jm2.17b  42918  expdiophlem1  42978  expdiophlem2  42979  hbt  43087  cotrclrcl  43704  k0004ss3  44115  bccp1k  44310  binomcxplemnn0  44318  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  stoweidlem17  45938  wallispilem1  45986  stirlinglem5  45999  etransclem23  46178  etransclem46  46201  etransclem48  46203  fmtnoge3  47404  fmtnorec1  47411  sqrtpwpw2p  47412  fmtnosqrt  47413  fmtnorec2lem  47416  fmtnorec3  47422  fmtnoprmfac1  47439  fmtnoprmfac2lem1  47440  fmtnofac1  47444  flsqrt  47467  perfectALTVlem1  47595  nn0eo  48262  fllog2  48302  dignnld  48337  0dig2nn0o  48347  dignn0ehalf  48351  dignn0flhalf  48352  nn0sumshdiglemA  48353  itcovalsuc  48401  ackvalsuc1mpt  48412  ackval1  48415  ackval2  48416  ackval3  48417  ackendofnn0  48418  ackval0val  48420  ackvalsucsucval  48422  aacllem  48895