Theorem nn0p1nn 11939

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7158  1c1 10540   + caddc 10542  ℕcn 11640  ℕ₀cn0 11900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-ltxr 10682  df-nn 11641  df-n0 11901

This theorem is referenced by:  elnn0nn  11942  elz2  12002  peano5uzi  12074  fseq1p1m1  12984  fzonn0p1  13117  nn0ennn  13350  expnbnd  13596  faccl  13646  facdiv  13650  facwordi  13652  faclbnd  13653  facubnd  13663  bcm1k  13678  bcp1n  13679  bcp1nk  13680  bcpasc  13684  hashf1  13818  fz1isolem  13822  ccats1pfxeqrex  14079  wrdind  14086  wrd2ind  14087  ccats1pfxeqbi  14106  isercoll  15026  isercoll2  15027  iseralt  15043  bcxmas  15192  climcndslem1  15206  fprodser  15305  fallfacval4  15399  bpolycl  15408  bpolysum  15409  bpolydiflem  15410  fsumkthpow  15412  efcllem  15433  ruclem7  15591  ruclem8  15592  ruclem9  15593  sadcp1  15806  smupp1  15831  prmfac1  16065  iserodd  16174  pcfac  16237  1arith  16265  4sqlem12  16294  vdwlem11  16329  vdwlem12  16330  vdwlem13  16331  ramub1  16366  ramcl  16367  prmop1  16376  sylow1lem1  18725  efgsrel  18862  lebnumii  23572  lmnn  23868  vitalilem4  24214  plyco  24833  dgrcolem2  24866  dgrco  24867  advlogexp  25240  cxpmul2  25274  atantayl3  25519  leibpilem2  25521  leibpi  25522  leibpisum  25523  log2cnv  25524  log2tlbnd  25525  log2ublem2  25527  log2ub  25529  birthdaylem2  25532  harmoniclbnd  25588  harmonicbnd4  25590  fsumharmonic  25591  facgam  25645  chpp1  25734  chtublem  25789  bcmono  25855  bcp1ctr  25857  gausslemma2dlem3  25946  2lgslem1a  25969  chtppilimlem1  26051  rplogsumlem2  26063  rpvmasumlem  26065  dchrisumlema  26066  dchrisumlem1  26067  dchrisum0flblem1  26086  dchrisum0lem1b  26093  dchrisum0lem1  26094  dchrisum0lem3  26097  selberg2lem  26128  pntrsumo1  26143  pntrlog2bndlem2  26156  pntrlog2bndlem4  26158  pntrlog2bndlem6a  26160  pntpbnd1  26164  pntpbnd2  26165  pntlemg  26176  pntlemj  26181  pntlemf  26183  qabvle  26203  ostth2lem2  26212  wlkonwlk1l  27447  wwlksnred  27672  wwlksnredwwlkn  27675  wwlksnredwwlkn0  27676  wwlksnwwlksnon  27696  minvecolem3  28655  minvecolem4  28659  cycpmco2lem4  30773  cycpmco2lem5  30774  cycpmco2lem6  30775  cycpmco2lem7  30776  archiabllem1a  30822  lmatfvlem  31082  signshnz  31863  subfacval2  32436  erdsze2lem2  32453  cvmliftlem7  32540  faclimlem1  32977  faclimlem2  32978  faclimlem3  32979  faclim  32980  faclim2  32982  poimirlem3  34897  poimirlem4  34898  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem28  34922  poimirlem29  34923  poimirlem31  34925  heiborlem4  35094  heiborlem6  35096  diophin  39376  rexrabdioph  39398  2rexfrabdioph  39400  3rexfrabdioph  39401  4rexfrabdioph  39402  6rexfrabdioph  39403  7rexfrabdioph  39404  elnn0rabdioph  39407  dvdsrabdioph  39414  irrapxlem4  39429  irrapxlem5  39430  2nn0ind  39549  jm2.27a  39609  itgpowd  39828  bccp1k  40680  binomcxplemrat  40689  binomcxplemfrat  40690  recnnltrp  41652  rpgtrecnn  41656  wallispilem3  42359  stirlinglem5  42370  vonioolem1  42969  fllog2  44635  blennnelnn  44643  dignn0flhalflem2  44683