Theorem nn0p1nn 12669

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7440  1c1 11225   + caddc 11227  ℕcn 12359  ℕ₀cn0 12630

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-om 7899  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-ltxr 11372  df-nn 12360  df-n0 12631

This theorem is used by:  elnn0nn  12672  elz2  12735  peano5uzi  12812  fseq1p1m1  13756  fzonn0p1  13901  nn0ennn  14146  expnbnd  14400  faccl  14451  facdiv  14455  facwordi  14457  faclbnd  14458  facubnd  14468  bcm1k  14483  bcp1n  14484  bcp1nk  14485  bcpasc  14489  hashf1  14626  fz1isolem  14630  ccats1pfxeqrex  14889  wrdind  14896  wrd2ind  14897  ccats1pfxeqbi  14916  isercoll  15861  isercoll2  15862  iseralt  15878  bcxmas  16030  climcndslem1  16044  fprodser  16142  fallfacval4  16235  bpolycl  16244  bpolysum  16245  bpolydiflem  16246  fsumkthpow  16248  efcllem  16269  ruclem7  16430  ruclem8  16431  ruclem9  16432  sadcp1  16651  smupp1  16676  prmfac1  16922  iserodd  17039  pcfac  17103  1arith  17131  4sqlem12  17160  vdwlem11  17195  vdwlem12  17196  vdwlem13  17197  ramub1  17232  ramcl  17233  prmop1  17242  sylow1lem1  19839  efgsrel  19975  psdcl  22509  psdmul  22514  lebnumii  25314  lmnn  25611  vitalilem4  25959  itgpowd  26397  plyco  26587  dgrcolem2  26620  dgrco  26621  advlogexp  27010  cxpmul2  27044  atantayl3  27294  leibpilem2  27296  leibpi  27297  leibpisum  27298  log2cnv  27299  log2tlbnd  27300  log2ublem2  27302  log2ub  27304  birthdaylem2  27307  harmoniclbnd  27363  harmonicbnd4  27365  fsumharmonic  27366  facgam  27420  chpp1  27509  chtublem  27565  bcmono  27631  bcp1ctr  27633  gausslemma2dlem3  27722  2lgslem1a  27745  chtppilimlem1  27827  rplogsumlem2  27839  rpvmasumlem  27841  dchrisumlema  27842  dchrisumlem1  27843  dchrisum0flblem1  27862  dchrisum0lem1b  27869  dchrisum0lem1  27870  dchrisum0lem3  27873  selberg2lem  27904  pntrsumo1  27919  pntrlog2bndlem2  27932  pntrlog2bndlem4  27934  pntrlog2bndlem6a  27936  pntpbnd1  27940  pntpbnd2  27941  pntlemg  27952  pntlemj  27957  pntlemf  27959  qabvle  27979  ostth2lem2  27988  wlkonwlk1l  30269  wwlksnred  30508  wwlksnredwwlkn  30511  wwlksnredwwlkn0  30512  wwlksnwwlksnon  30531  minvecolem3  31505  minvecolem4  31509  cycpmco2lem4  33757  cycpmco2lem5  33758  cycpmco2lem6  33759  cycpmco2lem7  33760  archiabllem1a  33819  lmatfvlem  34514  signshnz  35287  subfacval2  36118  erdsze2lem2  36135  cvmliftlem7  36222  faclimlem1  36685  faclimlem2  36686  faclimlem3  36687  faclim  36688  faclim2  36690  poimirlem3  38732  poimirlem4  38733  poimirlem12  38741  poimirlem15  38744  poimirlem16  38745  poimirlem17  38746  poimirlem19  38748  poimirlem20  38749  poimirlem23  38752  poimirlem24  38753  poimirlem25  38754  poimirlem28  38757  poimirlem29  38758  poimirlem31  38760  heiborlem4  38939  heiborlem6  38941  fz1sump1  43558  sumcubes  43561  diophin  43974  rexrabdioph  43992  2rexfrabdioph  43994  3rexfrabdioph  43995  4rexfrabdioph  43996  6rexfrabdioph  43997  7rexfrabdioph  43998  elnn0rabdioph  44001  dvdsrabdioph  44008  irrapxlem4  44023  irrapxlem5  44024  2nn0ind  44143  jm2.27a  44203  bccp1k  45515  binomcxplemrat  45524  binomcxplemfrat  45525  recnnltrp  46591  rpgtrecnn  46594  wallispilem3  47280  stirlinglem5  47291  vonioolem1  47893  cjnpoly  48142  fllog2  49883  blennnelnn  49891  dignn0flhalflem2  49931