Theorem nn0p1nn 12544

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7419  1c1 11141   + caddc 11143  ℕcn 12245  ℕ₀cn0 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-ltxr 11285  df-nn 12246  df-n0 12506

This theorem is referenced by:  elnn0nn  12547  elz2  12609  peano5uzi  12684  fseq1p1m1  13610  fzonn0p1  13744  nn0ennn  13980  expnbnd  14230  faccl  14278  facdiv  14282  facwordi  14284  faclbnd  14285  facubnd  14295  bcm1k  14310  bcp1n  14311  bcp1nk  14312  bcpasc  14316  hashf1  14454  fz1isolem  14458  ccats1pfxeqrex  14701  wrdind  14708  wrd2ind  14709  ccats1pfxeqbi  14728  isercoll  15650  isercoll2  15651  iseralt  15667  bcxmas  15817  climcndslem1  15831  fprodser  15929  fallfacval4  16023  bpolycl  16032  bpolysum  16033  bpolydiflem  16034  fsumkthpow  16036  efcllem  16057  ruclem7  16216  ruclem8  16217  ruclem9  16218  sadcp1  16433  smupp1  16458  prmfac1  16695  iserodd  16807  pcfac  16871  1arith  16899  4sqlem12  16928  vdwlem11  16963  vdwlem12  16964  vdwlem13  16965  ramub1  17000  ramcl  17001  prmop1  17010  sylow1lem1  19565  efgsrel  19701  psdcl  22108  psdmul  22113  lebnumii  24936  lmnn  25235  vitalilem4  25584  itgpowd  26029  plyco  26220  dgrcolem2  26254  dgrco  26255  advlogexp  26634  cxpmul2  26668  atantayl3  26916  leibpilem2  26918  leibpi  26919  leibpisum  26920  log2cnv  26921  log2tlbnd  26922  log2ublem2  26924  log2ub  26926  birthdaylem2  26929  harmoniclbnd  26986  harmonicbnd4  26988  fsumharmonic  26989  facgam  27043  chpp1  27132  chtublem  27189  bcmono  27255  bcp1ctr  27257  gausslemma2dlem3  27346  2lgslem1a  27369  chtppilimlem1  27451  rplogsumlem2  27463  rpvmasumlem  27465  dchrisumlema  27466  dchrisumlem1  27467  dchrisum0flblem1  27486  dchrisum0lem1b  27493  dchrisum0lem1  27494  dchrisum0lem3  27497  selberg2lem  27528  pntrsumo1  27543  pntrlog2bndlem2  27556  pntrlog2bndlem4  27558  pntrlog2bndlem6a  27560  pntpbnd1  27564  pntpbnd2  27565  pntlemg  27576  pntlemj  27581  pntlemf  27583  qabvle  27603  ostth2lem2  27612  wlkonwlk1l  29549  wwlksnred  29775  wwlksnredwwlkn  29778  wwlksnredwwlkn0  29779  wwlksnwwlksnon  29798  minvecolem3  30758  minvecolem4  30762  cycpmco2lem4  32942  cycpmco2lem5  32943  cycpmco2lem6  32944  cycpmco2lem7  32945  archiabllem1a  32991  lmatfvlem  33547  signshnz  34354  subfacval2  34928  erdsze2lem2  34945  cvmliftlem7  35032  faclimlem1  35468  faclimlem2  35469  faclimlem3  35470  faclim  35471  faclim2  35473  poimirlem3  37227  poimirlem4  37228  poimirlem12  37236  poimirlem15  37239  poimirlem16  37240  poimirlem17  37241  poimirlem19  37243  poimirlem20  37244  poimirlem23  37247  poimirlem24  37248  poimirlem25  37249  poimirlem28  37252  poimirlem29  37253  poimirlem31  37255  heiborlem4  37418  heiborlem6  37420  fz1sump1  42005  sumcubes  42008  diophin  42334  rexrabdioph  42356  2rexfrabdioph  42358  3rexfrabdioph  42359  4rexfrabdioph  42360  6rexfrabdioph  42361  7rexfrabdioph  42362  elnn0rabdioph  42365  dvdsrabdioph  42372  irrapxlem4  42387  irrapxlem5  42388  2nn0ind  42508  jm2.27a  42568  bccp1k  43920  binomcxplemrat  43929  binomcxplemfrat  43930  recnnltrp  44897  rpgtrecnn  44900  wallispilem3  45593  stirlinglem5  45604  vonioolem1  46206  fllog2  47827  blennnelnn  47835  dignn0flhalflem2  47875