Theorem nn0p1nn 12600

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7409  1c1 11158   + caddc 11160  ℕcn 12290  ℕ₀cn0 12561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-resscn 11214  ax-1cn 11215  ax-icn 11216  ax-addcl 11217  ax-addrcl 11218  ax-mulcl 11219  ax-mulrcl 11220  ax-mulcom 11221  ax-addass 11222  ax-mulass 11223  ax-distr 11224  ax-i2m1 11225  ax-1ne0 11226  ax-1rid 11227  ax-rnegex 11228  ax-rrecex 11229  ax-cnre 11230  ax-pre-lttri 11231  ax-pre-lttrn 11232  ax-pre-ltadd 11233

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6294  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-om 7862  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-ltxr 11305  df-nn 12291  df-n0 12562

This theorem is used by:  elnn0nn  12603  elz2  12666  peano5uzi  12743  fseq1p1m1  13686  fzonn0p1  13831  nn0ennn  14076  expnbnd  14329  faccl  14380  facdiv  14384  facwordi  14386  faclbnd  14387  facubnd  14397  bcm1k  14412  bcp1n  14413  bcp1nk  14414  bcpasc  14418  hashf1  14555  fz1isolem  14559  ccats1pfxeqrex  14817  wrdind  14824  wrd2ind  14825  ccats1pfxeqbi  14844  isercoll  15788  isercoll2  15789  iseralt  15805  bcxmas  15957  climcndslem1  15971  fprodser  16069  fallfacval4  16162  bpolycl  16171  bpolysum  16172  bpolydiflem  16173  fsumkthpow  16175  efcllem  16196  ruclem7  16357  ruclem8  16358  ruclem9  16359  sadcp1  16578  smupp1  16603  prmfac1  16844  iserodd  16960  pcfac  17024  1arith  17052  4sqlem12  17081  vdwlem11  17116  vdwlem12  17117  vdwlem13  17118  ramub1  17153  ramcl  17154  prmop1  17163  sylow1lem1  19759  efgsrel  19895  psdcl  22429  psdmul  22434  lebnumii  25234  lmnn  25531  vitalilem4  25879  itgpowd  26317  plyco  26507  dgrcolem2  26540  dgrco  26541  advlogexp  26932  cxpmul2  26966  atantayl3  27216  leibpilem2  27218  leibpi  27219  leibpisum  27220  log2cnv  27221  log2tlbnd  27222  log2ublem2  27224  log2ub  27226  birthdaylem2  27229  harmoniclbnd  27285  harmonicbnd4  27287  fsumharmonic  27288  facgam  27342  chpp1  27431  chtublem  27487  bcmono  27553  bcp1ctr  27555  gausslemma2dlem3  27644  2lgslem1a  27667  chtppilimlem1  27749  rplogsumlem2  27761  rpvmasumlem  27763  dchrisumlema  27764  dchrisumlem1  27765  dchrisum0flblem1  27784  dchrisum0lem1b  27791  dchrisum0lem1  27792  dchrisum0lem3  27795  selberg2lem  27826  pntrsumo1  27841  pntrlog2bndlem2  27854  pntrlog2bndlem4  27856  pntrlog2bndlem6a  27858  pntpbnd1  27862  pntpbnd2  27863  pntlemg  27874  pntlemj  27879  pntlemf  27881  qabvle  27901  ostth2lem2  27910  wlkonwlk1l  30161  wwlksnred  30400  wwlksnredwwlkn  30403  wwlksnredwwlkn0  30404  wwlksnwwlksnon  30423  minvecolem3  31397  minvecolem4  31401  cycpmco2lem4  33609  cycpmco2lem5  33610  cycpmco2lem6  33611  cycpmco2lem7  33612  archiabllem1a  33671  lmatfvlem  34366  signshnz  35140  subfacval2  35867  erdsze2lem2  35884  cvmliftlem7  35971  faclimlem1  36423  faclimlem2  36424  faclimlem3  36425  faclim  36426  faclim2  36428  poimirlem3  38455  poimirlem4  38456  poimirlem12  38464  poimirlem15  38467  poimirlem16  38468  poimirlem17  38469  poimirlem19  38471  poimirlem20  38472  poimirlem23  38475  poimirlem24  38476  poimirlem25  38477  poimirlem28  38480  poimirlem29  38481  poimirlem31  38483  heiborlem4  38662  heiborlem6  38664  fz1sump1  43283  sumcubes  43286  diophin  43715  rexrabdioph  43733  2rexfrabdioph  43735  3rexfrabdioph  43736  4rexfrabdioph  43737  6rexfrabdioph  43738  7rexfrabdioph  43739  elnn0rabdioph  43742  dvdsrabdioph  43749  irrapxlem4  43764  irrapxlem5  43765  2nn0ind  43884  jm2.27a  43944  bccp1k  45263  binomcxplemrat  45272  binomcxplemfrat  45273  recnnltrp  46304  rpgtrecnn  46307  wallispilem3  46993  stirlinglem5  47004  vonioolem1  47606  cjnpoly  47855  fllog2  49596  blennnelnn  49604  dignn0flhalflem2  49644