Theorem nn0p1nn 11594

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

Syntax hints:   → wi 4   ∈ wcel 2156  (class class class)co 6870  1c1 10218   + caddc 10220  ℕcn 11301  ℕ₀cn0 11555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-pnf 10357  df-mnf 10358  df-ltxr 10360  df-nn 11302  df-n0 11556

This theorem is referenced by:  elnn0nn  11597  elz2  11656  peano5uzi  11728  fseq1p1m1  12633  fzonn0p1  12765  nn0ennn  12998  expnbnd  13212  faccl  13286  facdiv  13290  facwordi  13292  faclbnd  13293  facubnd  13303  bcm1k  13318  bcp1n  13319  bcp1nk  13320  bcpasc  13324  hashf1  13454  fz1isolem  13458  wrdind  13696  wrd2ind  13697  ccats1swrdeqbi  13718  isercoll  14617  isercoll2  14618  iseralt  14634  bcxmas  14785  climcndslem1  14799  fprodser  14896  fallfacval4  14990  bpolycl  14999  bpolysum  15000  bpolydiflem  15001  fsumkthpow  15003  efcllem  15024  ruclem7  15181  ruclem8  15182  ruclem9  15183  sadcp1  15392  smupp1  15417  prmfac1  15644  iserodd  15753  pcfac  15816  1arith  15844  4sqlem12  15873  vdwlem11  15908  vdwlem12  15909  vdwlem13  15910  ramub1  15945  ramcl  15946  prmop1  15955  sylow1lem1  18210  efgsrel  18344  efgsp1  18347  lebnumii  22975  lmnn  23271  vitalilem4  23591  plyco  24210  dgrcolem2  24243  dgrco  24244  advlogexp  24614  cxpmul2  24648  atantayl3  24879  leibpilem2  24881  leibpi  24882  leibpisum  24883  log2cnv  24884  log2tlbnd  24885  log2ublem2  24887  log2ub  24889  birthdaylem2  24892  harmoniclbnd  24948  harmonicbnd4  24950  fsumharmonic  24951  facgam  25005  chpp1  25094  chtublem  25149  bcmono  25215  bcp1ctr  25217  gausslemma2dlem3  25306  2lgslem1a  25329  chtppilimlem1  25375  rplogsumlem2  25387  rpvmasumlem  25389  dchrisumlema  25390  dchrisumlem1  25391  dchrisum0flblem1  25410  dchrisum0lem1b  25417  dchrisum0lem1  25418  dchrisum0lem3  25421  selberg2lem  25452  pntrsumo1  25467  pntrlog2bndlem2  25480  pntrlog2bndlem4  25482  pntrlog2bndlem6a  25484  pntpbnd1  25488  pntpbnd2  25489  pntlemg  25500  pntlemj  25505  pntlemf  25507  qabvle  25527  ostth2lem2  25536  wlkonwlk1l  26786  wwlksnred  27028  wwlksnredwwlkn  27031  wwlksnredwwlkn0  27032  wwlksnwwlksnon  27052  wwlksnwwlksnonOLD  27054  minvecolem3  28059  minvecolem4  28063  archiabllem1a  30069  lmatfvlem  30205  signshnz  30992  subfacval2  31490  erdsze2lem2  31507  cvmliftlem7  31594  faclimlem1  31949  faclimlem2  31950  faclimlem3  31951  faclim  31952  faclim2  31954  poimirlem3  33723  poimirlem4  33724  poimirlem12  33732  poimirlem15  33735  poimirlem16  33736  poimirlem17  33737  poimirlem19  33739  poimirlem20  33740  poimirlem23  33743  poimirlem24  33744  poimirlem25  33745  poimirlem28  33748  poimirlem29  33749  poimirlem31  33751  heiborlem4  33922  heiborlem6  33924  diophin  37835  rexrabdioph  37857  2rexfrabdioph  37859  3rexfrabdioph  37860  4rexfrabdioph  37861  6rexfrabdioph  37862  7rexfrabdioph  37863  elnn0rabdioph  37866  dvdsrabdioph  37873  irrapxlem4  37888  irrapxlem5  37889  2nn0ind  38008  jm2.27a  38070  itgpowd  38297  bccp1k  39037  binomcxplemrat  39046  binomcxplemfrat  39047  recnnltrp  40070  rpgtrecnn  40074  wallispilem3  40760  stirlinglem5  40771  vonioolem1  41373  ccats1pfxeqrex  41994  ccats1pfxeqbi  42003  fllog2  42927  blennnelnn  42935  dignn0flhalflem2  42975