Theorem nn0p1nn 12202

Description: A nonnegative integer plus 1 is a positive integer. Strengthening of peano2nn 11915. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)

Assertion

Ref	Expression
nn0p1nn	⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)

Proof of Theorem nn0p1nn

Step	Hyp	Ref	Expression
1		1nn 11914	. 2 ⊢ 1 ∈ ℕ
2		nn0nnaddcl 12194	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ) → (𝑁 + 1) ∈ ℕ)
3	1, 2	mpan2 687	1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7255  1c1 10803   + caddc 10805  ℕcn 11903  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-nn 11904  df-n0 12164

This theorem is referenced by:  elnn0nn  12205  elz2  12267  peano5uzi  12339  fseq1p1m1  13259  fzonn0p1  13392  nn0ennn  13627  expnbnd  13875  faccl  13925  facdiv  13929  facwordi  13931  faclbnd  13932  facubnd  13942  bcm1k  13957  bcp1n  13958  bcp1nk  13959  bcpasc  13963  hashf1  14099  fz1isolem  14103  ccats1pfxeqrex  14356  wrdind  14363  wrd2ind  14364  ccats1pfxeqbi  14383  isercoll  15307  isercoll2  15308  iseralt  15324  bcxmas  15475  climcndslem1  15489  fprodser  15587  fallfacval4  15681  bpolycl  15690  bpolysum  15691  bpolydiflem  15692  fsumkthpow  15694  efcllem  15715  ruclem7  15873  ruclem8  15874  ruclem9  15875  sadcp1  16090  smupp1  16115  prmfac1  16354  iserodd  16464  pcfac  16528  1arith  16556  4sqlem12  16585  vdwlem11  16620  vdwlem12  16621  vdwlem13  16622  ramub1  16657  ramcl  16658  prmop1  16667  sylow1lem1  19118  efgsrel  19255  lebnumii  24035  lmnn  24332  vitalilem4  24680  itgpowd  25119  plyco  25307  dgrcolem2  25340  dgrco  25341  advlogexp  25715  cxpmul2  25749  atantayl3  25994  leibpilem2  25996  leibpi  25997  leibpisum  25998  log2cnv  25999  log2tlbnd  26000  log2ublem2  26002  log2ub  26004  birthdaylem2  26007  harmoniclbnd  26063  harmonicbnd4  26065  fsumharmonic  26066  facgam  26120  chpp1  26209  chtublem  26264  bcmono  26330  bcp1ctr  26332  gausslemma2dlem3  26421  2lgslem1a  26444  chtppilimlem1  26526  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlema  26541  dchrisumlem1  26542  dchrisum0flblem1  26561  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem3  26572  selberg2lem  26603  pntrsumo1  26618  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntrlog2bndlem6a  26635  pntpbnd1  26639  pntpbnd2  26640  pntlemg  26651  pntlemj  26656  pntlemf  26658  qabvle  26678  ostth2lem2  26687  wlkonwlk1l  27933  wwlksnred  28158  wwlksnredwwlkn  28161  wwlksnredwwlkn0  28162  wwlksnwwlksnon  28181  minvecolem3  29139  minvecolem4  29143  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  archiabllem1a  31347  lmatfvlem  31667  signshnz  32470  subfacval2  33049  erdsze2lem2  33066  cvmliftlem7  33153  faclimlem1  33615  faclimlem2  33616  faclimlem3  33617  faclim  33618  faclim2  33620  poimirlem3  35707  poimirlem4  35708  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  heiborlem4  35899  heiborlem6  35901  diophin  40510  rexrabdioph  40532  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  elnn0rabdioph  40541  dvdsrabdioph  40548  irrapxlem4  40563  irrapxlem5  40564  2nn0ind  40683  jm2.27a  40743  bccp1k  41848  binomcxplemrat  41857  binomcxplemfrat  41858  recnnltrp  42806  rpgtrecnn  42809  wallispilem3  43498  stirlinglem5  43509  vonioolem1  44108  fllog2  45802  blennnelnn  45810  dignn0flhalflem2  45850