Theorem peano2nn0 12564

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7431  1c1 11154   + caddc 11156  ℕ₀cn0 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-ltxr 11298  df-nn 12265  df-n0 12525

This theorem is referenced by:  nn0split  13680  fzonn0p1p1  13780  leexp2r  14211  expnbnd  14268  facdiv  14323  facwordi  14325  faclbnd  14326  faclbnd2  14327  faclbnd3  14328  faclbnd6  14335  bcnp1n  14350  bcp1m1  14356  bcpasc  14357  hashfz  14463  hashf1  14493  hashdifsnp1  14542  fi1uzind  14543  brfi1indALT  14546  pfxccatpfx2  14772  pfxccat3a  14773  swrds2  14976  iseraltlem2  15716  bcxmas  15868  climcndslem1  15882  climcnds  15884  pwdif  15901  geolim  15903  geo2sum  15906  mertenslem1  15917  mertenslem2  15918  mertens  15919  risefacp1  16062  fallfacp1  16063  binomfallfaclem1  16072  binomfallfaclem2  16073  fsumkthpow  16089  efcllem  16110  eftlub  16142  efsep  16143  effsumlt  16144  ruclem9  16271  nn0ob  16418  nn0oddm1d2  16419  pwp1fsum  16425  bitsp1  16465  sadcp1  16489  smuval2  16516  smu01lem  16519  smup1  16523  nn0seqcvgd  16604  algcvg  16610  nonsq  16793  iserodd  16869  pcprendvds  16874  pcpremul  16877  pcdvdsb  16903  4sqlem11  16989  vdwapun  17008  vdwlem1  17015  vdwlem9  17023  ramub1  17062  ramcl  17063  prmop1  17072  decexp2  17109  sylow1lem3  19633  efgsfo  19772  efgred  19781  telgsums  20026  telgsum  20027  srgbinomlem3  20246  srgbinomlem4  20247  assamulgscmlem2  21938  psdmplcl  22184  psdadd  22185  psdvsca  22186  psdmul  22188  chfacffsupp  22878  chfacfscmulfsupp  22881  chfacfscmulgsum  22882  chfacfpmmulfsupp  22885  chfacfpmmulgsum  22886  cpnord  25986  ply1divex  26191  fta1glem1  26222  fta1glem2  26223  fta1g  26224  plyco0  26246  plyaddlem1  26267  plymullem1  26268  plyco  26295  dvply1  26340  dvply2g  26341  dvply2gOLD  26342  aaliou3lem8  26402  aaliou3lem9  26407  dvtaylp  26427  dvradcnv  26479  pserdvlem2  26487  advlogexp  26712  atantayl3  26997  leibpi  27000  log2cnv  27002  ftalem4  27134  ftalem5  27135  perfectlem1  27288  bcp1ctr  27338  2lgslem3d1  27462  dchrisum0flblem1  27567  ostth2lem2  27693  ostth2lem3  27694  crctcshwlkn0lem7  29846  wwlksnred  29922  wwlksnext  29923  wwlksnextbi  29924  wwlksnredwwlkn  29925  wwlksnredwwlkn0  29926  wwlksnextproplem1  29939  wwlksnextproplem2  29940  wwlksnextproplem3  29941  rusgrnumwwlks  30004  clwwlkf  30076  clwwlknonex2lem2  30137  eupth2lems  30267  eucrct2eupth  30274  numclwlk2lem2f  30406  nndiffz1  32795  subfacval2  35172  erdsze2lem1  35188  bccolsum  35719  fwddifnp1  36147  knoppndvlem6  36500  poimirlem17  37624  heiborlem3  37800  heiborlem4  37801  heiborlem6  37803  facp2  42125  fac2xp3  42221  sqn5i  42299  sumcubes  42326  2rexfrabdioph  42784  elnn0rabdioph  42791  dvdsrabdioph  42798  jm2.17a  42949  jm2.17b  42950  expdiophlem1  43010  expdiophlem2  43011  hbt  43119  cotrclrcl  43732  k0004ss3  44143  bccp1k  44337  binomcxplemnn0  44345  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  dvnmul  45899  stoweidlem17  45973  wallispilem1  46021  stirlinglem5  46034  etransclem23  46213  etransclem46  46236  etransclem48  46238  fmtnoge3  47455  fmtnorec1  47462  sqrtpwpw2p  47463  fmtnosqrt  47464  fmtnorec2lem  47467  fmtnorec3  47473  fmtnoprmfac1  47490  fmtnoprmfac2lem1  47491  fmtnofac1  47495  flsqrt  47518  perfectALTVlem1  47646  isubgr3stgrlem2  47870  nn0eo  48378  fllog2  48418  dignnld  48453  0dig2nn0o  48463  dignn0ehalf  48467  dignn0flhalf  48468  nn0sumshdiglemA  48469  itcovalsuc  48517  ackvalsuc1mpt  48528  ackval1  48531  ackval2  48532  ackval3  48533  ackendofnn0  48534  ackval0val  48536  ackvalsucsucval  48538  aacllem  49032