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

Theorem 2nn 10795
Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
Assertion
Ref Expression
2nn  |-  2  e.  NN

Proof of Theorem 2nn
StepHypRef Expression
1 df-2 10695 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10647 . . 3  |-  1  e.  NN
3 peano2nn 10648 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2535 1  |-  2  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1897  (class class class)co 6314   1c1 9565    + caddc 9567   NNcn 10636   2c2 10686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-1cn 9622
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-ov 6317  df-om 6719  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-nn 10637  df-2 10695
This theorem is referenced by:  3nn  10796  2nn0  10914  2z  10997  uz3m2nn  11229  ige2m1fz1  11911  sqeq0  12370  expmulnbnd  12435  sqeq0d  12446  faclbnd5  12514  bcn2  12535  f1oun2prg  13047  wrdl2exs2  13070  wwlktovf  13079  climcndslem1  13955  climcndslem2  13956  climcnds  13957  harmonic  13965  geo2sum  13977  geo2lim  13979  ege2le3  14192  ef01bndlem  14286  egt2lt3  14306  nthruc  14351  bits0o  14451  bitsp1  14452  bitsfzolem  14455  bitsfzolemOLD  14456  bitsfzo  14457  bitsmod  14458  bitsfi  14459  bitscmp  14460  bitsinv1lem  14463  bitsinv1  14464  2ebits  14469  bitsinvp1  14471  sadcaddlem  14479  sadadd3  14483  sadaddlem  14488  sadasslem  14492  bitsres  14495  bitsuz  14496  bitsshft  14497  smumullem  14514  smumul  14515  sqgcd  14574  3lcm2e6woprm  14628  3prm  14689  3lcm2e6  14729  pythagtriplem4  14817  iserodd  14833  prmreclem3  14910  prmreclem5  14912  prmreclem6  14913  4sqlem12  14948  vdwlem3  14981  vdwlem9  14987  vdwlem10  14988  prmo2  15046  dec2dvds  15083  dec5nprm  15086  dec2nprm  15087  2expltfac  15111  4nprm  15124  5prm  15128  6nprm  15129  7prm  15130  8nprm  15131  10nprm  15133  11prm  15134  17prm  15136  23prm  15138  37prm  15140  43prm  15141  83prm  15142  139prm  15143  163prm  15144  317prm  15145  631prm  15146  1259lem1  15150  1259lem2  15151  1259lem3  15152  1259lem4  15153  1259lem5  15154  1259prm  15155  2503lem1  15156  2503lem2  15157  2503lem3  15158  2503prm  15159  4001lem1  15160  4001lem2  15161  4001lem3  15162  4001lem4  15163  4001prm  15164  plusgndx  15272  plusgid  15273  grpstr  15284  grpbase  15285  grpplusg  15286  ressplusg  15287  rngstr  15292  lmodstr  15309  topgrpstr  15334  dsndx  15348  dsid  15349  odrngstr  15352  ressds  15359  imasvalstr  15398  pmtrprfvalrn  17177  psgnunilem2  17184  psgnprfval  17210  psgnprfval1  17211  mgpds  17781  oppradd  17906  sraaddg  18450  srads  18457  opsrplusg  18751  cnfldstr  19020  zlmplusg  19138  znadd  19159  m2detleiblem1  19697  m2detleiblem5  19698  m2detleiblem6  19699  m2detleiblem3  19702  m2detleiblem4  19703  m2detleib  19704  tmslem  21545  tngplusg  21698  ovollb2lem  22489  ovolunlem1a  22497  ovolunlem1  22498  ovoliunlem1  22503  ovoliunlem3  22505  dyadf  22597  dyadovol  22599  dyadss  22600  dyaddisjlem  22601  dyadmaxlem  22603  opnmbllem  22607  mbfi1fseqlem1  22721  mbfi1fseqlem3  22723  mbfi1fseqlem4  22724  mbfi1fseqlem5  22725  mbfi1fseqlem6  22726  dveflem  22979  aaliou3lem9  23354  dcubic1lem  23817  dcubic2  23818  mcubic  23821  quartlem1  23831  quartlem2  23832  zetacvg  23988  lgamgulmlem4  24005  basellem1  24055  basellem2  24056  basellem3  24057  basellem4  24058  basellem5  24059  basellem6  24060  basellem7  24061  basellem8  24062  basellem9  24063  1sgm2ppw  24176  ppiublem1  24178  chtublem  24187  mersenne  24203  perfect1  24204  perfectlem1  24205  perfectlem2  24206  perfect  24207  pcbcctr  24252  bclbnd  24256  bposlem1  24260  bposlem2  24261  bposlem3  24262  bposlem4  24263  bposlem5  24264  bposlem6  24265  bposlem8  24267  lgsdir2lem2  24300  lgsqr  24322  lgseisenlem1  24325  lgseisenlem2  24326  lgseisenlem3  24327  lgseisenlem4  24328  lgsquadlem1  24330  lgsquadlem2  24331  lgsquad2lem2  24335  2sqlem3  24342  2sqlem8  24348  chebbnd1lem1  24355  chebbnd1lem3  24357  logdivsum  24419  log2sumbnd  24430  pntlemd  24480  pntlema  24482  pntlemb  24483  pntlemf  24491  pntlemo  24493  ostth2lem1  24504  trkgstr  24540  ttgplusg  24956  ttgds  24959  axlowdimlem6  25025  eengstr  25058  usgraexmplef  25176  cusgrasizeindb0  25246  usgrcyclnl2  25417  eupath2lem3  25755  konigsberg  25763  ex-xp  25934  ex-cnv  25935  ex-rn  25938  resvplusg  28644  lmat22e11  28692  lmat22e12  28693  lmat22e21  28694  lmat22e22  28695  lmat22det  28696  oddpwdc  29235  eulerpartlemt  29252  eulerpartlemgh  29259  fib0  29280  fib1  29281  fib3  29284  problem5  30349  bcprod  30422  opnmbllem0  32020  mblfinlem1  32021  dvasin  32072  areacirclem1  32076  heiborlem3  32189  heiborlem5  32191  heiborlem6  32192  heiborlem7  32193  heiborlem8  32194  heibor  32197  hlhilsplus  35555  jm2.17a  35854  jm2.17b  35855  jm2.17c  35856  acongrep  35874  acongeq  35877  jm2.27a  35904  jm2.27c  35906  rmydioph  35913  rmxdioph  35915  expdiophlem2  35921  expdioph  35922  frlmpwfi  36000  amgm2d  36693  hashnzfz2  36713  lhe4.4ex1a  36721  wallispilem5  37968  wallispi2lem1  37970  wallispi2  37972  stirlinglem3  37975  stirlinglem8  37980  stirlinglem10  37982  stirlinglem15  37987  dirkertrigeqlem3  37999  fouriersw  38132  hoicvrrex  38415  ovnsubaddlem1  38429  ovnsubaddlem2  38430  elmod2  38761  iseven5  38831  oddprmALTV  38853  perfectALTVlem1  38880  perfectALTVlem2  38881  perfectALTV  38882  nnsum3primes4  38920  nnsum3primesgbe  38924  nnsum4primesevenALTV  38933  bgoldbtbndlem1  38937  tgblthelfgott  38945  proththdlem  38950  proththd  38951  pfx2  38992  cusgrsizeindb0  39559  uspgrn2crct  39825  usgra2pthspth  39937  usgra2pthlem1  39939  pw2m1lepw2m1  40590  nnpw2even  40608  logbpw2m1  40650  blenpw2  40661  nnpw2pmod  40666  blen2  40668  nnpw2p  40669  nnpw2pb  40670  blennnt2  40672  nnolog2flm1  40673  dig2nn1st  40688  0dig2pr01  40693  dig2nn0  40694  0dig2nn0e  40695  0dig2nn0o  40696  dig2bits  40697  dignn0flhalflem1  40698  dignn0ehalf  40700  dignn0flhalf  40701  nn0sumshdiglemA  40702  nn0sumshdiglemB  40703  nn0sumshdiglem1  40704  nn0sumshdiglem2  40705  nn0mullong  40708
  Copyright terms: Public domain W3C validator