Theorem nn0p1nn 12094

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

Syntax hints:   → wi 4   ∈ wcel 2112  (class class class)co 7191  1c1 10695   + caddc 10697  ℕcn 11795  ℕ₀cn0 12055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-ltxr 10837  df-nn 11796  df-n0 12056

This theorem is referenced by:  elnn0nn  12097  elz2  12159  peano5uzi  12231  fseq1p1m1  13151  fzonn0p1  13284  nn0ennn  13517  expnbnd  13764  faccl  13814  facdiv  13818  facwordi  13820  faclbnd  13821  facubnd  13831  bcm1k  13846  bcp1n  13847  bcp1nk  13848  bcpasc  13852  hashf1  13988  fz1isolem  13992  ccats1pfxeqrex  14245  wrdind  14252  wrd2ind  14253  ccats1pfxeqbi  14272  isercoll  15196  isercoll2  15197  iseralt  15213  bcxmas  15362  climcndslem1  15376  fprodser  15474  fallfacval4  15568  bpolycl  15577  bpolysum  15578  bpolydiflem  15579  fsumkthpow  15581  efcllem  15602  ruclem7  15760  ruclem8  15761  ruclem9  15762  sadcp1  15977  smupp1  16002  prmfac1  16241  iserodd  16351  pcfac  16415  1arith  16443  4sqlem12  16472  vdwlem11  16507  vdwlem12  16508  vdwlem13  16509  ramub1  16544  ramcl  16545  prmop1  16554  sylow1lem1  18941  efgsrel  19078  lebnumii  23817  lmnn  24114  vitalilem4  24462  itgpowd  24901  plyco  25089  dgrcolem2  25122  dgrco  25123  advlogexp  25497  cxpmul2  25531  atantayl3  25776  leibpilem2  25778  leibpi  25779  leibpisum  25780  log2cnv  25781  log2tlbnd  25782  log2ublem2  25784  log2ub  25786  birthdaylem2  25789  harmoniclbnd  25845  harmonicbnd4  25847  fsumharmonic  25848  facgam  25902  chpp1  25991  chtublem  26046  bcmono  26112  bcp1ctr  26114  gausslemma2dlem3  26203  2lgslem1a  26226  chtppilimlem1  26308  rplogsumlem2  26320  rpvmasumlem  26322  dchrisumlema  26323  dchrisumlem1  26324  dchrisum0flblem1  26343  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem3  26354  selberg2lem  26385  pntrsumo1  26400  pntrlog2bndlem2  26413  pntrlog2bndlem4  26415  pntrlog2bndlem6a  26417  pntpbnd1  26421  pntpbnd2  26422  pntlemg  26433  pntlemj  26438  pntlemf  26440  qabvle  26460  ostth2lem2  26469  wlkonwlk1l  27705  wwlksnred  27930  wwlksnredwwlkn  27933  wwlksnredwwlkn0  27934  wwlksnwwlksnon  27953  minvecolem3  28911  minvecolem4  28915  cycpmco2lem4  31069  cycpmco2lem5  31070  cycpmco2lem6  31071  cycpmco2lem7  31072  archiabllem1a  31118  lmatfvlem  31433  signshnz  32236  subfacval2  32816  erdsze2lem2  32833  cvmliftlem7  32920  faclimlem1  33378  faclimlem2  33379  faclimlem3  33380  faclim  33381  faclim2  33383  poimirlem3  35466  poimirlem4  35467  poimirlem12  35475  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem23  35486  poimirlem24  35487  poimirlem25  35488  poimirlem28  35491  poimirlem29  35492  poimirlem31  35494  heiborlem4  35658  heiborlem6  35660  diophin  40238  rexrabdioph  40260  2rexfrabdioph  40262  3rexfrabdioph  40263  4rexfrabdioph  40264  6rexfrabdioph  40265  7rexfrabdioph  40266  elnn0rabdioph  40269  dvdsrabdioph  40276  irrapxlem4  40291  irrapxlem5  40292  2nn0ind  40411  jm2.27a  40471  bccp1k  41573  binomcxplemrat  41582  binomcxplemfrat  41583  recnnltrp  42530  rpgtrecnn  42533  wallispilem3  43226  stirlinglem5  43237  vonioolem1  43836  fllog2  45530  blennnelnn  45538  dignn0flhalflem2  45578