Theorem nn0p1nn 12460

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7370  1c1 11048   + caddc 11050  ℕcn 12165  ℕ₀cn0 12421

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 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7692  ax-resscn 11104  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-addrcl 11108  ax-mulcl 11109  ax-mulrcl 11110  ax-mulcom 11111  ax-addass 11112  ax-mulass 11113  ax-distr 11114  ax-i2m1 11115  ax-1ne0 11116  ax-1rid 11117  ax-rnegex 11118  ax-rrecex 11119  ax-cnre 11120  ax-pre-lttri 11121  ax-pre-lttrn 11122  ax-pre-ltadd 11123

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6453  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7373  df-om 7824  df-2nd 7949  df-frecs 8238  df-wrecs 8269  df-recs 8318  df-rdg 8356  df-er 8649  df-en 8897  df-dom 8898  df-sdom 8899  df-pnf 11189  df-mnf 11190  df-ltxr 11192  df-nn 12166  df-n0 12422

This theorem is referenced by:  elnn0nn  12463  elz2  12526  peano5uzi  12602  fseq1p1m1  13538  fzonn0p1  13682  nn0ennn  13923  expnbnd  14176  faccl  14227  facdiv  14231  facwordi  14233  faclbnd  14234  facubnd  14244  bcm1k  14259  bcp1n  14260  bcp1nk  14261  bcpasc  14265  hashf1  14401  fz1isolem  14405  ccats1pfxeqrex  14658  wrdind  14665  wrd2ind  14666  ccats1pfxeqbi  14685  isercoll  15612  isercoll2  15613  iseralt  15629  bcxmas  15779  climcndslem1  15793  fprodser  15893  fallfacval4  15987  bpolycl  15996  bpolysum  15997  bpolydiflem  15998  fsumkthpow  16000  efcllem  16021  ruclem7  16182  ruclem8  16183  ruclem9  16184  sadcp1  16403  smupp1  16428  prmfac1  16668  iserodd  16784  pcfac  16848  1arith  16876  4sqlem12  16905  vdwlem11  16940  vdwlem12  16941  vdwlem13  16942  ramub1  16977  ramcl  16978  prmop1  16987  sylow1lem1  19514  efgsrel  19650  psdcl  22083  psdmul  22088  lebnumii  24900  lmnn  25198  vitalilem4  25547  itgpowd  25992  plyco  26181  dgrcolem2  26215  dgrco  26216  advlogexp  26599  cxpmul2  26633  atantayl3  26884  leibpilem2  26886  leibpi  26887  leibpisum  26888  log2cnv  26889  log2tlbnd  26890  log2ublem2  26892  log2ub  26894  birthdaylem2  26897  harmoniclbnd  26954  harmonicbnd4  26956  fsumharmonic  26957  facgam  27011  chpp1  27100  chtublem  27157  bcmono  27223  bcp1ctr  27225  gausslemma2dlem3  27314  2lgslem1a  27337  chtppilimlem1  27419  rplogsumlem2  27431  rpvmasumlem  27433  dchrisumlema  27434  dchrisumlem1  27435  dchrisum0flblem1  27454  dchrisum0lem1b  27461  dchrisum0lem1  27462  dchrisum0lem3  27465  selberg2lem  27496  pntrsumo1  27511  pntrlog2bndlem2  27524  pntrlog2bndlem4  27526  pntrlog2bndlem6a  27528  pntpbnd1  27532  pntpbnd2  27533  pntlemg  27544  pntlemj  27549  pntlemf  27551  qabvle  27571  ostth2lem2  27580  wlkonwlk1l  29644  wwlksnred  29874  wwlksnredwwlkn  29877  wwlksnredwwlkn0  29878  wwlksnwwlksnon  29897  minvecolem3  30857  minvecolem4  30861  cycpmco2lem4  33103  cycpmco2lem5  33104  cycpmco2lem6  33105  cycpmco2lem7  33106  archiabllem1a  33162  lmatfvlem  33800  signshnz  34577  subfacval2  35169  erdsze2lem2  35186  cvmliftlem7  35273  faclimlem1  35725  faclimlem2  35726  faclimlem3  35727  faclim  35728  faclim2  35730  poimirlem3  37612  poimirlem4  37613  poimirlem12  37621  poimirlem15  37624  poimirlem16  37625  poimirlem17  37626  poimirlem19  37628  poimirlem20  37629  poimirlem23  37632  poimirlem24  37633  poimirlem25  37634  poimirlem28  37637  poimirlem29  37638  poimirlem31  37640  heiborlem4  37803  heiborlem6  37805  fz1sump1  42293  sumcubes  42296  diophin  42755  rexrabdioph  42777  2rexfrabdioph  42779  3rexfrabdioph  42780  4rexfrabdioph  42781  6rexfrabdioph  42782  7rexfrabdioph  42783  elnn0rabdioph  42786  dvdsrabdioph  42793  irrapxlem4  42808  irrapxlem5  42809  2nn0ind  42929  jm2.27a  42989  bccp1k  44325  binomcxplemrat  44334  binomcxplemfrat  44335  recnnltrp  45368  rpgtrecnn  45371  wallispilem3  46060  stirlinglem5  46071  vonioolem1  46673  cjnpoly  46885  fllog2  48552  blennnelnn  48560  dignn0flhalflem2  48600