Theorem nn0p1nn 12570

Description: A nonnegative integer plus 1 is a positive integer. Strengthening of peano2nn 12272. (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 12271	. 2 ⊢ 1 ∈ ℕ
2		nn0nnaddcl 12562	. 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 7416  1c1 11128   + caddc 11130  ℕcn 12260  ℕ₀cn0 12531

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-om 7866  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275  df-nn 12261  df-n0 12532

This theorem is used by:  elnn0nn  12573  elz2  12636  peano5uzi  12713  fseq1p1m1  13655  fzonn0p1  13800  nn0ennn  14045  expnbnd  14298  faccl  14349  facdiv  14353  facwordi  14355  faclbnd  14356  facubnd  14366  bcm1k  14381  bcp1n  14382  bcp1nk  14383  bcpasc  14387  hashf1  14524  fz1isolem  14528  ccats1pfxeqrex  14786  wrdind  14793  wrd2ind  14794  ccats1pfxeqbi  14813  isercoll  15757  isercoll2  15758  iseralt  15774  bcxmas  15926  climcndslem1  15940  fprodser  16040  fallfacval4  16133  bpolycl  16142  bpolysum  16143  bpolydiflem  16144  fsumkthpow  16146  efcllem  16167  ruclem7  16328  ruclem8  16329  ruclem9  16330  sadcp1  16549  smupp1  16574  prmfac1  16815  iserodd  16931  pcfac  16995  1arith  17023  4sqlem12  17052  vdwlem11  17087  vdwlem12  17088  vdwlem13  17089  ramub1  17124  ramcl  17125  prmop1  17134  sylow1lem1  19726  efgsrel  19862  psdcl  22390  psdmul  22395  lebnumii  25195  lmnn  25492  vitalilem4  25840  itgpowd  26279  plyco  26468  dgrcolem2  26501  dgrco  26502  advlogexp  26890  cxpmul2  26924  atantayl3  27174  leibpilem2  27176  leibpi  27177  leibpisum  27178  log2cnv  27179  log2tlbnd  27180  log2ublem2  27182  log2ub  27184  birthdaylem2  27187  harmoniclbnd  27243  harmonicbnd4  27245  fsumharmonic  27246  facgam  27300  chpp1  27389  chtublem  27445  bcmono  27511  bcp1ctr  27513  gausslemma2dlem3  27602  2lgslem1a  27625  chtppilimlem1  27707  rplogsumlem2  27719  rpvmasumlem  27721  dchrisumlema  27722  dchrisumlem1  27723  dchrisum0flblem1  27742  dchrisum0lem1b  27749  dchrisum0lem1  27750  dchrisum0lem3  27753  selberg2lem  27784  pntrsumo1  27799  pntrlog2bndlem2  27812  pntrlog2bndlem4  27814  pntrlog2bndlem6a  27816  pntpbnd1  27820  pntpbnd2  27821  pntlemg  27832  pntlemj  27837  pntlemf  27839  qabvle  27859  ostth2lem2  27868  wlkonwlk1l  30107  wwlksnred  30346  wwlksnredwwlkn  30349  wwlksnredwwlkn0  30350  wwlksnwwlksnon  30369  minvecolem3  31343  minvecolem4  31347  cycpmco2lem4  33556  cycpmco2lem5  33557  cycpmco2lem6  33558  cycpmco2lem7  33559  archiabllem1a  33618  lmatfvlem  34312  signshnz  35086  subfacval2  35753  erdsze2lem2  35770  cvmliftlem7  35857  faclimlem1  36309  faclimlem2  36310  faclimlem3  36311  faclim  36312  faclim2  36314  poimirlem3  38359  poimirlem4  38360  poimirlem12  38368  poimirlem15  38371  poimirlem16  38372  poimirlem17  38373  poimirlem19  38375  poimirlem20  38376  poimirlem23  38379  poimirlem24  38380  poimirlem25  38381  poimirlem28  38384  poimirlem29  38385  poimirlem31  38387  heiborlem4  38551  heiborlem6  38553  fz1sump1  43172  sumcubes  43175  diophin  43604  rexrabdioph  43622  2rexfrabdioph  43624  3rexfrabdioph  43625  4rexfrabdioph  43626  6rexfrabdioph  43627  7rexfrabdioph  43628  elnn0rabdioph  43631  dvdsrabdioph  43638  irrapxlem4  43653  irrapxlem5  43654  2nn0ind  43773  jm2.27a  43833  bccp1k  45152  binomcxplemrat  45161  binomcxplemfrat  45162  recnnltrp  46193  rpgtrecnn  46196  wallispilem3  46882  stirlinglem5  46893  vonioolem1  47495  cjnpoly  47744  fllog2  49485  blennnelnn  49493  dignn0flhalflem2  49533