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

Theorem nn0p1nn 10223
Description: A nonnegative integer plus 1 is a natural number. (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 9975 . 2  |-  1  e.  NN
2 nn0nnaddcl 10216 . 2  |-  ( ( N  e.  NN0  /\  1  e.  NN )  ->  ( N  +  1 )  e.  NN )
31, 2mpan2 653 1  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721  (class class class)co 6048   1c1 8955    + caddc 8957   NNcn 9964   NN0cn0 10185
This theorem is referenced by:  elnn0nn  10226  elz2  10262  peano5uzi  10322  fseq1p1m1  11085  nn0ennn  11281  expnbnd  11471  faccl  11539  facdiv  11541  facwordi  11543  faclbnd  11544  facubnd  11554  bcm1k  11569  bcp1n  11570  bcp1nk  11571  bcpasc  11575  hashf1  11669  fz1isolem  11673  wrdind  11754  isercoll  12424  isercoll2  12425  iseralt  12441  bcxmas  12578  climcndslem1  12592  efcllem  12643  ruclem7  12798  ruclem8  12799  ruclem9  12800  sadcp1  12930  smupp1  12955  prmfac1  13081  iserodd  13172  pcfac  13231  1arith  13258  4sqlem12  13287  vdwlem11  13322  vdwlem12  13323  vdwlem13  13324  ramub1  13359  ramcl  13360  sylow1lem1  15195  efgsrel  15329  efgsp1  15332  lebnumii  18952  lmnn  19177  vitalilem4  19464  plyco  20121  dgrcolem2  20153  dgrco  20154  advlogexp  20507  cxpmul2  20541  atantayl3  20740  leibpilem2  20742  leibpi  20743  leibpisum  20744  log2cnv  20745  log2tlbnd  20746  log2ublem2  20748  log2ub  20750  birthdaylem2  20752  harmoniclbnd  20808  harmonicbnd4  20810  fsumharmonic  20811  chpp1  20899  chtublem  20956  bcmono  21022  bcp1ctr  21024  chtppilimlem1  21128  rplogsumlem2  21140  rpvmasumlem  21142  dchrisumlema  21143  dchrisumlem1  21144  dchrisum0flblem1  21163  dchrisum0lem1b  21170  dchrisum0lem1  21171  dchrisum0lem3  21174  selberg2lem  21205  pntrsumo1  21220  pntrlog2bndlem2  21233  pntrlog2bndlem4  21235  pntrlog2bndlem6a  21237  pntpbnd1  21241  pntpbnd2  21242  pntlemg  21253  pntlemj  21258  pntlemf  21260  qabvle  21280  ostth2lem2  21289  eupath2lem3  21662  minvecolem3  22339  minvecolem4  22343  facgam  24811  subfacval2  24834  erdsze2lem2  24851  cvmliftlem7  24939  fprodser  25236  faclimlem1  25318  faclimlem2  25319  faclimlem3  25320  faclim  25321  faclim2  25323  bpolycl  26010  bpolysum  26011  bpolydiflem  26012  fsumkthpow  26014  heiborlem4  26421  heiborlem6  26423  diophin  26729  rexrabdioph  26752  2rexfrabdioph  26754  3rexfrabdioph  26755  4rexfrabdioph  26756  6rexfrabdioph  26757  7rexfrabdioph  26758  elnn0rabdioph  26761  dvdsrabdioph  26768  irrapxlem4  26786  irrapxlem5  26787  2nn0ind  26906  jm2.27a  26974  wallispilem3  27691  stirlinglem5  27702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-recs 6600  df-rdg 6635  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-pnf 9086  df-mnf 9087  df-ltxr 9089  df-nn 9965  df-n0 10186
  Copyright terms: Public domain W3C validator