Theorem nn0p1nn 12565

Description: A nonnegative integer plus 1 is a positive integer. Strengthening of peano2nn 12278. (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 12277	. 2 ⊢ 1 ∈ ℕ
2		nn0nnaddcl 12557	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ) → (𝑁 + 1) ∈ ℕ)
3	1, 2	mpan2 691	1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  1c1 11156   + caddc 11158  ℕcn 12266  ℕ₀cn0 12526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300  df-nn 12267  df-n0 12527

This theorem is referenced by:  elnn0nn  12568  elz2  12631  peano5uzi  12707  fseq1p1m1  13638  fzonn0p1  13781  nn0ennn  14020  expnbnd  14271  faccl  14322  facdiv  14326  facwordi  14328  faclbnd  14329  facubnd  14339  bcm1k  14354  bcp1n  14355  bcp1nk  14356  bcpasc  14360  hashf1  14496  fz1isolem  14500  ccats1pfxeqrex  14753  wrdind  14760  wrd2ind  14761  ccats1pfxeqbi  14780  isercoll  15704  isercoll2  15705  iseralt  15721  bcxmas  15871  climcndslem1  15885  fprodser  15985  fallfacval4  16079  bpolycl  16088  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  efcllem  16113  ruclem7  16272  ruclem8  16273  ruclem9  16274  sadcp1  16492  smupp1  16517  prmfac1  16757  iserodd  16873  pcfac  16937  1arith  16965  4sqlem12  16994  vdwlem11  17029  vdwlem12  17030  vdwlem13  17031  ramub1  17066  ramcl  17067  prmop1  17076  sylow1lem1  19616  efgsrel  19752  psdcl  22165  psdmul  22170  lebnumii  24998  lmnn  25297  vitalilem4  25646  itgpowd  26091  plyco  26280  dgrcolem2  26314  dgrco  26315  advlogexp  26697  cxpmul2  26731  atantayl3  26982  leibpilem2  26984  leibpi  26985  leibpisum  26986  log2cnv  26987  log2tlbnd  26988  log2ublem2  26990  log2ub  26992  birthdaylem2  26995  harmoniclbnd  27052  harmonicbnd4  27054  fsumharmonic  27055  facgam  27109  chpp1  27198  chtublem  27255  bcmono  27321  bcp1ctr  27323  gausslemma2dlem3  27412  2lgslem1a  27435  chtppilimlem1  27517  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlema  27532  dchrisumlem1  27533  dchrisum0flblem1  27552  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem3  27563  selberg2lem  27594  pntrsumo1  27609  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntrlog2bndlem6a  27626  pntpbnd1  27630  pntpbnd2  27631  pntlemg  27642  pntlemj  27647  pntlemf  27649  qabvle  27669  ostth2lem2  27678  wlkonwlk1l  29681  wwlksnred  29912  wwlksnredwwlkn  29915  wwlksnredwwlkn0  29916  wwlksnwwlksnon  29935  minvecolem3  30895  minvecolem4  30899  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  archiabllem1a  33198  lmatfvlem  33814  signshnz  34606  subfacval2  35192  erdsze2lem2  35209  cvmliftlem7  35296  faclimlem1  35743  faclimlem2  35744  faclimlem3  35745  faclim  35746  faclim2  35748  poimirlem3  37630  poimirlem4  37631  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  heiborlem4  37821  heiborlem6  37823  fz1sump1  42344  sumcubes  42347  diophin  42783  rexrabdioph  42805  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  elnn0rabdioph  42814  dvdsrabdioph  42821  irrapxlem4  42836  irrapxlem5  42837  2nn0ind  42957  jm2.27a  43017  bccp1k  44360  binomcxplemrat  44369  binomcxplemfrat  44370  recnnltrp  45388  rpgtrecnn  45391  wallispilem3  46082  stirlinglem5  46093  vonioolem1  46695  fllog2  48489  blennnelnn  48497  dignn0flhalflem2  48537