Theorem nn0p1nn 12488

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7390  1c1 11076   + caddc 11078  ℕcn 12193  ℕ₀cn0 12449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-nn 12194  df-n0 12450

This theorem is referenced by:  elnn0nn  12491  elz2  12554  peano5uzi  12630  fseq1p1m1  13566  fzonn0p1  13710  nn0ennn  13951  expnbnd  14204  faccl  14255  facdiv  14259  facwordi  14261  faclbnd  14262  facubnd  14272  bcm1k  14287  bcp1n  14288  bcp1nk  14289  bcpasc  14293  hashf1  14429  fz1isolem  14433  ccats1pfxeqrex  14687  wrdind  14694  wrd2ind  14695  ccats1pfxeqbi  14714  isercoll  15641  isercoll2  15642  iseralt  15658  bcxmas  15808  climcndslem1  15822  fprodser  15922  fallfacval4  16016  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  efcllem  16050  ruclem7  16211  ruclem8  16212  ruclem9  16213  sadcp1  16432  smupp1  16457  prmfac1  16697  iserodd  16813  pcfac  16877  1arith  16905  4sqlem12  16934  vdwlem11  16969  vdwlem12  16970  vdwlem13  16971  ramub1  17006  ramcl  17007  prmop1  17016  sylow1lem1  19535  efgsrel  19671  psdcl  22055  psdmul  22060  lebnumii  24872  lmnn  25170  vitalilem4  25519  itgpowd  25964  plyco  26153  dgrcolem2  26187  dgrco  26188  advlogexp  26571  cxpmul2  26605  atantayl3  26856  leibpilem2  26858  leibpi  26859  leibpisum  26860  log2cnv  26861  log2tlbnd  26862  log2ublem2  26864  log2ub  26866  birthdaylem2  26869  harmoniclbnd  26926  harmonicbnd4  26928  fsumharmonic  26929  facgam  26983  chpp1  27072  chtublem  27129  bcmono  27195  bcp1ctr  27197  gausslemma2dlem3  27286  2lgslem1a  27309  chtppilimlem1  27391  rplogsumlem2  27403  rpvmasumlem  27405  dchrisumlema  27406  dchrisumlem1  27407  dchrisum0flblem1  27426  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem3  27437  selberg2lem  27468  pntrsumo1  27483  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntrlog2bndlem6a  27500  pntpbnd1  27504  pntpbnd2  27505  pntlemg  27516  pntlemj  27521  pntlemf  27523  qabvle  27543  ostth2lem2  27552  wlkonwlk1l  29598  wwlksnred  29829  wwlksnredwwlkn  29832  wwlksnredwwlkn0  29833  wwlksnwwlksnon  29852  minvecolem3  30812  minvecolem4  30816  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  archiabllem1a  33152  lmatfvlem  33812  signshnz  34589  subfacval2  35181  erdsze2lem2  35198  cvmliftlem7  35285  faclimlem1  35737  faclimlem2  35738  faclimlem3  35739  faclim  35740  faclim2  35742  poimirlem3  37624  poimirlem4  37625  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  heiborlem4  37815  heiborlem6  37817  fz1sump1  42305  sumcubes  42308  diophin  42767  rexrabdioph  42789  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  elnn0rabdioph  42798  dvdsrabdioph  42805  irrapxlem4  42820  irrapxlem5  42821  2nn0ind  42941  jm2.27a  43001  bccp1k  44337  binomcxplemrat  44346  binomcxplemfrat  44347  recnnltrp  45380  rpgtrecnn  45383  wallispilem3  46072  stirlinglem5  46083  vonioolem1  46685  fllog2  48561  blennnelnn  48569  dignn0flhalflem2  48609