Theorem peano2nn0 12639

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7418  1c1 11194   + caddc 11196  ℕ₀cn0 12599

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341  df-nn 12329  df-n0 12600

This theorem is used by:  nn0split  13770  fzonn0p1p1  13872  leexp2r  14310  expnbnd  14369  facdiv  14424  facwordi  14426  faclbnd  14427  faclbnd2  14428  faclbnd3  14429  faclbnd6  14436  bcnp1n  14451  bcp1m1  14457  bcpasc  14458  hashfz  14565  hashf1  14595  hashdifsnp1  14644  fi1uzind  14645  brfi1indALT  14648  pfxccatpfx2  14879  pfxccat3a  14880  swrds2  15084  iseraltlem2  15843  bcxmas  15997  climcndslem1  16011  climcnds  16013  pwdif  16030  geolim  16032  geo2sum  16035  mertenslem1  16046  mertenslem2  16047  mertens  16048  risefacp1  16188  fallfacp1  16189  binomfallfaclem1  16198  binomfallfaclem2  16199  fsumkthpow  16215  efcllem  16236  eftlub  16270  efsep  16271  effsumlt  16272  ruclem9  16399  nn0ob  16547  nn0oddm1d2  16548  pwp1fsum  16554  bitsp1  16594  sadcp1  16618  smuval2  16645  smu01lem  16648  smup1  16652  nn0seqcvgd  16738  algcvg  16744  nonsq  16928  iserodd  17006  pcprendvds  17011  pcpremul  17014  pcdvdsb  17040  4sqlem11  17126  vdwapun  17145  vdwlem1  17152  vdwlem9  17160  ramub1  17199  ramcl  17200  prmop1  17209  sylow1lem3  19807  efgsfo  19946  efgred  19955  telgsums  20200  telgsum  20201  srgbinomlem3  20447  srgbinomlem4  20448  assamulgscmlem2  22201  psdmplcl  22476  psdadd  22477  psdvsca  22478  psdmul  22480  chfacffsupp  23167  chfacfscmulfsupp  23170  chfacfscmulgsum  23171  chfacfpmmulfsupp  23174  chfacfpmmulgsum  23175  cpnord  26248  ply1divex  26448  fta1glem1  26479  fta1glem2  26480  fta1g  26481  plyco0  26503  plyaddlem1  26525  plymullem1  26526  plyco  26553  dvply1  26598  dvply2g  26599  aaliou3lem8  26665  aaliou3lem9  26670  dvtaylp  26690  dvradcnv  26741  pserdvlem2  26748  advlogexp  26976  atantayl3  27260  leibpi  27263  log2cnv  27265  ftalem4  27396  ftalem5  27397  perfectlem1  27549  bcp1ctr  27599  2lgslem3d1  27723  dchrisum0flblem1  27828  ostth2lem2  27954  ostth2lem3  27955  crctcshwlkn0lem7  30398  wwlksnred  30474  wwlksnext  30475  wwlksnextbi  30476  wwlksnredwwlkn  30477  wwlksnredwwlkn0  30478  wwlksnextproplem1  30491  wwlksnextproplem2  30492  wwlksnextproplem3  30493  rusgrnumwwlks  30559  clwwlkf  30631  clwwlknonex2lem2  30692  eupth2lems  30832  eucrct2eupth  30839  numclwlk2lem2f  30971  nndiffz1  33371  nn0diffz0  33379  2exple2exp  33418  gsummoncoe1fz  34123  esplyindfv  34201  vietalem  34204  nn0constr  34386  subfacval2  35931  erdsze2lem1  35947  bccolsum  36483  fwddifnp1  36910  knoppndvlem6  37363  poimirlem17  38535  heiborlem3  38727  heiborlem4  38728  heiborlem6  38730  facp2  43173  sqn5i  43322  sumcubes  43350  2rexfrabdioph  43782  elnn0rabdioph  43789  dvdsrabdioph  43796  jm2.17a  43946  jm2.17b  43947  expdiophlem1  44007  expdiophlem2  44008  hbt  44116  cotrclrcl  44727  k0004ss3  45138  bccp1k  45310  binomcxplemnn0  45318  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnmul  46922  stoweidlem17  46996  wallispilem1  47044  stirlinglem5  47057  etransclem23  47236  etransclem46  47259  etransclem48  47261  fmtnoge3  48584  fmtnorec1  48591  sqrtpwpw2p  48592  fmtnosqrt  48593  fmtnorec2lem  48596  fmtnorec3  48602  fmtnoprmfac1  48619  fmtnoprmfac2lem1  48620  fmtnofac1  48624  flsqrt  48647  perfectALTVlem1  48788  isubgr3stgrlem2  49034  nn0eo  49609  fllog2  49649  dignnld  49684  0dig2nn0o  49694  dignn0ehalf  49698  dignn0flhalf  49699  nn0sumshdiglemA  49700  itcovalsuc  49748  ackvalsuc1mpt  49759  ackval1  49762  ackval2  49763  ackval3  49764  ackendofnn0  49765  ackval0val  49767  ackvalsucsucval  49769  aacllem  50908