Theorem nn0p1nn 12645

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420  1c1 11201   + caddc 11203  ℕcn 12335  ℕ₀cn0 12606

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-nn 12336  df-n0 12607

This theorem is used by:  elnn0nn  12648  elz2  12711  peano5uzi  12788  fseq1p1m1  13732  fzonn0p1  13877  nn0ennn  14122  expnbnd  14376  faccl  14427  facdiv  14431  facwordi  14433  faclbnd  14434  facubnd  14444  bcm1k  14459  bcp1n  14460  bcp1nk  14461  bcpasc  14465  hashf1  14602  fz1isolem  14606  ccats1pfxeqrex  14864  wrdind  14871  wrd2ind  14872  ccats1pfxeqbi  14891  isercoll  15835  isercoll2  15836  iseralt  15852  bcxmas  16004  climcndslem1  16018  fprodser  16116  fallfacval4  16209  bpolycl  16218  bpolysum  16219  bpolydiflem  16220  fsumkthpow  16222  efcllem  16243  ruclem7  16404  ruclem8  16405  ruclem9  16406  sadcp1  16625  smupp1  16650  prmfac1  16896  iserodd  17013  pcfac  17077  1arith  17105  4sqlem12  17134  vdwlem11  17169  vdwlem12  17170  vdwlem13  17171  ramub1  17206  ramcl  17207  prmop1  17216  sylow1lem1  19812  efgsrel  19948  psdcl  22482  psdmul  22487  lebnumii  25287  lmnn  25584  vitalilem4  25932  itgpowd  26370  plyco  26560  dgrcolem2  26593  dgrco  26594  advlogexp  26983  cxpmul2  27017  atantayl3  27267  leibpilem2  27269  leibpi  27270  leibpisum  27271  log2cnv  27272  log2tlbnd  27273  log2ublem2  27275  log2ub  27277  birthdaylem2  27280  harmoniclbnd  27336  harmonicbnd4  27338  fsumharmonic  27339  facgam  27393  chpp1  27482  chtublem  27538  bcmono  27604  bcp1ctr  27606  gausslemma2dlem3  27695  2lgslem1a  27718  chtppilimlem1  27800  rplogsumlem2  27812  rpvmasumlem  27814  dchrisumlema  27815  dchrisumlem1  27816  dchrisum0flblem1  27835  dchrisum0lem1b  27842  dchrisum0lem1  27843  dchrisum0lem3  27846  selberg2lem  27877  pntrsumo1  27892  pntrlog2bndlem2  27905  pntrlog2bndlem4  27907  pntrlog2bndlem6a  27909  pntpbnd1  27913  pntpbnd2  27914  pntlemg  27925  pntlemj  27930  pntlemf  27932  qabvle  27952  ostth2lem2  27961  wlkonwlk1l  30242  wwlksnred  30481  wwlksnredwwlkn  30484  wwlksnredwwlkn0  30485  wwlksnwwlksnon  30504  minvecolem3  31478  minvecolem4  31482  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2lem7  33693  archiabllem1a  33752  lmatfvlem  34447  signshnz  35220  subfacval2  35952  erdsze2lem2  35969  cvmliftlem7  36056  faclimlem1  36508  faclimlem2  36509  faclimlem3  36510  faclim  36511  faclim2  36513  poimirlem3  38542  poimirlem4  38543  poimirlem12  38551  poimirlem15  38554  poimirlem16  38555  poimirlem17  38556  poimirlem19  38558  poimirlem20  38559  poimirlem23  38562  poimirlem24  38563  poimirlem25  38564  poimirlem28  38567  poimirlem29  38568  poimirlem31  38570  heiborlem4  38749  heiborlem6  38751  fz1sump1  43368  sumcubes  43371  diophin  43783  rexrabdioph  43801  2rexfrabdioph  43803  3rexfrabdioph  43804  4rexfrabdioph  43805  6rexfrabdioph  43806  7rexfrabdioph  43807  elnn0rabdioph  43810  dvdsrabdioph  43817  irrapxlem4  43832  irrapxlem5  43833  2nn0ind  43952  jm2.27a  44012  bccp1k  45325  binomcxplemrat  45334  binomcxplemfrat  45335  recnnltrp  46388  rpgtrecnn  46391  wallispilem3  47077  stirlinglem5  47088  vonioolem1  47690  cjnpoly  47939  fllog2  49680  blennnelnn  49688  dignn0flhalflem2  49728