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

Theorem peano2nn0 11177
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 11152 . 2 1 ∈ ℕ0
2 nn0addcl 11172 . 2 ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
31, 2mpan2 702 1 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6524  1c1 9790   + caddc 9792  0cn0 11136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-ov 6527  df-om 6932  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-er 7603  df-en 7816  df-dom 7817  df-sdom 7818  df-pnf 9929  df-mnf 9930  df-ltxr 9932  df-nn 10865  df-n0 11137
This theorem is referenced by:  nn0split  12275  fzonn0p1p1  12365  elfzom1p1elfzo  12366  leexp2r  12732  expnbnd  12807  facdiv  12888  facwordi  12890  faclbnd  12891  faclbnd2  12892  faclbnd3  12893  faclbnd6  12900  bcnp1n  12915  bcp1m1  12921  bcpasc  12922  hashfz  13023  hashf1  13047  brfi1indlem  13076  fi1uzind  13077  brfi1indALT  13080  fi1uzindOLD  13083  brfi1indALTOLD  13086  swrds2  13476  iseraltlem2  14204  bcxmas  14349  climcndslem1  14363  climcnds  14365  geolim  14383  geo2sum  14386  mertenslem1  14398  mertenslem2  14399  mertens  14400  risefacp1  14542  fallfacp1  14543  binomfallfaclem1  14552  binomfallfaclem2  14553  fsumkthpow  14569  efcllem  14590  eftlub  14621  efsep  14622  effsumlt  14623  ruclem9  14749  nn0ob  14881  nn0oddm1d2  14882  pwp1fsum  14895  bitsp1  14934  sadcp1  14958  smuval2  14985  smu01lem  14988  smup1  14992  nn0seqcvgd  15064  algcvg  15070  nonsq  15248  iserodd  15321  pcprendvds  15326  pcpremul  15329  pcdvdsb  15354  4sqlem11  15440  vdwapun  15459  vdwlem1  15466  vdwlem9  15474  ramub1  15513  ramcl  15514  prmop1  15523  decexp2  15560  sylow1lem3  17781  efgsfo  17918  efgred  17927  telgsums  18156  telgsum  18157  srgbinomlem3  18308  srgbinomlem4  18309  assamulgscmlem2  19113  chfacffsupp  20419  chfacfscmulfsupp  20422  chfacfscmulgsum  20423  chfacfpmmulfsupp  20426  chfacfpmmulgsum  20427  cpnord  23418  ply1divex  23614  fta1glem1  23643  fta1glem2  23644  fta1g  23645  plyco0  23666  plyaddlem1  23687  plymullem1  23688  plyco  23715  dvply1  23757  dvply2g  23758  aaliou3lem8  23818  aaliou3lem9  23823  dvtaylp  23842  dvradcnv  23893  pserdvlem2  23900  advlogexp  24115  atantayl3  24380  leibpi  24383  log2cnv  24385  ftalem4  24516  ftalem5  24517  perfectlem1  24668  bcp1ctr  24718  2lgslem3d1  24842  dchrisum0flblem1  24911  ostth2lem2  25037  ostth2lem3  25038  wwlknred  26014  wwlknext  26015  wwlknextbi  26016  wwlknredwwlkn  26017  wwlknredwwlkn0  26018  wwlknfi  26029  wwlkextproplem2  26033  wwlkextproplem3  26034  clwwlkf  26085  clwlkfclwwlk1hash  26132  rusgranumwlks  26246  eupap1  26266  eupath2lem3  26269  eupath2  26270  extwwlkfablem2  26368  numclwwlkovf2ex  26376  numclwlk2lem2f  26393  nndiffz1  28739  subfacval2  30226  erdsze2lem1  30242  bccolsum  30681  fwddifnp1  31245  knoppndvlem6  31481  poimirlem17  32396  heiborlem3  32582  heiborlem4  32583  heiborlem6  32585  2rexfrabdioph  36178  elnn0rabdioph  36185  dvdsrabdioph  36192  jm2.17a  36345  jm2.17b  36346  expdiophlem1  36406  expdiophlem2  36407  hbt  36519  cotrclrcl  36853  k0004ss3  37271  bccp1k  37362  binomcxplemnn0  37370  ioodvbdlimc1lem2  38623  ioodvbdlimc2lem  38625  dvnmul  38634  stoweidlem17  38711  wallispilem1  38759  stirlinglem5  38772  etransclem23  38951  etransclem46  38974  etransclem48  38976  fmtnoge3  39782  fmtnorec1  39789  sqrtpwpw2p  39790  fmtnosqrt  39791  fmtnorec2lem  39794  fmtnorec3  39800  fmtnoprmfac1  39817  fmtnoprmfac2lem1  39818  fmtnofac1  39822  pwdif  39841  flsqrt  39848  perfectALTVlem1  39966  pfxccatpfx2  40093  pfxccat3a  40094  crctcsh1wlkn0lem7  41018  wwlksnred  41097  wwlksnext  41098  wwlksnextbi  41099  wwlksnredwwlkn  41100  wwlksnredwwlkn0  41101  wwlksnfi  41111  wwlksnextproplem1  41114  wwlksnextproplem2  41115  wwlksnextproplem3  41116  rusgrnumwwlks  41176  clwwlksf  41221  eupth2lems  41405  eucrct2eupth  41412  av-numclwwlkovf2ex  41516  av-numclwlk2lem2f  41532  nn0eo  42115  fllog2  42159  dignnld  42194  0dig2nn0o  42204  dignn0ehalf  42208  dignn0flhalf  42209  nn0sumshdiglemA  42210  aacllem  42316
  Copyright terms: Public domain W3C validator