Theorem nn0p1nn 12522

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

Syntax hints:   → wi 4   ∈ wcel 2144  (class class class)co 7398  1c1 11076   + caddc 11078  ℕcn 12212  ℕ₀cn0 12483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7401  df-om 7849  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-ltxr 11223  df-nn 12213  df-n0 12484

This theorem is referenced by:  elnn0nn  12525  elz2  12588  peano5uzi  12664  fseq1p1m1  13605  fzonn0p1  13750  nn0ennn  13994  expnbnd  14247  faccl  14298  facdiv  14302  facwordi  14304  faclbnd  14305  facubnd  14315  bcm1k  14330  bcp1n  14331  bcp1nk  14332  bcpasc  14336  hashf1  14472  fz1isolem  14476  ccats1pfxeqrex  14730  wrdind  14737  wrd2ind  14738  ccats1pfxeqbi  14757  isercoll  15697  isercoll2  15698  iseralt  15714  bcxmas  15867  climcndslem1  15881  fprodser  15981  fallfacval4  16075  bpolycl  16084  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  efcllem  16109  ruclem7  16270  ruclem8  16271  ruclem9  16272  sadcp1  16491  smupp1  16516  prmfac1  16757  iserodd  16873  pcfac  16937  1arith  16965  4sqlem12  16994  vdwlem11  17029  vdwlem12  17030  vdwlem13  17031  ramub1  17066  ramcl  17067  prmop1  17076  sylow1lem1  19640  efgsrel  19776  psdcl  22228  psdmul  22233  lebnumii  25030  lmnn  25327  vitalilem4  25675  itgpowd  26114  plyco  26303  dgrcolem2  26336  dgrco  26337  advlogexp  26722  cxpmul2  26756  atantayl3  27006  leibpilem2  27008  leibpi  27009  leibpisum  27010  log2cnv  27011  log2tlbnd  27012  log2ublem2  27014  log2ub  27016  birthdaylem2  27019  harmoniclbnd  27075  harmonicbnd4  27077  fsumharmonic  27078  facgam  27132  chpp1  27221  chtublem  27277  bcmono  27343  bcp1ctr  27345  gausslemma2dlem3  27434  2lgslem1a  27457  chtppilimlem1  27539  rplogsumlem2  27551  rpvmasumlem  27553  dchrisumlema  27554  dchrisumlem1  27555  dchrisum0flblem1  27574  dchrisum0lem1b  27581  dchrisum0lem1  27582  dchrisum0lem3  27585  selberg2lem  27616  pntrsumo1  27631  pntrlog2bndlem2  27644  pntrlog2bndlem4  27646  pntrlog2bndlem6a  27648  pntpbnd1  27652  pntpbnd2  27653  pntlemg  27664  pntlemj  27669  pntlemf  27671  qabvle  27691  ostth2lem2  27700  wlkonwlk1l  29864  wwlksnred  30094  wwlksnredwwlkn  30097  wwlksnredwwlkn0  30098  wwlksnwwlksnon  30117  minvecolem3  31081  minvecolem4  31085  cycpmco2lem4  33311  cycpmco2lem5  33312  cycpmco2lem6  33313  cycpmco2lem7  33314  archiabllem1a  33373  lmatfvlem  34114  signshnz  34887  subfacval2  35542  erdsze2lem2  35559  cvmliftlem7  35646  faclimlem1  36098  faclimlem2  36099  faclimlem3  36100  faclim  36101  faclim2  36103  poimirlem3  38127  poimirlem4  38128  poimirlem12  38136  poimirlem15  38139  poimirlem16  38140  poimirlem17  38141  poimirlem19  38143  poimirlem20  38144  poimirlem23  38147  poimirlem24  38148  poimirlem25  38149  poimirlem28  38152  poimirlem29  38153  poimirlem31  38155  heiborlem4  38318  heiborlem6  38320  fz1sump1  42924  sumcubes  42927  diophin  43358  rexrabdioph  43376  2rexfrabdioph  43378  3rexfrabdioph  43379  4rexfrabdioph  43380  6rexfrabdioph  43381  7rexfrabdioph  43382  elnn0rabdioph  43385  dvdsrabdioph  43392  irrapxlem4  43407  irrapxlem5  43408  2nn0ind  43527  jm2.27a  43587  bccp1k  44922  binomcxplemrat  44931  binomcxplemfrat  44932  recnnltrp  45957  rpgtrecnn  45960  wallispilem3  46646  stirlinglem5  46657  vonioolem1  47259  cjnpoly  47488  fllog2  49195  blennnelnn  49203  dignn0flhalflem2  49243