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

Theorem 2re 10937
Description: The number 2 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2re 2 ∈ ℝ

Proof of Theorem 2re
StepHypRef Expression
1 df-2 10926 . 2 2 = (1 + 1)
2 1re 9895 . . 3 1 ∈ ℝ
32, 2readdcli 9909 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2683 1 2 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  (class class class)co 6527  cr 9791  1c1 9793   + caddc 9795  2c2 10917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-2 10926
This theorem is referenced by:  2cn  10938  3re  10941  2ne0  10960  3pos  10961  2lt3  11042  1lt3  11043  2lt4  11045  1lt4  11046  2lt5  11049  2lt6  11054  1lt6  11055  2lt7  11060  1lt7  11061  2lt8  11067  1lt8  11068  2lt9  11075  1lt9  11076  2lt10OLD  11084  1lt10OLD  11085  1le2  11088  2rene0  11090  halfre  11093  halfgt0  11095  halflt1  11097  rehalfcl  11105  halfpos2  11108  halfnneg2  11110  addltmul  11115  nominpos  11116  avglt1  11117  avglt2  11118  div4p1lem1div2  11134  nn0lele2xi  11195  nn0n0n1ge2b  11206  nn0ge2m1nn  11207  halfnz  11287  3halfnz  11288  2lt10  11512  1lt10  11513  uzuzle23  11561  uz3m2nn  11563  2rp  11669  zgt1rpn0n1  11703  fztpval  12227  fz0to4untppr  12266  fzo0to42pr  12377  2tnp1ge0ge0  12447  flhalf  12448  fldiv4p1lem1div2  12453  fldiv4lem1div2uz2  12454  2txmodxeq0  12547  expubnd  12738  expmulnbnd  12813  nn0opthlem2  12873  faclbnd2  12895  faclbnd4lem1  12897  faclbnd5  12902  4bc2eq6  12933  hashfun  13036  hashge2el2dif  13067  hashge2el2difr  13068  wrdlenge2n0  13142  f1oun2prg  13458  2swrd2eqwrdeq  13490  sqrlem7  13783  sqrt4  13807  sqrt2gt1lt2  13809  abstri  13864  sqreulem  13893  amgm2  13903  caucvgrlem  14197  iseralt  14209  climcndslem1  14366  climcndslem2  14367  climcnds  14368  geoihalfsum  14399  efcllem  14593  ege2le3  14605  ef01bndlem  14699  cos01bnd  14701  cos2bnd  14703  cos01gt0  14706  sin02gt0  14707  sincos2sgn  14709  sin4lt0  14710  eirrlem  14717  egt2lt3  14719  epos  14720  ene1  14723  sqrt2re  14764  oexpneg  14853  mod2eq1n2dvds  14855  oddge22np1  14857  evennn02n  14858  evennn2n  14859  nn0ehalf  14879  nn0o1gt2  14881  nno  14882  nn0o  14883  nn0oddm1d2  14885  nnoddm1d2  14886  n2dvds1  14888  flodddiv4t2lthalf  14924  bitsp1o  14939  bitsfzolem  14940  bitsfzo  14941  bitsfi  14943  6gcd4e2  15039  isprm7  15204  3lcm2e6  15224  oddprm  15299  iserodd  15324  prmreclem2  15405  prmreclem6  15409  4sqlem11  15443  4sqlem12  15444  prmgaplem7  15545  2expltfac  15583  oppgtset  17551  efgredleme  17925  mgpsca  18265  mgptset  18266  mgpds  18268  matplusg  19981  chfacfscmul0  20424  chfacfpmmul0  20428  psmetge0  21869  xmetge0  21900  bl2in  21956  metnrmlem3  22403  iihalf1  22469  iihalf2  22471  pcoass  22563  tchcphlem1  22763  csbren  22907  trirn  22908  minveclem2  22922  minveclem4  22928  pjthlem1  22933  ovolunlem1a  22988  dyadss  23085  opnmbllem  23092  vitalilem2  23101  vitalilem4  23103  mbfi1fseqlem5  23209  lhop1lem  23497  aaliou3lem2  23819  aaliou3lem8  23821  pilem2  23927  pilem3  23928  pipos  23933  sinhalfpilem  23936  sincosq1lem  23970  sincosq4sgn  23974  tangtx  23978  sinq12gt0  23980  sincos4thpi  23986  tan4thpi  23987  sincos6thpi  23988  sineq0  23994  cosordlem  23998  tanord1  24004  efif1olem1  24009  efif1olem2  24010  efif1olem4  24012  efif1o  24013  efifo  24014  cxpcn3lem  24205  root1id  24212  root1eq1  24213  root1cj  24214  cxpeq  24215  logblog  24247  ang180lem1  24256  ang180lem2  24257  chordthmlem2  24277  1cubrlem  24285  atancj  24354  atantan  24367  atanbndlem  24369  atans2  24375  leibpilem1  24384  leibpi  24386  log2tlbnd  24389  log2ublem2  24391  log2ub  24393  divsqrtsumlem  24423  harmonicbnd3  24451  zetacvg  24458  lgamgulmlem2  24473  lgamgulmlem3  24474  lgamgulmlem4  24475  lgamgulmlem6  24477  lgamucov  24481  basellem1  24524  basellem2  24525  basellem3  24526  basellem5  24528  chtdif  24601  ppidif  24606  ppinncl  24617  chtrpcl  24618  ppieq0  24619  ppiltx  24620  ppiublem1  24644  ppiub  24646  chpeq0  24650  chteq0  24651  chtublem  24653  chtub  24654  chpval2  24660  chpub  24662  mersenne  24669  perfectlem1  24671  perfectlem2  24672  dchrptlem1  24706  dchrptlem2  24707  bcmono  24719  bclbnd  24722  bpos1lem  24724  bposlem1  24726  bposlem2  24727  bposlem3  24728  bposlem4  24729  bposlem5  24730  bposlem6  24731  bposlem7  24732  bposlem8  24733  bposlem9  24734  lgslem1  24739  lgsdirprm  24773  gausslemma2dlem0c  24800  gausslemma2dlem1a  24807  gausslemma2dlem2  24809  gausslemma2dlem3  24810  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgseisen  24821  lgsquadlem1  24822  lgsquadlem2  24823  m1lgs  24830  2lgslem1a1  24831  2lgslem1a2  24832  2lgslem1c  24835  2lgslem4  24848  2sqlem11  24871  chebbnd1lem1  24875  chebbnd1lem2  24876  chebbnd1lem3  24877  chebbnd1  24878  chtppilimlem1  24879  chtppilimlem2  24880  chtppilim  24881  chto1ub  24882  chebbnd2  24883  chto1lb  24884  chpchtlim  24885  chpo1ub  24886  chpo1ubb  24887  rplogsumlem1  24890  rplogsumlem2  24891  dchrisumlem2  24896  dchrisumlem3  24897  dchrvmasumiflem1  24907  dchrisum0fno1  24917  dchrisum0re  24919  dchrisum0lem1b  24921  dchrisum0lem1  24922  dchrisum0lem2  24924  rplogsum  24933  mulog2sumlem1  24940  mulog2sumlem2  24941  log2sumbnd  24950  selberglem2  24952  selbergb  24955  selberg2b  24958  chpdifbndlem1  24959  logdivbnd  24962  selberg3lem1  24963  selberg3  24965  selberg4lem1  24966  selberg4  24967  pntrmax  24970  pntrsumbnd2  24973  selberg3r  24975  selberg4r  24976  selberg34r  24977  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntrlog2bndlem6  24989  pntrlog2bnd  24990  pntpbnd1a  24991  pntpbnd1  24992  pntpbnd2  24993  pntpbnd  24994  pntibndlem2  24997  pntibndlem3  24998  pntibnd  24999  pntlemb  25003  pntlemg  25004  pntlemh  25005  pntlemr  25008  pntlemk  25012  pntlemo  25013  pnt2  25019  pnt  25020  ostth2lem1  25024  ostth3  25044  istrkg3ld  25077  tgldimor  25114  trgcgrg  25128  tgcgr4  25144  axlowdimlem6  25545  axlowdimlem16  25555  axlowdimlem17  25556  axlowdim  25559  umgrafi  25617  usisuslgra  25660  usgraex2elv  25692  usgraexmpldifpr  25694  constr3lem4  25941  constr3trllem3  25946  constr3pthlem1  25949  constr3pthlem3  25951  wwlkextwrd  26022  wwlkextfun  26023  wwlkextinj  26024  wwlkm1edg  26029  wwlkextproplem3  26037  clwwlkgt0  26065  clwwlkn0  26068  clwlkisclwwlklem2a1  26073  clwlkisclwwlklem2a2  26074  clwlkisclwwlklem2fv1  26076  clwlkisclwwlklem2fv2  26077  clwlkisclwwlklem2a4  26078  clwlkisclwwlklem2a  26079  clwlkisclwwlklem1  26081  clwlkisclwwlk2  26084  clwwlkext2edg  26096  usg2cwwkdifex  26115  clwlkfclwwlk  26137  konigsberg  26280  vdgfrgragt2  26320  extwwlkfablem2  26371  numclwwlkovf2ex  26379  frgrareggt1  26409  frgrareg  26410  frgraregord013  26411  ex-pss  26443  ex-res  26456  ex-fv  26458  ex-fl  26462  ex-mod  26464  ex-abs  26470  nvge0  26707  ipidsq  26753  minvecolem2  26921  minvecolem4  26926  normlem7  27163  norm-ii-i  27184  norm3lemt  27199  normpar2i  27203  bcsiALT  27226  pjhthlem1  27440  opsqrlem6  28194  cdj3lem1  28483  addltmulALT  28495  oppgle  28790  resvplusg  28970  sqsscirc1  29088  nexple  29205  dya2iocucvr  29479  omssubadd  29495  oddpwdc  29549  eulerpartlemgc  29557  fibp1  29596  coinfliplem  29673  coinflipspace  29675  ballotlem2  29683  signstfveq0  29786  subfacp1lem1  30221  subfacp1lem5  30226  subfacval3  30231  problem2  30619  problem2OLD  30620  problem5  30623  circum  30628  nn0prpwlem  31293  dnibndlem10  31453  knoppcnlem2  31460  knoppcnlem4  31462  knoppcnlem10  31468  unbdqndv2lem1  31476  knoppndvlem1  31479  knoppndvlem10  31488  knoppndvlem11  31489  knoppndvlem12  31490  knoppndvlem14  31492  knoppndvlem15  31493  knoppndvlem17  31495  knoppndvlem18  31496  knoppndvlem19  31497  knoppndvlem20  31498  knoppndvlem21  31499  cnndvlem1  31504  taupi  32149  relowlpssretop  32191  sin2h  32372  cos2h  32373  tan2h  32374  poimirlem7  32389  poimirlem9  32391  opnmbllem0  32418  mblfinlem1  32419  mblfinlem2  32420  itg2addnclem  32434  isbnd2  32555  isbnd3  32556  heiborlem7  32589  rabren3dioph  36200  pellexlem2  36215  pellexlem5  36218  pell14qrgapw  36261  pellfundex  36271  rmspecsqrtnq  36291  rmspecsqrtnqOLD  36292  jm2.24nn  36347  jm2.17a  36348  jm2.17b  36349  jm2.17c  36350  acongrep  36368  acongeq  36371  jm2.22  36383  jm2.23  36384  jm2.20nn  36385  jm3.1lem2  36406  expdiophlem1  36409  imo72b2lem0  37290  lhe4.4ex1a  37353  isosctrlem1ALT  37995  sineq0ALT  37998  lt3addmuld  38259  suplesup  38300  infleinflem2  38332  infleinf  38333  sumnnodd  38501  0ellimcdiv  38520  sinaover2ne0  38555  stoweidlem13  38710  stoweidlem14  38711  stoweidlem26  38723  stoweidlem49  38746  stoweidlem52  38749  wallispilem4  38765  wallispilem5  38766  wallispi  38767  wallispi2lem1  38768  wallispi2lem2  38769  wallispi2  38770  stirlinglem1  38771  stirlinglem3  38773  stirlinglem5  38775  stirlinglem6  38776  stirlinglem7  38777  stirlinglem10  38780  stirlinglem11  38781  stirlinglem15  38785  stirlingr  38787  dirker2re  38789  dirkerval2  38791  dirkerre  38792  dirkerper  38793  dirkertrigeqlem1  38795  dirkertrigeqlem3  38797  dirkercncflem1  38800  dirkercncflem2  38801  dirkercncflem4  38803  fourierdlem24  38828  fourierdlem43  38847  fourierdlem44  38848  fourierdlem57  38860  fourierdlem58  38861  fourierdlem62  38865  fourierdlem66  38869  fourierdlem68  38871  fourierdlem72  38875  fourierdlem76  38879  fourierdlem78  38881  fourierdlem79  38882  fourierdlem94  38897  fourierdlem103  38906  fourierdlem104  38907  fourierdlem111  38914  fourierdlem113  38916  sqwvfoura  38925  sqwvfourb  38926  fourierswlem  38927  fouriersw  38928  etransclem23  38954  salexct2  39037  salexct3  39040  salgencntex  39041  salgensscntex  39042  sge0ad2en  39128  ovnsubaddlem1  39264  smfmullem4  39483  smf2id  39490  fmtnoge3  39785  fmtnof1  39790  fmtnoprmfac2lem1  39821  fmtno4prmfac  39827  fmtno4prm  39830  2pwp1prm  39846  31prm  39855  sfprmdvdsmersenne  39863  lighneallem2  39866  lighneallem4a  39868  lighneallem4b  39869  dfodd4  39914  oexpnegALTV  39931  nn0o1gt2ALTV  39948  nnoALTV  39949  nn0oALTV  39950  nn0e  39951  perfectALTVlem1  39969  perfectALTVlem2  39970  gbogt5  39989  sgoldbalt  40008  nnsum3primes4  40009  nnsum3primesgbe  40013  nnsum3primesle9  40015  nnsum4primesodd  40017  nnsum4primesoddALTV  40018  wtgoldbnnsum4prm  40023  bgoldbnnsum3prm  40025  pfx2  40080  2leaddle2  40171  p1lep2  40173  xnn0n0n1ge2b  40218  upgrfi  40319  umgrupgr  40330  umgrislfupgrlem  40349  umgrislfupgr  40350  lfgrnloop  40352  upgredg  40372  usgruspgr  40410  usgrislfuspgr  40416  lfuhgr1v0e  40482  nbusgrvtxm1  40609  vdegp1bi-av  40755  upgrewlkle2  40810  lfgrwlkprop  40898  upgr2pthnlp  40940  usgr2pthlem  40971  pthdlem1  40974  wwlksm1edg  41080  wwlksnextwrd  41105  wwlksnextfun  41106  wwlksnextinj  41107  wwlksnextproplem3  41119  clwlkclwwlklem2a1  41203  clwlkclwwlklem2a2  41204  clwlkclwwlklem2fv1  41206  clwlkclwwlklem2fv2  41207  clwlkclwwlklem2a4  41208  clwlkclwwlklem2a  41209  clwlkclwwlklem2  41211  clwlkclwwlk2  41214  clwwlksext2edg  41232  clwlksfclwwlk  41271  konigsbergiedgw  41418  konigsbergiedgwOLD  41419  konigsbergssiedgw  41421  konigsberglem1  41424  konigsberglem2  41425  konigsberglem3  41426  konigsberg-av  41429  frgrwopreglem2  41484  av-extwwlkfablem2  41512  av-numclwwlkovf2ex  41519  av-frgrareggt1  41549  plusgndxnmulrndx  41745  cznnring  41750  nn0le2is012  41940  ply1mulgsumlem2  41971  zlmodzxznm  42082  zlmodzxzldeplem  42083  difmodm1lt  42113  nn0eo  42118  flnn0div2ge  42123  rege1logbzge0  42153  fldivexpfllog2  42159  logbpw2m1  42161  fllog2  42162  blenpw2m1  42173  nnpw2blen  42174  nnolog2flm1  42184  blennngt2o2  42186  dig2nn1st  42199  dig2nn0  42205  dig2bits  42208  dignn0flhalflem1  42209  dignn0flhalflem2  42210  dignn0flhalf  42212  nn0sumshdiglemA  42213
  Copyright terms: Public domain W3C validator