Theorem peano2nn0 12571

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 12547	. 2 ⊢ 1 ∈ ℕ0
2		nn0addcl 12566	. 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 7414  1c1 11128   + caddc 11130  ℕ₀cn0 12531

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275  df-nn 12261  df-n0 12532

This theorem is used by:  nn0split  13701  fzonn0p1p1  13803  leexp2r  14241  expnbnd  14299  facdiv  14354  facwordi  14356  faclbnd  14357  faclbnd2  14358  faclbnd3  14359  faclbnd6  14366  bcnp1n  14381  bcp1m1  14387  bcpasc  14388  hashfz  14495  hashf1  14525  hashdifsnp1  14574  fi1uzind  14575  brfi1indALT  14578  pfxccatpfx2  14809  pfxccat3a  14810  swrds2  15014  iseraltlem2  15773  bcxmas  15927  climcndslem1  15941  climcnds  15943  pwdif  15960  geolim  15962  geo2sum  15965  mertenslem1  15976  mertenslem2  15977  mertens  15978  risefacp1  16118  fallfacp1  16119  binomfallfaclem1  16128  binomfallfaclem2  16129  fsumkthpow  16145  efcllem  16166  eftlub  16200  efsep  16201  effsumlt  16202  ruclem9  16329  nn0ob  16477  nn0oddm1d2  16478  pwp1fsum  16484  bitsp1  16524  sadcp1  16548  smuval2  16575  smu01lem  16578  smup1  16582  nn0seqcvgd  16663  algcvg  16669  nonsq  16853  iserodd  16930  pcprendvds  16935  pcpremul  16938  pcdvdsb  16964  4sqlem11  17050  vdwapun  17069  vdwlem1  17076  vdwlem9  17084  ramub1  17123  ramcl  17124  prmop1  17133  sylow1lem3  19730  efgsfo  19869  efgred  19878  telgsums  20123  telgsum  20124  srgbinomlem3  20370  srgbinomlem4  20371  assamulgscmlem2  22118  psdmplcl  22393  psdadd  22394  psdvsca  22395  psdmul  22397  chfacffsupp  23084  chfacfscmulfsupp  23087  chfacfscmulgsum  23088  chfacfpmmulfsupp  23091  chfacfpmmulgsum  23092  cpnord  26165  ply1divex  26365  fta1glem1  26396  fta1glem2  26397  fta1g  26398  plyco0  26420  plyaddlem1  26442  plymullem1  26443  plyco  26470  dvply1  26517  dvply2g  26518  aaliou3lem8  26584  aaliou3lem9  26589  dvtaylp  26609  dvradcnv  26660  pserdvlem2  26667  advlogexp  26895  atantayl3  27179  leibpi  27182  log2cnv  27184  ftalem4  27315  ftalem5  27316  perfectlem1  27468  bcp1ctr  27518  2lgslem3d1  27642  dchrisum0flblem1  27747  ostth2lem2  27873  ostth2lem3  27874  crctcshwlkn0lem7  30287  wwlksnred  30363  wwlksnext  30364  wwlksnextbi  30365  wwlksnredwwlkn  30366  wwlksnredwwlkn0  30367  wwlksnextproplem1  30380  wwlksnextproplem2  30381  wwlksnextproplem3  30382  rusgrnumwwlks  30448  clwwlkf  30520  clwwlknonex2lem2  30581  eupth2lems  30721  eucrct2eupth  30728  numclwlk2lem2f  30860  nndiffz1  33260  nn0diffz0  33268  2exple2exp  33307  gsummoncoe1fz  34011  esplyindfv  34089  vietalem  34092  nn0constr  34274  subfacval2  35769  erdsze2lem1  35785  bccolsum  36321  fwddifnp1  36748  knoppndvlem6  37217  poimirlem17  38389  heiborlem3  38566  heiborlem4  38567  heiborlem6  38569  facp2  43012  sqn5i  43163  sumcubes  43191  2rexfrabdioph  43640  elnn0rabdioph  43647  dvdsrabdioph  43654  jm2.17a  43804  jm2.17b  43805  expdiophlem1  43865  expdiophlem2  43866  hbt  43974  cotrclrcl  44585  k0004ss3  44996  bccp1k  45168  binomcxplemnn0  45176  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  dvnmul  46774  stoweidlem17  46848  wallispilem1  46896  stirlinglem5  46909  etransclem23  47088  etransclem46  47111  etransclem48  47113  fmtnoge3  48436  fmtnorec1  48443  sqrtpwpw2p  48444  fmtnosqrt  48445  fmtnorec2lem  48448  fmtnorec3  48454  fmtnoprmfac1  48471  fmtnoprmfac2lem1  48472  fmtnofac1  48476  flsqrt  48499  perfectALTVlem1  48640  isubgr3stgrlem2  48886  nn0eo  49461  fllog2  49501  dignnld  49536  0dig2nn0o  49546  dignn0ehalf  49550  dignn0flhalf  49551  nn0sumshdiglemA  49552  itcovalsuc  49600  ackvalsuc1mpt  49611  ackval1  49614  ackval2  49615  ackval3  49616  ackendofnn0  49617  ackval0val  49619  ackvalsucsucval  49621  aacllem  50775