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

Theorem nn0p1nn 10910
Description: A nonnegative integer plus 1 is a positive integer. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)
Assertion
Ref Expression
nn0p1nn  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )

Proof of Theorem nn0p1nn
StepHypRef Expression
1 1nn 10621 . 2  |-  1  e.  NN
2 nn0nnaddcl 10902 . 2  |-  ( ( N  e.  NN0  /\  1  e.  NN )  ->  ( N  +  1 )  e.  NN )
31, 2mpan2 675 1  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868  (class class class)co 6302   1c1 9541    + caddc 9543   NNcn 10610   NN0cn0 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-om 6704  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9678  df-mnf 9679  df-ltxr 9681  df-nn 10611  df-n0 10871
This theorem is referenced by:  elnn0nn  10913  elz2  10955  peano5uzi  11025  fseq1p1m1  11869  fzonn0p1  11990  nn0ennn  12192  expnbnd  12401  faccl  12469  facdiv  12472  facwordi  12474  faclbnd  12475  facubnd  12485  bcm1k  12500  bcp1n  12501  bcp1nk  12502  bcpasc  12506  hashf1  12618  fz1isolem  12622  wrdind  12824  wrd2ind  12825  ccats1swrdeqbi  12845  isercoll  13719  isercoll2  13720  iseralt  13739  bcxmas  13881  climcndslem1  13895  fprodser  13991  fallfacval4  14084  bpolycl  14093  bpolysum  14094  bpolydiflem  14095  fsumkthpow  14097  efcllem  14120  ruclem7  14276  ruclem8  14277  ruclem9  14278  sadcp1  14417  smupp1  14442  prmfac1  14659  iserodd  14773  pcfac  14832  1arith  14859  4sqlem12  14888  vdwlem11  14929  vdwlem12  14930  vdwlem13  14931  ramub1  14974  ramcl  14975  prmop1  14984  sylow1lem1  17238  efgsrel  17372  efgsp1  17375  lebnumii  21984  lmnn  22220  vitalilem4  22556  plyco  23182  dgrcolem2  23215  dgrco  23216  advlogexp  23587  cxpmul2  23621  atantayl3  23852  leibpilem2  23854  leibpi  23855  leibpisum  23856  log2cnv  23857  log2tlbnd  23858  log2ublem2  23860  log2ub  23862  birthdaylem2  23865  harmoniclbnd  23921  harmonicbnd4  23923  fsumharmonic  23924  facgam  23978  chpp1  24069  chtublem  24126  bcmono  24192  bcp1ctr  24194  chtppilimlem1  24298  rplogsumlem2  24310  rpvmasumlem  24312  dchrisumlema  24313  dchrisumlem1  24314  dchrisum0flblem1  24333  dchrisum0lem1b  24340  dchrisum0lem1  24341  dchrisum0lem3  24344  selberg2lem  24375  pntrsumo1  24390  pntrlog2bndlem2  24403  pntrlog2bndlem4  24405  pntrlog2bndlem6a  24407  pntpbnd1  24411  pntpbnd2  24412  pntlemg  24423  pntlemj  24428  pntlemf  24430  qabvle  24450  ostth2lem2  24459  wwlknred  25437  wwlknredwwlkn  25440  wwlknredwwlkn0  25441  eupath2lem3  25693  minvecolem3  26504  minvecolem4  26508  minvecolem3OLD  26514  minvecolem4OLD  26518  archiabllem1a  28503  lmatfvlem  28637  signshnz  29476  subfacval2  29906  erdsze2lem2  29923  cvmliftlem7  30010  faclimlem1  30374  faclimlem2  30375  faclimlem3  30376  faclim  30377  faclim2  30379  poimirlem3  31857  poimirlem4  31858  poimirlem12  31866  poimirlem15  31869  poimirlem16  31870  poimirlem17  31871  poimirlem19  31873  poimirlem20  31874  poimirlem23  31877  poimirlem24  31878  poimirlem25  31879  poimirlem28  31882  poimirlem29  31883  poimirlem31  31885  heiborlem4  32060  heiborlem6  32062  diophin  35534  rexrabdioph  35556  2rexfrabdioph  35558  3rexfrabdioph  35559  4rexfrabdioph  35560  6rexfrabdioph  35561  7rexfrabdioph  35562  elnn0rabdioph  35565  dvdsrabdioph  35572  irrapxlem4  35589  irrapxlem5  35590  2nn0ind  35713  jm2.27a  35780  itgpowd  36019  bccp1k  36548  binomcxplemrat  36557  binomcxplemfrat  36558  wallispilem3  37749  stirlinglem5  37760  ccats1pfxeqrex  38675  ccats1pfxeqbi  38684  fllog2  39653  blennnelnn  39661  dignn0flhalflem2  39701
  Copyright terms: Public domain W3C validator