Theorem nn0p1nn 12473

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7364  1c1 11036   + caddc 11038  ℕcn 12171  ℕ₀cn0 12434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7367  df-om 7815  df-2nd 7940  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-ltxr 11181  df-nn 12172  df-n0 12435

This theorem is referenced by:  elnn0nn  12476  elz2  12539  peano5uzi  12615  fseq1p1m1  13549  fzonn0p1  13694  nn0ennn  13938  expnbnd  14191  faccl  14242  facdiv  14246  facwordi  14248  faclbnd  14249  facubnd  14259  bcm1k  14274  bcp1n  14275  bcp1nk  14276  bcpasc  14280  hashf1  14416  fz1isolem  14420  ccats1pfxeqrex  14674  wrdind  14681  wrd2ind  14682  ccats1pfxeqbi  14701  isercoll  15627  isercoll2  15628  iseralt  15644  bcxmas  15797  climcndslem1  15811  fprodser  15911  fallfacval4  16005  bpolycl  16014  bpolysum  16015  bpolydiflem  16016  fsumkthpow  16018  efcllem  16039  ruclem7  16200  ruclem8  16201  ruclem9  16202  sadcp1  16421  smupp1  16446  prmfac1  16687  iserodd  16803  pcfac  16867  1arith  16895  4sqlem12  16924  vdwlem11  16959  vdwlem12  16960  vdwlem13  16961  ramub1  16996  ramcl  16997  prmop1  17006  sylow1lem1  19570  efgsrel  19706  psdcl  22124  psdmul  22129  lebnumii  24930  lmnn  25227  vitalilem4  25575  itgpowd  26014  plyco  26203  dgrcolem2  26236  dgrco  26237  advlogexp  26616  cxpmul2  26650  atantayl3  26900  leibpilem2  26902  leibpi  26903  leibpisum  26904  log2cnv  26905  log2tlbnd  26906  log2ublem2  26908  log2ub  26910  birthdaylem2  26913  harmoniclbnd  26969  harmonicbnd4  26971  fsumharmonic  26972  facgam  27026  chpp1  27115  chtublem  27171  bcmono  27237  bcp1ctr  27239  gausslemma2dlem3  27328  2lgslem1a  27351  chtppilimlem1  27433  rplogsumlem2  27445  rpvmasumlem  27447  dchrisumlema  27448  dchrisumlem1  27449  dchrisum0flblem1  27468  dchrisum0lem1b  27475  dchrisum0lem1  27476  dchrisum0lem3  27479  selberg2lem  27510  pntrsumo1  27525  pntrlog2bndlem2  27538  pntrlog2bndlem4  27540  pntrlog2bndlem6a  27542  pntpbnd1  27546  pntpbnd2  27547  pntlemg  27558  pntlemj  27563  pntlemf  27565  qabvle  27585  ostth2lem2  27594  wlkonwlk1l  29727  wwlksnred  29957  wwlksnredwwlkn  29960  wwlksnredwwlkn0  29961  wwlksnwwlksnon  29980  minvecolem3  30944  minvecolem4  30948  cycpmco2lem4  33187  cycpmco2lem5  33188  cycpmco2lem6  33189  cycpmco2lem7  33190  archiabllem1a  33249  lmatfvlem  33956  signshnz  34732  subfacval2  35366  erdsze2lem2  35383  cvmliftlem7  35470  faclimlem1  35922  faclimlem2  35923  faclimlem3  35924  faclim  35925  faclim2  35927  poimirlem3  37941  poimirlem4  37942  poimirlem12  37950  poimirlem15  37953  poimirlem16  37954  poimirlem17  37955  poimirlem19  37957  poimirlem20  37958  poimirlem23  37961  poimirlem24  37962  poimirlem25  37963  poimirlem28  37966  poimirlem29  37967  poimirlem31  37969  heiborlem4  38132  heiborlem6  38134  fz1sump1  42739  sumcubes  42742  diophin  43201  rexrabdioph  43219  2rexfrabdioph  43221  3rexfrabdioph  43222  4rexfrabdioph  43223  6rexfrabdioph  43224  7rexfrabdioph  43225  elnn0rabdioph  43228  dvdsrabdioph  43235  irrapxlem4  43250  irrapxlem5  43251  2nn0ind  43370  jm2.27a  43430  bccp1k  44765  binomcxplemrat  44774  binomcxplemfrat  44775  recnnltrp  45803  rpgtrecnn  45806  wallispilem3  46492  stirlinglem5  46503  vonioolem1  47105  cjnpoly  47328  fllog2  49035  blennnelnn  49043  dignn0flhalflem2  49083