MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano2nn0 Structured version   Visualization version   GIF version

Theorem peano2nn0 11929
Description: Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
peano2nn0 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Proof of Theorem peano2nn0
StepHypRef Expression
1 1nn0 11905 . 2 1 ∈ ℕ0
2 nn0addcl 11924 . 2 ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
31, 2mpan2 689 1 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  (class class class)co 7148  1c1 10530   + caddc 10532  0cn0 11889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-om 7573  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672  df-nn 11631  df-n0 11890
This theorem is referenced by:  nn0split  13014  fzonn0p1p1  13108  leexp2r  13530  expnbnd  13585  facdiv  13639  facwordi  13641  faclbnd  13642  faclbnd2  13643  faclbnd3  13644  faclbnd6  13651  bcnp1n  13666  bcp1m1  13672  bcpasc  13673  hashfz  13780  hashf1  13807  hashdifsnp1  13846  fi1uzind  13847  brfi1indALT  13850  pfxccatpfx2  14091  pfxccat3a  14092  swrds2  14294  iseraltlem2  15031  bcxmas  15182  climcndslem1  15196  climcnds  15198  pwdif  15215  geolim  15218  geo2sum  15221  mertenslem1  15232  mertenslem2  15233  mertens  15234  risefacp1  15375  fallfacp1  15376  binomfallfaclem1  15385  binomfallfaclem2  15386  fsumkthpow  15402  efcllem  15423  eftlub  15454  efsep  15455  effsumlt  15456  ruclem9  15583  nn0ob  15727  nn0oddm1d2  15728  pwp1fsum  15734  bitsp1  15772  sadcp1  15796  smuval2  15823  smu01lem  15826  smup1  15830  nn0seqcvgd  15906  algcvg  15912  nonsq  16091  iserodd  16164  pcprendvds  16169  pcpremul  16172  pcdvdsb  16197  4sqlem11  16283  vdwapun  16302  vdwlem1  16309  vdwlem9  16317  ramub1  16356  ramcl  16357  prmop1  16366  decexp2  16403  sylow1lem3  18717  efgsfo  18857  efgred  18866  telgsums  19105  telgsum  19106  srgbinomlem3  19284  srgbinomlem4  19285  assamulgscmlem2  20121  chfacffsupp  21456  chfacfscmulfsupp  21459  chfacfscmulgsum  21460  chfacfpmmulfsupp  21463  chfacfpmmulgsum  21464  cpnord  24524  ply1divex  24722  fta1glem1  24751  fta1glem2  24752  fta1g  24753  plyco0  24774  plyaddlem1  24795  plymullem1  24796  plyco  24823  dvply1  24865  dvply2g  24866  aaliou3lem8  24926  aaliou3lem9  24931  dvtaylp  24950  dvradcnv  25001  pserdvlem2  25008  advlogexp  25230  atantayl3  25509  leibpi  25512  log2cnv  25514  ftalem4  25645  ftalem5  25646  perfectlem1  25797  bcp1ctr  25847  2lgslem3d1  25971  dchrisum0flblem1  26076  ostth2lem2  26202  ostth2lem3  26203  crctcshwlkn0lem7  27586  wwlksnred  27662  wwlksnext  27663  wwlksnextbi  27664  wwlksnredwwlkn  27665  wwlksnredwwlkn0  27666  wwlksnfiOLD  27677  wwlksnextproplem1  27680  wwlksnextproplem2  27681  wwlksnextproplem3  27682  rusgrnumwwlks  27745  clwwlkf  27818  clwwlknonex2lem2  27879  eupth2lems  28009  eucrct2eupth  28016  numclwlk2lem2f  28148  nndiffz1  30501  subfacval2  32422  erdsze2lem1  32438  bccolsum  32959  fwddifnp1  33614  knoppndvlem6  33844  poimirlem17  34896  heiborlem3  35078  heiborlem4  35079  heiborlem6  35081  sqn5i  39156  2rexfrabdioph  39378  elnn0rabdioph  39385  dvdsrabdioph  39392  jm2.17a  39542  jm2.17b  39543  expdiophlem1  39603  expdiophlem2  39604  hbt  39715  cotrclrcl  40072  k0004ss3  40488  bccp1k  40658  binomcxplemnn0  40666  ioodvbdlimc1lem2  42201  ioodvbdlimc2lem  42203  dvnmul  42212  stoweidlem17  42287  wallispilem1  42335  stirlinglem5  42348  etransclem23  42527  etransclem46  42550  etransclem48  42552  fmtnoge3  43677  fmtnorec1  43684  sqrtpwpw2p  43685  fmtnosqrt  43686  fmtnorec2lem  43689  fmtnorec3  43695  fmtnoprmfac1  43712  fmtnoprmfac2lem1  43713  fmtnofac1  43717  flsqrt  43741  perfectALTVlem1  43871  nn0eo  44573  fllog2  44613  dignnld  44648  0dig2nn0o  44658  dignn0ehalf  44662  dignn0flhalf  44663  nn0sumshdiglemA  44664  aacllem  44887
  Copyright terms: Public domain W3C validator