Theorem nn0p1nn 10618

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 10332	. 2 |- 1 e. NN
2		nn0nnaddcl 10610	. 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 1756  (class class class)co 6090   1c1 9282   + caddc 9284   NNcn 10321   NN0cn0 10578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530  ax-un 6371  ax-resscn 9338  ax-1cn 9339  ax-icn 9340  ax-addcl 9341  ax-addrcl 9342  ax-mulcl 9343  ax-mulrcl 9344  ax-mulcom 9345  ax-addass 9346  ax-mulass 9347  ax-distr 9348  ax-i2m1 9349  ax-1ne0 9350  ax-1rid 9351  ax-rnegex 9352  ax-rrecex 9353  ax-cnre 9354  ax-pre-lttri 9355  ax-pre-lttrn 9356  ax-pre-ltadd 9357

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 2973  df-sbc 3186  df-csb 3288  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-pss 3343  df-nul 3637  df-if 3791  df-pw 3861  df-sn 3877  df-pr 3879  df-tp 3881  df-op 3883  df-uni 4091  df-iun 4172  df-br 4292  df-opab 4350  df-mpt 4351  df-tr 4385  df-eprel 4631  df-id 4635  df-po 4640  df-so 4641  df-fr 4678  df-we 4680  df-ord 4721  df-on 4722  df-lim 4723  df-suc 4724  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6093  df-om 6476  df-recs 6831  df-rdg 6865  df-er 7100  df-en 7310  df-dom 7311  df-sdom 7312  df-pnf 9419  df-mnf 9420  df-ltxr 9422  df-nn 10322  df-n0 10579

This theorem is referenced by:  elnn0nn  10621  elz2  10662  peano5uzi  10729  fseq1p1m1  11533  fzonn0p1  11608  nn0ennn  11800  expnbnd  11992  faccl  12060  facdiv  12062  facwordi  12064  faclbnd  12065  facubnd  12075  bcm1k  12090  bcp1n  12091  bcp1nk  12092  bcpasc  12096  hashf1  12209  fz1isolem  12213  wrdind  12370  wrd2ind  12371  ccats1swrdeqbi  12388  isercoll  13144  isercoll2  13145  iseralt  13161  bcxmas  13297  climcndslem1  13311  efcllem  13362  ruclem7  13517  ruclem8  13518  ruclem9  13519  sadcp1  13650  smupp1  13675  prmfac1  13803  iserodd  13901  pcfac  13960  1arith  13987  4sqlem12  14016  vdwlem11  14051  vdwlem12  14052  vdwlem13  14053  ramub1  14088  ramcl  14089  sylow1lem1  16096  efgsrel  16230  efgsp1  16233  lebnumii  20537  lmnn  20773  vitalilem4  21090  plyco  21708  dgrcolem2  21740  dgrco  21741  advlogexp  22099  cxpmul2  22133  atantayl3  22333  leibpilem2  22335  leibpi  22336  leibpisum  22337  log2cnv  22338  log2tlbnd  22339  log2ublem2  22341  log2ub  22343  birthdaylem2  22345  harmoniclbnd  22401  harmonicbnd4  22403  fsumharmonic  22404  chpp1  22492  chtublem  22549  bcmono  22615  bcp1ctr  22617  chtppilimlem1  22721  rplogsumlem2  22733  rpvmasumlem  22735  dchrisumlema  22736  dchrisumlem1  22737  dchrisum0flblem1  22756  dchrisum0lem1b  22763  dchrisum0lem1  22764  dchrisum0lem3  22767  selberg2lem  22798  pntrsumo1  22813  pntrlog2bndlem2  22826  pntrlog2bndlem4  22828  pntrlog2bndlem6a  22830  pntpbnd1  22834  pntpbnd2  22835  pntlemg  22846  pntlemj  22851  pntlemf  22853  qabvle  22873  ostth2lem2  22882  eupath2lem3  23599  minvecolem3  24276  minvecolem4  24280  signshnz  26991  facgam  27051  subfacval2  27074  erdsze2lem2  27091  cvmliftlem7  27179  fprodser  27461  fallfacval4  27545  faclimlem1  27548  faclimlem2  27549  faclimlem3  27550  faclim  27551  faclim2  27553  bpolycl  28194  bpolysum  28195  bpolydiflem  28196  fsumkthpow  28198  heiborlem4  28711  heiborlem6  28713  diophin  29109  rexrabdioph  29130  2rexfrabdioph  29132  3rexfrabdioph  29133  4rexfrabdioph  29134  6rexfrabdioph  29135  7rexfrabdioph  29136  elnn0rabdioph  29139  dvdsrabdioph  29146  irrapxlem4  29164  irrapxlem5  29165  2nn0ind  29284  jm2.27a  29352  itgpowd  29588  wallispilem3  29860  stirlinglem5  29871  wwlknred  30353  wwlknredwwlkn  30356  wwlknredwwlkn0  30357