Theorem peano2nn0 12650

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7421  1c1 11205   + caddc 11207  ℕ₀cn0 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-ltxr 11352  df-nn 12340  df-n0 12611

This theorem is used by:  nn0split  13781  fzonn0p1p1  13883  leexp2r  14321  expnbnd  14380  facdiv  14435  facwordi  14437  faclbnd  14438  faclbnd2  14439  faclbnd3  14440  faclbnd6  14447  bcnp1n  14462  bcp1m1  14468  bcpasc  14469  hashfz  14576  hashf1  14606  hashdifsnp1  14655  fi1uzind  14656  brfi1indALT  14659  pfxccatpfx2  14891  pfxccat3a  14892  swrds2  15097  iseraltlem2  15856  bcxmas  16010  climcndslem1  16024  climcnds  16026  pwdif  16043  geolim  16045  geo2sum  16048  mertenslem1  16059  mertenslem2  16060  mertens  16061  risefacp1  16201  fallfacp1  16202  binomfallfaclem1  16211  binomfallfaclem2  16212  fsumkthpow  16228  efcllem  16249  eftlub  16283  efsep  16284  effsumlt  16285  ruclem9  16412  nn0ob  16560  nn0oddm1d2  16561  pwp1fsum  16567  bitsp1  16607  sadcp1  16631  smuval2  16658  smu01lem  16661  smup1  16665  nn0seqcvgd  16751  algcvg  16757  nonsq  16941  iserodd  17019  pcprendvds  17024  pcpremul  17027  pcdvdsb  17053  4sqlem11  17139  vdwapun  17158  vdwlem1  17165  vdwlem9  17173  ramub1  17212  ramcl  17213  prmop1  17222  sylow1lem3  19820  efgsfo  19959  efgred  19968  telgsums  20213  telgsum  20214  srgbinomlem3  20460  srgbinomlem4  20461  assamulgscmlem2  22214  psdmplcl  22489  psdadd  22490  psdvsca  22491  psdmul  22493  chfacffsupp  23180  chfacfscmulfsupp  23183  chfacfscmulgsum  23184  chfacfpmmulfsupp  23187  chfacfpmmulgsum  23188  cpnord  26261  ply1divex  26461  fta1glem1  26492  fta1glem2  26493  fta1g  26494  plyco0  26516  plyaddlem1  26538  plymullem1  26539  plyco  26566  dvply1  26611  dvply2g  26612  aaliou3lem8  26678  aaliou3lem9  26683  dvtaylp  26703  dvradcnv  26754  pserdvlem2  26761  advlogexp  26989  atantayl3  27273  leibpi  27276  log2cnv  27278  ftalem4  27409  ftalem5  27410  perfectlem1  27562  bcp1ctr  27612  2lgslem3d1  27736  dchrisum0flblem1  27841  ostth2lem2  27967  ostth2lem3  27968  crctcshwlkn0lem7  30411  wwlksnred  30487  wwlksnext  30488  wwlksnextbi  30489  wwlksnredwwlkn  30490  wwlksnredwwlkn0  30491  wwlksnextproplem1  30504  wwlksnextproplem2  30505  wwlksnextproplem3  30506  rusgrnumwwlks  30572  clwwlkf  30644  clwwlknonex2lem2  30705  eupth2lems  30845  eucrct2eupth  30852  numclwlk2lem2f  30984  nndiffz1  33425  nn0diffz0  33433  2exple2exp  33472  gsummoncoe1fz  34177  esplyindfv  34255  vietalem  34258  nn0constr  34440  subfacval2  36039  erdsze2lem1  36055  bccolsum  36597  fwddifnp1  37023  knoppndvlem6  37476  poimirlem17  38649  heiborlem3  38841  heiborlem4  38842  heiborlem6  38844  facp2  43287  sqn5i  43436  sumcubes  43464  2rexfrabdioph  43897  elnn0rabdioph  43904  dvdsrabdioph  43911  jm2.17a  44061  jm2.17b  44062  expdiophlem1  44122  expdiophlem2  44123  hbt  44226  cotrclrcl  44836  k0004ss3  45247  bccp1k  45419  binomcxplemnn0  45427  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnmul  47047  stoweidlem17  47121  wallispilem1  47169  stirlinglem5  47182  etransclem23  47361  etransclem46  47384  etransclem48  47386  fmtnoge3  48709  fmtnorec1  48716  sqrtpwpw2p  48717  fmtnosqrt  48718  fmtnorec2lem  48721  fmtnorec3  48727  fmtnoprmfac1  48744  fmtnoprmfac2lem1  48745  fmtnofac1  48749  flsqrt  48772  perfectALTVlem1  48913  isubgr3stgrlem2  49159  nn0eo  49734  fllog2  49774  dignnld  49809  0dig2nn0o  49819  dignn0ehalf  49823  dignn0flhalf  49824  nn0sumshdiglemA  49825  itcovalsuc  49873  ackvalsuc1mpt  49884  ackval1  49887  ackval2  49888  ackval3  49889  ackendofnn0  49890  ackval0val  49892  ackvalsucsucval  49894  aacllem  51108