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

Theorem peano2nn0 11446
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 11421 . 2 1 ∈ ℕ0
2 nn0addcl 11441 . 2 ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
31, 2mpan2 709 1 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2103  (class class class)co 6765  1c1 10050   + caddc 10052  0cn0 11405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-ov 6768  df-om 7183  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-ltxr 10192  df-nn 11134  df-n0 11406
This theorem is referenced by:  nn0split  12569  fzonn0p1p1  12662  elfzom1p1elfzo  12663  leexp2r  13033  expnbnd  13108  facdiv  13189  facwordi  13191  faclbnd  13192  faclbnd2  13193  faclbnd3  13194  faclbnd6  13201  bcnp1n  13216  bcp1m1  13222  bcpasc  13223  hashfz  13327  hashf1  13354  brfi1indlem  13391  fi1uzind  13392  brfi1indALT  13395  swrds2  13806  iseraltlem2  14533  bcxmas  14687  climcndslem1  14701  climcnds  14703  geolim  14721  geo2sum  14724  mertenslem1  14736  mertenslem2  14737  mertens  14738  risefacp1  14880  fallfacp1  14881  binomfallfaclem1  14890  binomfallfaclem2  14891  fsumkthpow  14907  efcllem  14928  eftlub  14959  efsep  14960  effsumlt  14961  ruclem9  15087  nn0ob  15223  nn0oddm1d2  15224  pwp1fsum  15237  bitsp1  15276  sadcp1  15300  smuval2  15327  smu01lem  15330  smup1  15334  nn0seqcvgd  15406  algcvg  15412  nonsq  15590  iserodd  15663  pcprendvds  15668  pcpremul  15671  pcdvdsb  15696  4sqlem11  15782  vdwapun  15801  vdwlem1  15808  vdwlem9  15816  ramub1  15855  ramcl  15856  prmop1  15865  decexp2  15902  sylow1lem3  18136  efgsfo  18273  efgred  18282  telgsums  18511  telgsum  18512  srgbinomlem3  18663  srgbinomlem4  18664  assamulgscmlem2  19472  chfacffsupp  20784  chfacfscmulfsupp  20787  chfacfscmulgsum  20788  chfacfpmmulfsupp  20791  chfacfpmmulgsum  20792  cpnord  23818  ply1divex  24016  fta1glem1  24045  fta1glem2  24046  fta1g  24047  plyco0  24068  plyaddlem1  24089  plymullem1  24090  plyco  24117  dvply1  24159  dvply2g  24160  aaliou3lem8  24220  aaliou3lem9  24225  dvtaylp  24244  dvradcnv  24295  pserdvlem2  24302  advlogexp  24521  atantayl3  24786  leibpi  24789  log2cnv  24791  ftalem4  24922  ftalem5  24923  perfectlem1  25074  bcp1ctr  25124  2lgslem3d1  25248  dchrisum0flblem1  25317  ostth2lem2  25443  ostth2lem3  25444  crctcshwlkn0lem7  26840  wwlksnred  26931  wwlksnext  26932  wwlksnextbi  26933  wwlksnredwwlkn  26934  wwlksnredwwlkn0  26935  wwlksnfi  26945  wwlksnextproplem1  26948  wwlksnextproplem2  26949  wwlksnextproplem3  26950  rusgrnumwwlks  27017  clwwlkf  27097  clwwlknonex2lem2  27178  eupth2lems  27311  eucrct2eupth  27318  numclwlk2lem2f  27459  numclwlk2lem2fOLD  27466  nndiffz1  29778  subfacval2  31397  erdsze2lem1  31413  bccolsum  31853  fwddifnp1  32499  knoppndvlem6  32735  poimirlem17  33658  heiborlem3  33844  heiborlem4  33845  heiborlem6  33847  2rexfrabdioph  37779  elnn0rabdioph  37786  dvdsrabdioph  37793  jm2.17a  37946  jm2.17b  37947  expdiophlem1  38007  expdiophlem2  38008  hbt  38119  cotrclrcl  38453  k0004ss3  38870  bccp1k  38959  binomcxplemnn0  38967  ioodvbdlimc1lem2  40567  ioodvbdlimc2lem  40569  dvnmul  40578  stoweidlem17  40654  wallispilem1  40702  stirlinglem5  40715  etransclem23  40894  etransclem46  40917  etransclem48  40919  pfxccatpfx2  41855  pfxccat3a  41856  fmtnoge3  41869  fmtnorec1  41876  sqrtpwpw2p  41877  fmtnosqrt  41878  fmtnorec2lem  41881  fmtnorec3  41887  fmtnoprmfac1  41904  fmtnoprmfac2lem1  41905  fmtnofac1  41909  pwdif  41928  flsqrt  41935  perfectALTVlem1  42057  nn0eo  42749  fllog2  42789  dignnld  42824  0dig2nn0o  42834  dignn0ehalf  42838  dignn0flhalf  42839  nn0sumshdiglemA  42840  aacllem  42977
  Copyright terms: Public domain W3C validator