MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0p1nn Structured version   Visualization version   GIF version

Theorem nn0p1nn 11544
Description: A nonnegative integer plus 1 is a positive integer. Strengthening of peano2nn 11244. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)
Assertion
Ref Expression
nn0p1nn (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)

Proof of Theorem nn0p1nn
StepHypRef Expression
1 1nn 11243 . 2 1 ∈ ℕ
2 nn0nnaddcl 11536 . 2 ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ) → (𝑁 + 1) ∈ ℕ)
31, 2mpan2 709 1 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  (class class class)co 6814  1c1 10149   + caddc 10151  cn 11232  0cn0 11504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6817  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-pnf 10288  df-mnf 10289  df-ltxr 10291  df-nn 11233  df-n0 11505
This theorem is referenced by:  elnn0nn  11547  elz2  11606  peano5uzi  11678  fseq1p1m1  12627  fzonn0p1  12759  nn0ennn  12992  expnbnd  13207  faccl  13284  facdiv  13288  facwordi  13290  faclbnd  13291  facubnd  13301  bcm1k  13316  bcp1n  13317  bcp1nk  13318  bcpasc  13322  hashf1  13453  fz1isolem  13457  wrdind  13696  wrd2ind  13697  ccats1swrdeqbi  13718  isercoll  14617  isercoll2  14618  iseralt  14634  bcxmas  14786  climcndslem1  14800  fprodser  14898  fallfacval4  14993  bpolycl  15002  bpolysum  15003  bpolydiflem  15004  fsumkthpow  15006  efcllem  15027  ruclem7  15184  ruclem8  15185  ruclem9  15186  sadcp1  15399  smupp1  15424  prmfac1  15653  iserodd  15762  pcfac  15825  1arith  15853  4sqlem12  15882  vdwlem11  15917  vdwlem12  15918  vdwlem13  15919  ramub1  15954  ramcl  15955  prmop1  15964  sylow1lem1  18233  efgsrel  18367  efgsp1  18370  lebnumii  22986  lmnn  23281  vitalilem4  23599  plyco  24216  dgrcolem2  24249  dgrco  24250  advlogexp  24621  cxpmul2  24655  atantayl3  24886  leibpilem2  24888  leibpi  24889  leibpisum  24890  log2cnv  24891  log2tlbnd  24892  log2ublem2  24894  log2ub  24896  birthdaylem2  24899  harmoniclbnd  24955  harmonicbnd4  24957  fsumharmonic  24958  facgam  25012  chpp1  25101  chtublem  25156  bcmono  25222  bcp1ctr  25224  gausslemma2dlem3  25313  2lgslem1a  25336  chtppilimlem1  25382  rplogsumlem2  25394  rpvmasumlem  25396  dchrisumlema  25397  dchrisumlem1  25398  dchrisum0flblem1  25417  dchrisum0lem1b  25424  dchrisum0lem1  25425  dchrisum0lem3  25428  selberg2lem  25459  pntrsumo1  25474  pntrlog2bndlem2  25487  pntrlog2bndlem4  25489  pntrlog2bndlem6a  25491  pntpbnd1  25495  pntpbnd2  25496  pntlemg  25507  pntlemj  25512  pntlemf  25514  qabvle  25534  ostth2lem2  25543  wlkonwlk1l  26790  wwlksnred  27031  wwlksnredwwlkn  27034  wwlksnredwwlkn0  27035  wwlksnwwlksnon  27054  wwlksnwwlksnonOLD  27056  minvecolem3  28062  minvecolem4  28066  archiabllem1a  30075  lmatfvlem  30211  signshnz  30998  subfacval2  31497  erdsze2lem2  31514  cvmliftlem7  31601  faclimlem1  31957  faclimlem2  31958  faclimlem3  31959  faclim  31960  faclim2  31962  poimirlem3  33743  poimirlem4  33744  poimirlem12  33752  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem19  33759  poimirlem20  33760  poimirlem23  33763  poimirlem24  33764  poimirlem25  33765  poimirlem28  33768  poimirlem29  33769  poimirlem31  33771  heiborlem4  33944  heiborlem6  33946  diophin  37856  rexrabdioph  37878  2rexfrabdioph  37880  3rexfrabdioph  37881  4rexfrabdioph  37882  6rexfrabdioph  37883  7rexfrabdioph  37884  elnn0rabdioph  37887  dvdsrabdioph  37894  irrapxlem4  37909  irrapxlem5  37910  2nn0ind  38030  jm2.27a  38092  itgpowd  38320  bccp1k  39060  binomcxplemrat  39069  binomcxplemfrat  39070  recnnltrp  40109  rpgtrecnn  40113  wallispilem3  40805  stirlinglem5  40816  vonioolem1  41418  ccats1pfxeqrex  41950  ccats1pfxeqbi  41959  fllog2  42890  blennnelnn  42898  dignn0flhalflem2  42938
  Copyright terms: Public domain W3C validator