Theorem peano2nn0 12550

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7414  1c1 11139   + caddc 11141  ℕ₀cn0 12510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-pss 3953  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-iun 4975  df-br 5126  df-opab 5188  df-mpt 5208  df-tr 5242  df-id 5560  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6303  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-om 7871  df-2nd 7998  df-frecs 8289  df-wrecs 8320  df-recs 8394  df-rdg 8433  df-er 8728  df-en 8969  df-dom 8970  df-sdom 8971  df-pnf 11280  df-mnf 11281  df-ltxr 11283  df-nn 12250  df-n0 12511

This theorem is referenced by:  nn0split  13666  fzonn0p1p1  13766  leexp2r  14197  expnbnd  14254  facdiv  14309  facwordi  14311  faclbnd  14312  faclbnd2  14313  faclbnd3  14314  faclbnd6  14321  bcnp1n  14336  bcp1m1  14342  bcpasc  14343  hashfz  14449  hashf1  14479  hashdifsnp1  14528  fi1uzind  14529  brfi1indALT  14532  pfxccatpfx2  14758  pfxccat3a  14759  swrds2  14962  iseraltlem2  15702  bcxmas  15854  climcndslem1  15868  climcnds  15870  pwdif  15887  geolim  15889  geo2sum  15892  mertenslem1  15903  mertenslem2  15904  mertens  15905  risefacp1  16048  fallfacp1  16049  binomfallfaclem1  16058  binomfallfaclem2  16059  fsumkthpow  16075  efcllem  16096  eftlub  16128  efsep  16129  effsumlt  16130  ruclem9  16257  nn0ob  16404  nn0oddm1d2  16405  pwp1fsum  16411  bitsp1  16451  sadcp1  16475  smuval2  16502  smu01lem  16505  smup1  16509  nn0seqcvgd  16590  algcvg  16596  nonsq  16779  iserodd  16856  pcprendvds  16861  pcpremul  16864  pcdvdsb  16890  4sqlem11  16976  vdwapun  16995  vdwlem1  17002  vdwlem9  17010  ramub1  17049  ramcl  17050  prmop1  17059  sylow1lem3  19591  efgsfo  19730  efgred  19739  telgsums  19984  telgsum  19985  srgbinomlem3  20198  srgbinomlem4  20199  assamulgscmlem2  21887  psdmplcl  22133  psdadd  22134  psdvsca  22135  psdmul  22137  chfacffsupp  22829  chfacfscmulfsupp  22832  chfacfscmulgsum  22833  chfacfpmmulfsupp  22836  chfacfpmmulgsum  22837  cpnord  25926  ply1divex  26131  fta1glem1  26162  fta1glem2  26163  fta1g  26164  plyco0  26186  plyaddlem1  26207  plymullem1  26208  plyco  26235  dvply1  26280  dvply2g  26281  dvply2gOLD  26282  aaliou3lem8  26342  aaliou3lem9  26347  dvtaylp  26367  dvradcnv  26419  pserdvlem2  26427  advlogexp  26652  atantayl3  26937  leibpi  26940  log2cnv  26942  ftalem4  27074  ftalem5  27075  perfectlem1  27228  bcp1ctr  27278  2lgslem3d1  27402  dchrisum0flblem1  27507  ostth2lem2  27633  ostth2lem3  27634  crctcshwlkn0lem7  29783  wwlksnred  29859  wwlksnext  29860  wwlksnextbi  29861  wwlksnredwwlkn  29862  wwlksnredwwlkn0  29863  wwlksnextproplem1  29876  wwlksnextproplem2  29877  wwlksnextproplem3  29878  rusgrnumwwlks  29941  clwwlkf  30013  clwwlknonex2lem2  30074  eupth2lems  30204  eucrct2eupth  30211  numclwlk2lem2f  30343  nndiffz1  32735  2exple2exp  32781  subfacval2  35133  erdsze2lem1  35149  bccolsum  35680  fwddifnp1  36107  knoppndvlem6  36459  poimirlem17  37585  heiborlem3  37761  heiborlem4  37762  heiborlem6  37764  facp2  42085  fac2xp3  42181  sqn5i  42265  sumcubes  42292  2rexfrabdioph  42752  elnn0rabdioph  42759  dvdsrabdioph  42766  jm2.17a  42917  jm2.17b  42918  expdiophlem1  42978  expdiophlem2  42979  hbt  43087  cotrclrcl  43700  k0004ss3  44111  bccp1k  44305  binomcxplemnn0  44313  ioodvbdlimc1lem2  45892  ioodvbdlimc2lem  45894  dvnmul  45903  stoweidlem17  45977  wallispilem1  46025  stirlinglem5  46038  etransclem23  46217  etransclem46  46240  etransclem48  46242  fmtnoge3  47463  fmtnorec1  47470  sqrtpwpw2p  47471  fmtnosqrt  47472  fmtnorec2lem  47475  fmtnorec3  47481  fmtnoprmfac1  47498  fmtnoprmfac2lem1  47499  fmtnofac1  47503  flsqrt  47526  perfectALTVlem1  47654  isubgr3stgrlem2  47880  nn0eo  48395  fllog2  48435  dignnld  48470  0dig2nn0o  48480  dignn0ehalf  48484  dignn0flhalf  48485  nn0sumshdiglemA  48486  itcovalsuc  48534  ackvalsuc1mpt  48545  ackval1  48548  ackval2  48549  ackval3  48550  ackendofnn0  48551  ackval0val  48553  ackvalsucsucval  48555  aacllem  49316