Theorem nn0p1nn 12542

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

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 7410  1c1 11100   + caddc 11102  ℕcn 12232  ℕ₀cn0 12503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-ltxr 11247  df-nn 12233  df-n0 12504

This theorem is referenced by:  elnn0nn  12545  elz2  12608  peano5uzi  12684  fseq1p1m1  13625  fzonn0p1  13770  nn0ennn  14014  expnbnd  14267  faccl  14318  facdiv  14322  facwordi  14324  faclbnd  14325  facubnd  14335  bcm1k  14350  bcp1n  14351  bcp1nk  14352  bcpasc  14356  hashf1  14493  fz1isolem  14497  ccats1pfxeqrex  14751  wrdind  14758  wrd2ind  14759  ccats1pfxeqbi  14778  isercoll  15718  isercoll2  15719  iseralt  15735  bcxmas  15888  climcndslem1  15902  fprodser  16002  fallfacval4  16096  bpolycl  16105  bpolysum  16106  bpolydiflem  16107  fsumkthpow  16109  efcllem  16130  ruclem7  16291  ruclem8  16292  ruclem9  16293  sadcp1  16512  smupp1  16537  prmfac1  16778  iserodd  16894  pcfac  16958  1arith  16986  4sqlem12  17015  vdwlem11  17050  vdwlem12  17051  vdwlem13  17052  ramub1  17087  ramcl  17088  prmop1  17097  sylow1lem1  19667  efgsrel  19803  psdcl  22303  psdmul  22308  lebnumii  25104  lmnn  25401  vitalilem4  25749  itgpowd  26188  plyco  26377  dgrcolem2  26410  dgrco  26411  advlogexp  26796  cxpmul2  26830  atantayl3  27080  leibpilem2  27082  leibpi  27083  leibpisum  27084  log2cnv  27085  log2tlbnd  27086  log2ublem2  27088  log2ub  27090  birthdaylem2  27093  harmoniclbnd  27149  harmonicbnd4  27151  fsumharmonic  27152  facgam  27206  chpp1  27295  chtublem  27351  bcmono  27417  bcp1ctr  27419  gausslemma2dlem3  27508  2lgslem1a  27531  chtppilimlem1  27613  rplogsumlem2  27625  rpvmasumlem  27627  dchrisumlema  27628  dchrisumlem1  27629  dchrisum0flblem1  27648  dchrisum0lem1b  27655  dchrisum0lem1  27656  dchrisum0lem3  27659  selberg2lem  27690  pntrsumo1  27705  pntrlog2bndlem2  27718  pntrlog2bndlem4  27720  pntrlog2bndlem6a  27722  pntpbnd1  27726  pntpbnd2  27727  pntlemg  27738  pntlemj  27743  pntlemf  27745  qabvle  27765  ostth2lem2  27774  wlkonwlk1l  29977  wwlksnred  30207  wwlksnredwwlkn  30210  wwlksnredwwlkn0  30211  wwlksnwwlksnon  30230  minvecolem3  31194  minvecolem4  31198  cycpmco2lem4  33415  cycpmco2lem5  33416  cycpmco2lem6  33417  cycpmco2lem7  33418  archiabllem1a  33477  lmatfvlem  34171  signshnz  34944  subfacval2  35633  erdsze2lem2  35650  cvmliftlem7  35737  faclimlem1  36189  faclimlem2  36190  faclimlem3  36191  faclim  36192  faclim2  36194  poimirlem3  38218  poimirlem4  38219  poimirlem12  38227  poimirlem15  38230  poimirlem16  38231  poimirlem17  38232  poimirlem19  38234  poimirlem20  38235  poimirlem23  38238  poimirlem24  38239  poimirlem25  38240  poimirlem28  38243  poimirlem29  38244  poimirlem31  38246  heiborlem4  38409  heiborlem6  38411  fz1sump1  43017  sumcubes  43020  diophin  43451  rexrabdioph  43469  2rexfrabdioph  43471  3rexfrabdioph  43472  4rexfrabdioph  43473  6rexfrabdioph  43474  7rexfrabdioph  43475  elnn0rabdioph  43478  dvdsrabdioph  43485  irrapxlem4  43500  irrapxlem5  43501  2nn0ind  43620  jm2.27a  43680  bccp1k  44999  binomcxplemrat  45008  binomcxplemfrat  45009  recnnltrp  46040  rpgtrecnn  46043  wallispilem3  46729  stirlinglem5  46740  vonioolem1  47342  cjnpoly  47571  fllog2  49293  blennnelnn  49301  dignn0flhalflem2  49341