Theorem peano2nn0 12540

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7408  1c1 11097   + caddc 11099  ℕ₀cn0 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  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 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-ltxr 11244  df-nn 12230  df-n0 12501

This theorem is referenced by:  nn0split  13667  fzonn0p1p1  13769  leexp2r  14206  expnbnd  14264  facdiv  14319  facwordi  14321  faclbnd  14322  faclbnd2  14323  faclbnd3  14324  faclbnd6  14331  bcnp1n  14346  bcp1m1  14352  bcpasc  14353  hashfz  14460  hashf1  14490  hashdifsnp1  14539  fi1uzind  14540  brfi1indALT  14543  pfxccatpfx2  14770  pfxccat3a  14771  swrds2  14973  iseraltlem2  15730  bcxmas  15885  climcndslem1  15899  climcnds  15901  pwdif  15918  geolim  15920  geo2sum  15923  mertenslem1  15934  mertenslem2  15935  mertens  15936  risefacp1  16079  fallfacp1  16080  binomfallfaclem1  16089  binomfallfaclem2  16090  fsumkthpow  16106  efcllem  16127  eftlub  16161  efsep  16162  effsumlt  16163  ruclem9  16290  nn0ob  16438  nn0oddm1d2  16439  pwp1fsum  16445  bitsp1  16485  sadcp1  16509  smuval2  16536  smu01lem  16539  smup1  16543  nn0seqcvgd  16624  algcvg  16630  nonsq  16814  iserodd  16891  pcprendvds  16896  pcpremul  16899  pcdvdsb  16925  4sqlem11  17011  vdwapun  17030  vdwlem1  17037  vdwlem9  17045  ramub1  17084  ramcl  17085  prmop1  17094  sylow1lem3  19666  efgsfo  19805  efgred  19814  telgsums  20059  telgsum  20060  srgbinomlem3  20306  srgbinomlem4  20307  assamulgscmlem2  22015  psdmplcl  22290  psdadd  22291  psdvsca  22292  psdmul  22294  chfacffsupp  22978  chfacfscmulfsupp  22981  chfacfscmulgsum  22982  chfacfpmmulfsupp  22985  chfacfpmmulgsum  22986  cpnord  26059  ply1divex  26259  fta1glem1  26290  fta1glem2  26291  fta1g  26292  plyco0  26314  plyaddlem1  26335  plymullem1  26336  plyco  26363  dvply1  26410  dvply2g  26411  aaliou3lem8  26471  aaliou3lem9  26476  dvtaylp  26495  dvradcnv  26546  pserdvlem2  26553  advlogexp  26782  atantayl3  27066  leibpi  27069  log2cnv  27071  ftalem4  27202  ftalem5  27203  perfectlem1  27355  bcp1ctr  27405  2lgslem3d1  27529  dchrisum0flblem1  27634  ostth2lem2  27760  ostth2lem3  27761  crctcshwlkn0lem7  30102  wwlksnred  30178  wwlksnext  30179  wwlksnextbi  30180  wwlksnredwwlkn  30181  wwlksnredwwlkn0  30182  wwlksnextproplem1  30195  wwlksnextproplem2  30196  wwlksnextproplem3  30197  rusgrnumwwlks  30263  clwwlkf  30335  clwwlknonex2lem2  30396  eupth2lems  30526  eucrct2eupth  30533  numclwlk2lem2f  30665  nndiffz1  33068  nn0diffz0  33076  2exple2exp  33115  gsummoncoe1fz  33829  esplyindfv  33907  vietalem  33910  nn0constr  34092  subfacval2  35574  erdsze2lem1  35590  bccolsum  36126  fwddifnp1  36552  knoppndvlem6  36991  poimirlem17  38171  heiborlem3  38347  heiborlem4  38348  heiborlem6  38350  facp2  42795  sqn5i  42929  sumcubes  42957  2rexfrabdioph  43408  elnn0rabdioph  43415  dvdsrabdioph  43422  jm2.17a  43572  jm2.17b  43573  expdiophlem1  43633  expdiophlem2  43634  hbt  43742  cotrclrcl  44353  k0004ss3  44764  bccp1k  44936  binomcxplemnn0  44944  ioodvbdlimc1lem2  46531  ioodvbdlimc2lem  46533  dvnmul  46542  stoweidlem17  46616  wallispilem1  46664  stirlinglem5  46677  etransclem23  46856  etransclem46  46879  etransclem48  46881  fmtnoge3  48164  fmtnorec1  48171  sqrtpwpw2p  48172  fmtnosqrt  48173  fmtnorec2lem  48176  fmtnorec3  48182  fmtnoprmfac1  48199  fmtnoprmfac2lem1  48200  fmtnofac1  48204  flsqrt  48227  perfectALTVlem1  48368  isubgr3stgrlem2  48614  nn0eo  49186  fllog2  49226  dignnld  49261  0dig2nn0o  49271  dignn0ehalf  49275  dignn0flhalf  49276  nn0sumshdiglemA  49277  itcovalsuc  49325  ackvalsuc1mpt  49336  ackval1  49339  ackval2  49340  ackval3  49341  ackendofnn0  49342  ackval0val  49344  ackvalsucsucval  49346  aacllem  50457