Theorem nn0p1nn 10842

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

Step	Hyp	Ref	Expression
1		1nn 10554	. 2 |- 1 e. NN
2		nn0nnaddcl 10834	. 2 |- ( ( N e. NN0 /\ 1 e. NN ) -> ( N + 1 ) e. NN )
3	1, 2	mpan2 671	1 |- ( N e. NN0 -> ( N + 1 ) e. NN )

Syntax hints:   -> wi 4   e. wcel 1804  (class class class)co 6281   1c1 9496   + caddc 9498   NNcn 10543   NN0cn0 10802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-om 6686  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-ltxr 9636  df-nn 10544  df-n0 10803

This theorem is referenced by:  elnn0nn  10845  elz2  10888  peano5uzi  10958  fseq1p1m1  11763  fzonn0p1  11874  nn0ennn  12071  expnbnd  12277  faccl  12345  facdiv  12347  facwordi  12349  faclbnd  12350  facubnd  12360  bcm1k  12375  bcp1n  12376  bcp1nk  12377  bcpasc  12381  hashf1  12488  fz1isolem  12492  wrdind  12684  wrd2ind  12685  ccats1swrdeqbi  12705  isercoll  13472  isercoll2  13473  iseralt  13489  bcxmas  13629  climcndslem1  13643  fprodser  13738  efcllem  13795  ruclem7  13951  ruclem8  13952  ruclem9  13953  sadcp1  14087  smupp1  14112  prmfac1  14241  iserodd  14341  pcfac  14400  1arith  14427  4sqlem12  14456  vdwlem11  14491  vdwlem12  14492  vdwlem13  14493  ramub1  14528  ramcl  14529  sylow1lem1  16597  efgsrel  16731  efgsp1  16734  lebnumii  21444  lmnn  21680  vitalilem4  21998  plyco  22616  dgrcolem2  22649  dgrco  22650  advlogexp  23014  cxpmul2  23048  atantayl3  23248  leibpilem2  23250  leibpi  23251  leibpisum  23252  log2cnv  23253  log2tlbnd  23254  log2ublem2  23256  log2ub  23258  birthdaylem2  23260  harmoniclbnd  23316  harmonicbnd4  23318  fsumharmonic  23319  chpp1  23407  chtublem  23464  bcmono  23530  bcp1ctr  23532  chtppilimlem1  23636  rplogsumlem2  23648  rpvmasumlem  23650  dchrisumlema  23651  dchrisumlem1  23652  dchrisum0flblem1  23671  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0lem3  23682  selberg2lem  23713  pntrsumo1  23728  pntrlog2bndlem2  23741  pntrlog2bndlem4  23743  pntrlog2bndlem6a  23745  pntpbnd1  23749  pntpbnd2  23750  pntlemg  23761  pntlemj  23766  pntlemf  23768  qabvle  23788  ostth2lem2  23797  wwlknred  24701  wwlknredwwlkn  24704  wwlknredwwlkn0  24705  eupath2lem3  24957  minvecolem3  25770  minvecolem4  25774  archiabllem1a  27713  signshnz  28526  facgam  28586  subfacval2  28609  erdsze2lem2  28626  cvmliftlem7  28714  fallfacval4  29141  faclimlem1  29144  faclimlem2  29145  faclimlem3  29146  faclim  29147  faclim2  29149  bpolycl  29790  bpolysum  29791  bpolydiflem  29792  fsumkthpow  29794  heiborlem4  30286  heiborlem6  30288  diophin  30682  rexrabdioph  30703  2rexfrabdioph  30705  3rexfrabdioph  30706  4rexfrabdioph  30707  6rexfrabdioph  30708  7rexfrabdioph  30709  elnn0rabdioph  30712  dvdsrabdioph  30719  irrapxlem4  30737  irrapxlem5  30738  2nn0ind  30857  jm2.27a  30923  itgpowd  31158  wallispilem3  31803  stirlinglem5  31814