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

Theorem peano2nn0 10721
Description: Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
peano2nn0  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )

Proof of Theorem peano2nn0
StepHypRef Expression
1 1nn0 10696 . 2  |-  1  e.  NN0
2 nn0addcl 10716 . 2  |-  ( ( N  e.  NN0  /\  1  e.  NN0 )  -> 
( N  +  1 )  e.  NN0 )
31, 2mpan2 671 1  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758  (class class class)co 6190   1c1 9384    + caddc 9386   NN0cn0 10680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-ov 6193  df-om 6577  df-recs 6932  df-rdg 6966  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-ltxr 9524  df-nn 10424  df-n0 10681
This theorem is referenced by:  leexp2r  12022  expnbnd  12094  facdiv  12164  facwordi  12166  faclbnd  12167  faclbnd2  12168  faclbnd3  12169  faclbnd6  12176  bcnp1n  12191  bcp1m1  12197  bcpasc  12198  hashfz  12290  hashf1  12312  brfi1indlem  12320  brfi1uzind  12321  swrds2  12647  iseraltlem2  13262  bcxmas  13400  climcndslem1  13414  climcnds  13416  geolim  13432  geo2sum  13435  mertenslem1  13446  mertenslem2  13447  mertens  13448  efcllem  13465  eftlub  13495  efsep  13496  effsumlt  13497  ruclem9  13622  bitsp1  13729  sadcp1  13753  smuval2  13780  smu01lem  13783  smup1  13787  nn0seqcvgd  13847  algcvg  13853  nonsq  13939  iserodd  14004  pcprendvds  14009  pcpremul  14012  pcdvdsb  14037  4sqlem11  14118  vdwapun  14137  vdwlem1  14144  vdwlem9  14152  ramub1  14191  ramcl  14192  decexp2  14206  sylow1lem3  16203  efgsfo  16340  efgred  16349  srgbinomlem3  16746  srgbinomlem4  16747  cpnord  21525  ply1divex  21724  fta1glem1  21753  fta1glem2  21754  fta1g  21755  plyco0  21776  plyaddlem1  21797  plymullem1  21798  plyco  21825  dvply1  21866  dvply2g  21867  aaliou3lem8  21927  aaliou3lem9  21932  dvtaylp  21951  dvradcnv  22002  pserdvlem2  22009  advlogexp  22216  atantayl3  22450  leibpi  22453  log2cnv  22455  ftalem4  22529  ftalem5  22530  perfectlem1  22684  bcp1ctr  22734  dchrisum0flblem1  22873  ostth2lem2  22999  ostth2lem3  23000  eupap1  23732  eupath2lem3  23735  eupath2  23736  nndiffz1  26209  subfacval2  27209  erdsze2lem1  27225  risefacp1  27666  fallfacp1  27667  binomfallfaclem1  27676  binomfallfaclem2  27677  fsumkthpow  28333  heiborlem3  28850  heiborlem4  28851  heiborlem6  28853  2rexfrabdioph  29272  elnn0rabdioph  29279  dvdsrabdioph  29286  jm2.17a  29441  jm2.17b  29442  expdiophlem1  29508  expdiophlem2  29509  hbt  29624  stoweidlem17  29950  wallispilem1  29998  stirlinglem5  30011  elfzom1p1elfzo  30353  fzonn0p1p1  30354  elfzom1elp1fzo  30356  wwlknred  30493  wwlknext  30494  wwlknextbi  30495  wwlknredwwlkn  30496  wwlknredwwlkn0  30497  wwlknfi  30508  clwwlkf  30594  clwlkfclwwlk1hash  30653  wwlkextproplem2  30699  wwlkextproplem3  30700  rusgranumwlks  30712  extwwlkfablem2  30809  numclwwlkovf2ex  30817  numclwlk2lem2f  30834  nn0split  30875  telescgsum  30955  assamulgscmlem2  30965  chfacffsupp  31310  chfacfscmulfsupp  31313  chfacfscmulgsum  31314  chfacfpmmulfsupp  31317  chfacfpmmulgsum  31318
  Copyright terms: Public domain W3C validator