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

Theorem 2nn 11688
Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
Assertion
Ref Expression
2nn 2 ∈ ℕ

Proof of Theorem 2nn
StepHypRef Expression
1 df-2 11678 . 2 2 = (1 + 1)
2 1nn 11626 . . 3 1 ∈ ℕ
3 peano2nn 11627 . . 3 (1 ∈ ℕ → (1 + 1) ∈ ℕ)
42, 3ax-mp 5 . 2 (1 + 1) ∈ ℕ
51, 4eqeltri 2908 1 2 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  (class class class)co 7130  1c1 10515   + caddc 10517  cn 11615  2c2 11670
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-1cn 10572
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7133  df-om 7556  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-nn 11616  df-2 11678
This theorem is referenced by:  3nn  11694  2nn0  11892  2z  11992  uz3m2nn  12269  ige2m1fz1  12979  sqeq0  13470  sqeq0d  13493  expmulnbnd  13580  faclbnd5  13642  bcn2  13663  f1oun2prg  14258  wrdl2exs2  14287  pfx2  14288  wwlktovf  14299  reusq0  14801  climcndslem1  15183  climcndslem2  15184  climcnds  15185  harmonic  15193  geo2sum  15208  geo2lim  15210  ege2le3  15422  ef01bndlem  15516  egt2lt3  15538  nthruc  15584  mod2eq0even  15674  bits0o  15756  bitsp1  15757  bitsfzolem  15760  bitsfzo  15761  bitsmod  15762  bitsfi  15763  bitscmp  15764  bitsinv1lem  15767  bitsinv1  15768  2ebits  15773  bitsinvp1  15775  sadcaddlem  15783  sadadd3  15787  sadaddlem  15792  sadasslem  15796  bitsres  15799  bitsuz  15800  bitsshft  15801  smumullem  15818  smumul  15819  sqgcd  15886  3lcm2e6woprm  15936  prm2orodd  16012  4nprm  16016  isevengcd2  16047  3lcm2e6  16049  pythagtriplem4  16133  iserodd  16149  oddprmdvds  16216  prmreclem3  16231  prmreclem5  16233  prmreclem6  16234  4sqlem12  16269  vdwlem3  16296  vdwlem9  16302  vdwlem10  16303  prmo2  16353  dec2dvds  16376  dec5nprm  16379  dec2nprm  16380  2expltfac  16405  5prm  16421  6nprm  16422  7prm  16423  8nprm  16424  10nprm  16426  11prm  16427  17prm  16429  23prm  16431  37prm  16433  43prm  16434  83prm  16435  139prm  16436  163prm  16437  317prm  16438  631prm  16439  1259lem1  16443  1259lem2  16444  1259lem3  16445  1259lem4  16446  1259lem5  16447  1259prm  16448  2503lem1  16449  2503lem2  16450  2503lem3  16451  2503prm  16452  4001lem1  16453  4001lem2  16454  4001lem3  16455  4001lem4  16456  4001prm  16457  plusgndx  16574  plusgid  16575  grpstr  16588  grpbase  16589  grpplusg  16590  ressplusg  16591  rngstr  16598  lmodstr  16615  topgrpstr  16640  dsndx  16654  dsid  16655  odrngstr  16658  ressds  16665  imasvalstr  16704  pmtrprfvalrn  18595  psgnunilem2  18602  psgnprfval  18628  psgnprfval1  18629  mgpds  19228  oppradd  19359  sraaddg  19927  srads  19934  opsrplusg  20236  cnfldstr  20523  cnfldfun  20533  zlmplusg  20642  znadd  20663  m2detleiblem1  21209  m2detleiblem5  21210  m2detleiblem6  21211  m2detleiblem3  21214  m2detleiblem4  21215  m2detleib  21216  tmslem  23068  tngplusg  23227  ovollb2lem  24071  ovolunlem1a  24079  ovolunlem1  24080  ovoliunlem1  24085  ovoliunlem3  24087  dyadf  24174  dyadovol  24176  dyadss  24177  dyaddisjlem  24178  dyadmaxlem  24180  opnmbllem  24184  mbfi1fseqlem1  24298  mbfi1fseqlem3  24300  mbfi1fseqlem4  24301  mbfi1fseqlem5  24302  mbfi1fseqlem6  24303  dveflem  24561  aaliou3lem9  24925  quartlem1  25422  quartlem2  25423  zetacvg  25579  lgamgulmlem4  25596  basellem1  25645  basellem2  25646  basellem3  25647  basellem4  25648  basellem5  25649  basellem6  25650  basellem7  25651  basellem8  25652  basellem9  25653  1sgm2ppw  25763  ppiublem1  25765  chtublem  25774  mersenne  25790  perfect1  25791  perfectlem1  25792  perfectlem2  25793  perfect  25794  pcbcctr  25839  bclbnd  25843  bposlem1  25847  bposlem2  25848  bposlem3  25849  bposlem4  25850  bposlem5  25851  bposlem6  25852  bposlem8  25854  lgsdir2lem2  25889  lgsqr  25914  lgsqrmodndvds  25916  gausslemma2dlem1a  25928  gausslemma2d  25937  lgseisenlem1  25938  lgseisenlem2  25939  lgseisenlem3  25940  lgseisenlem4  25941  lgsquadlem1  25943  lgsquadlem2  25944  lgsquad2lem2  25948  2lgslem1c  25956  2lgs  25970  2sqlem3  25983  2sqlem8  25989  chebbnd1lem1  26032  chebbnd1lem3  26034  logdivsum  26096  log2sumbnd  26107  pntlemd  26157  pntlema  26159  pntlemb  26160  pntlemf  26168  pntlemo  26170  ostth2lem1  26181  trkgstr  26217  ttgplusg  26651  ttgds  26654  axlowdimlem6  26720  eengstr  26753  usgrexmplef  27028  cusgrsizeindb0  27218  usgr2pthlem  27531  uspgrn2crct  27573  usgr2wspthons3  27729  clwwlkn2  27808  wwlksext2clwwlk  27821  eupth2lem3lem4  27995  frgrhash2wsp  28096  2clwwlk2clwwlk  28114  dlwwlknondlwlknonf1olem1  28128  clwlknon2num  28132  numclwlk2lem2f1o  28143  ex-xp  28200  ex-cnv  28201  ex-rn  28204  ex-mod  28213  resvplusg  30914  lmat22e11  31094  lmat22e12  31095  lmat22e21  31096  lmat22e22  31097  lmat22det  31098  oddpwdc  31620  eulerpartlemt  31637  eulerpartlemgh  31644  fib0  31665  fib1  31666  fib3  31669  chtvalz  31908  hgt750lem  31930  hgt750lemb  31935  hgt750leme  31937  problem5  32920  bcprod  32978  bj-endcomp  34620  opnmbllem0  34979  mblfinlem1  34980  dvasin  35027  areacirclem1  35031  heiborlem3  35137  heiborlem5  35139  heiborlem6  35140  heiborlem7  35141  heiborlem8  35142  heibor  35145  hlhilsplus  39122  12gcd5e1  39170  420gcd8e4  39173  12lcm5e60  39175  60lcm7e420  39177  420lcm8e840  39178  lcm2un  39181  lcmineqlem19  39214  lcmineqlem20  39215  lcmineqlem22  39217  lcmineqlem23  39218  lcmineqlem  39219  3lexlogpow5ineq2  39221  3lexlogpow5ineq3  39222  dffltz  39426  jm2.17a  39712  jm2.17b  39713  jm2.17c  39714  acongrep  39732  acongeq  39735  jm2.27a  39757  jm2.27c  39759  rmydioph  39766  rmxdioph  39768  expdiophlem2  39774  expdioph  39775  frlmpwfi  39853  amgm2d  40718  mnringaddgd  40743  hashnzfz2  40840  lhe4.4ex1a  40848  limsup10exlem  42237  wallispilem5  42534  wallispi2lem1  42536  wallispi2  42538  stirlinglem3  42541  stirlinglem8  42546  stirlinglem10  42548  stirlinglem15  42553  dirkertrigeqlem3  42565  fouriersw  42696  hoicvrrex  43018  ovnsubaddlem1  43032  ovnsubaddlem2  43033  ovnsubadd2lem  43107  ovolval5lem1  43114  ovolval5lem2  43115  elmod2  43710  fmtnoodd  43873  fmtnof1  43875  fmtnosqrt  43879  fmtnorec4  43889  257prm  43901  odz2prm2pw  43903  fmtnoprmfac1lem  43904  fmtnoprmfac1  43905  fmtnoprmfac2lem1  43906  fmtnoprmfac2  43907  fmtno4prm  43915  2pwp1prm  43929  139prmALT  43936  127prm  43939  sfprmdvdsmersenne  43944  lighneallem1  43946  lighneallem3  43948  proththdlem  43954  proththd  43955  iseven5  44005  oddprmALTV  44028  perfectALTVlem1  44062  perfectALTVlem2  44063  perfectALTV  44064  fppr2odd  44072  2exp340mod341  44074  341fppr2  44075  fpprel2  44082  nnsum3primes4  44129  nnsum3primesgbe  44133  evengpoap3  44140  nnsum4primesevenALTV  44142  bgoldbtbndlem1  44146  tgblthelfgott  44156  pw2m1lepw2m1  44751  nnpw2even  44765  logbpw2m1  44803  blenpw2  44814  nnpw2pmod  44819  blen2  44821  nnpw2p  44822  nnpw2pb  44823  blennnt2  44825  nnolog2flm1  44826  dig2nn1st  44841  0dig2pr01  44846  dig2nn0  44847  0dig2nn0e  44848  0dig2nn0o  44849  dig2bits  44850  dignn0flhalflem1  44851  dignn0ehalf  44853  dignn0flhalf  44854  nn0sumshdiglemA  44855  nn0sumshdiglemB  44856  nn0sumshdiglem1  44857  nn0sumshdiglem2  44858  nn0mullong  44861  itcovalt2lem2  44901  amgmw2d  45143
  Copyright terms: Public domain W3C validator