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

Theorem 2re 11700
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 11689 . 2 2 = (1 + 1)
2 1re 10630 . . 3 1 ∈ ℝ
32, 2readdcli 10645 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2909 1 2 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  (class class class)co 7145  cr 10525  1c1 10527   + caddc 10529  2c2 11681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148  df-2 11689
This theorem is referenced by:  2cnALT  11702  3re  11706  2ne0  11730  3pos  11731  2lt3  11798  1lt3  11799  2lt4  11801  1lt4  11802  2lt5  11805  2lt6  11810  1lt6  11811  2lt7  11816  1lt7  11817  2lt8  11823  1lt8  11824  2lt9  11831  1lt9  11832  1le2  11835  2rene0  11837  halfre  11840  halfgt0  11842  halflt1  11844  rehalfcl  11852  halfpos2  11855  halfnneg2  11857  addltmul  11862  nominpos  11863  avglt1  11864  avglt2  11865  div4p1lem1div2  11881  nn0lele2xi  11941  nn0n0n1ge2b  11952  nn0ge2m1nn  11953  nn0le2is012  12035  halfnz  12049  3halfnz  12050  2lt10  12225  1lt10  12226  eluz4eluz2  12274  uzuzle23  12278  uz3m2nn  12280  2rp  12384  xnn0n0n1ge2b  12516  fztpval  12959  fz0to4untppr  13000  fzo0to42pr  13114  flhalf  13190  fldiv4p1lem1div2  13195  2txmodxeq0  13289  expubnd  13531  expmulnbnd  13586  nn0opthlem2  13619  faclbnd2  13641  faclbnd4lem1  13643  faclbnd5  13648  4bc2eq6  13679  hashgt23el  13775  hashfun  13788  hashge2el2dif  13828  hashge2el2difr  13829  wrdlenge2n0  13894  f1oun2prg  14269  sqrlem7  14598  sqrt4  14622  sqrt2gt1lt2  14624  abstri  14680  sqreulem  14709  amgm2  14719  caucvgrlem  15019  climcndslem1  15194  climcndslem2  15195  climcnds  15196  efcllem  15421  ege2le3  15433  ef01bndlem  15527  cos01bnd  15529  cos2bnd  15531  cos01gt0  15534  sin02gt0  15535  sincos2sgn  15537  sin4lt0  15538  eirrlem  15547  egt2lt3  15549  epos  15550  ene1  15553  sqrt2re  15593  mod2eq1n2dvds  15686  oddge22np1  15688  evennn2n  15690  n2dvds1OLD  15708  nn0o1gt2  15722  nno  15723  nn0o  15724  nnoddm1d2  15727  bitsp1o  15772  bitsfzolem  15773  bitsfzo  15774  bitsfi  15776  6gcd4e2  15876  2mulprm  16027  ge2nprmge4  16035  isprm7  16042  3lcm2e6  16062  prmreclem2  16243  prmreclem6  16247  4sqlem11  16281  4sqlem12  16282  prmgaplem7  16383  2expltfac  16416  plusgndxnmulrndx  16607  oppgtset  18420  efgredleme  18800  mgpsca  19177  mgptset  19178  mgpds  19180  rmodislmod  19633  cnfldfun  20487  zringndrg  20567  chfacfscmul0  21396  chfacfpmmul0  21400  psmetge0  22851  xmetge0  22883  bl2in  22939  metnrmlem3  23398  iihalf1  23464  iihalf2  23466  pcoass  23557  tcphcphlem1  23767  csbren  23931  trirn  23932  minveclem2  23958  minveclem4  23964  pjthlem1  23969  ovolunlem1a  24026  dyadss  24124  opnmbllem  24131  vitalilem2  24139  vitalilem4  24141  mbfi1fseqlem5  24249  lhop1lem  24539  aaliou3lem2  24861  aaliou3lem8  24863  pilem2  24969  pilem3  24970  pipos  24975  sinhalfpilem  24978  sincosq1lem  25012  sincosq4sgn  25016  tangtx  25020  sinq12gt0  25022  sincos4thpi  25028  tan4thpi  25029  sincos6thpi  25030  sineq0  25038  cosordlem  25042  tanord1  25048  efif1olem1  25053  efif1olem2  25054  efif1olem4  25056  efif1o  25057  efifo  25058  2irrexpq  25240  cxpcn3lem  25255  root1id  25262  root1eq1  25263  root1cj  25264  cxpeq  25265  2logb9irr  25300  2logb3irr  25302  ang180lem1  25314  ang180lem2  25315  chordthmlem2  25338  1cubrlem  25346  atancj  25415  atantan  25428  atanbndlem  25430  atans2  25436  leibpilem1OLD  25446  leibpi  25448  log2tlbnd  25451  log2ublem2  25453  log2ub  25455  divsqrtsumlem  25485  harmonicbnd3  25513  zetacvg  25520  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem4  25537  lgamgulmlem6  25539  lgamucov  25543  basellem1  25586  basellem2  25587  basellem3  25588  basellem5  25590  chtdif  25663  ppidif  25668  ppinncl  25679  chtrpcl  25680  ppieq0  25681  ppiltx  25682  ppiublem1  25706  ppiub  25708  chpeq0  25712  chteq0  25713  chtublem  25715  chtub  25716  chpval2  25722  chpub  25724  mersenne  25731  perfectlem1  25733  perfectlem2  25734  dchrptlem1  25768  dchrptlem2  25769  bcmono  25781  bclbnd  25784  bpos1lem  25786  bposlem1  25788  bposlem2  25789  bposlem3  25790  bposlem4  25791  bposlem5  25792  bposlem6  25793  bposlem7  25794  bposlem8  25795  bposlem9  25796  lgslem1  25801  lgsdirprm  25835  gausslemma2dlem0c  25862  gausslemma2dlem1a  25869  gausslemma2dlem2  25871  gausslemma2dlem3  25872  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgseisen  25883  lgsquadlem1  25884  lgsquadlem2  25885  m1lgs  25892  2lgslem1a1  25893  2lgslem1a2  25894  2lgslem1c  25897  2lgslem4  25910  2sqlem11  25933  2sq2  25937  2sqreultlem  25951  2sqreunnltlem  25954  chebbnd1lem1  25973  chebbnd1lem2  25974  chebbnd1lem3  25975  chebbnd1  25976  chtppilimlem1  25977  chtppilimlem2  25978  chtppilim  25979  chto1ub  25980  chebbnd2  25981  chto1lb  25982  chpchtlim  25983  chpo1ub  25984  chpo1ubb  25985  rplogsumlem1  25988  rplogsumlem2  25989  dchrisumlem2  25994  dchrisumlem3  25995  dchrvmasumiflem1  26005  dchrisum0fno1  26015  dchrisum0re  26017  dchrisum0lem1b  26019  dchrisum0lem1  26020  dchrisum0lem2  26022  rplogsum  26031  mulog2sumlem1  26038  mulog2sumlem2  26039  log2sumbnd  26048  selberglem2  26050  selbergb  26053  selberg2b  26056  chpdifbndlem1  26057  logdivbnd  26060  selberg3lem1  26061  selberg3  26063  selberg4lem1  26064  selberg4  26065  pntrmax  26068  pntrsumbnd2  26071  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntrlog2bnd  26088  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  pntpbnd  26092  pntibndlem2  26095  pntibndlem3  26096  pntibnd  26097  pntlemb  26101  pntlemg  26102  pntlemh  26103  pntlemr  26106  pntlemk  26110  pntlemo  26111  pnt2  26117  pnt  26118  ostth2lem1  26122  ostth3  26142  istrkg3ld  26175  tgldimor  26216  trgcgrg  26229  tgcgr4  26245  axlowdimlem6  26661  axlowdimlem16  26671  axlowdimlem17  26672  axlowdim  26675  upgrfi  26804  umgrupgr  26816  umgrislfupgrlem  26835  umgrislfupgr  26836  lfgrnloop  26838  usgruspgr  26891  usgrislfuspgr  26897  lfuhgr1v0e  26964  usgrexmpldifpr  26968  usgrexmplef  26969  nbusgrvtxm1  27089  vdegp1bi  27247  upgrewlkle2  27316  lfgrwlkprop  27397  upgr2pthnlp  27441  usgr2pthlem  27472  pthdlem1  27475  wwlksm1edg  27587  wwlksnextwrd  27603  wwlksnextfun  27604  wwlksnextinj  27605  wwlksnextproplem3  27618  clwlkclwwlklem2a1  27698  clwlkclwwlklem2a2  27699  clwlkclwwlklem2fv1  27701  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwlkclwwlk2  27709  clwlkclwwlkf  27714  clwwlkext2edg  27763  konigsbergiedgw  27955  konigsbergssiedgw  27957  konigsberglem1  27959  konigsberglem2  27960  konigsberglem3  27961  konigsberg  27964  frgrreggt1  28100  ex-pss  28135  ex-res  28148  ex-fv  28150  ex-fl  28154  ex-mod  28156  ex-abs  28162  ipidsq  28415  minvecolem2  28580  minvecolem4  28585  normlem7  28821  norm-ii-i  28842  norm3lemt  28857  normpar2i  28861  bcsiALT  28884  pjhthlem1  29096  opsqrlem6  29850  cdj3lem1  30139  addltmulALT  30151  threehalves  30519  pfx1s2  30543  wrdt2ind  30555  oppgle  30568  cyc3conja  30727  resvplusg  30834  sqsscirc1  31051  nexple  31168  dya2iocucvr  31442  omssubadd  31458  oddpwdc  31512  eulerpartlemgc  31520  fibp1  31559  coinfliplem  31636  coinflipspace  31638  ballotlem2  31646  signstfveq0  31747  prodfzo03  31774  hgt750lemd  31819  logdivsqrle  31821  hgt750lem  31822  hgt750lem2  31823  hgt750leme  31829  lfuhgr2  32263  usgrcyclgt2v  32276  acycgr2v  32295  subfacp1lem1  32324  subfacp1lem5  32329  subfacval3  32334  problem2  32807  problem5  32810  circum  32815  nn0prpwlem  33568  dnibndlem10  33724  knoppcnlem2  33731  knoppcnlem4  33733  knoppcnlem10  33739  unbdqndv2lem1  33746  knoppndvlem1  33749  knoppndvlem10  33758  knoppndvlem11  33759  knoppndvlem12  33760  knoppndvlem14  33762  knoppndvlem15  33763  knoppndvlem17  33765  knoppndvlem18  33766  knoppndvlem19  33767  knoppndvlem20  33768  knoppndvlem21  33769  cnndvlem1  33774  taupi  34487  relowlpssretop  34528  sin2h  34764  cos2h  34765  tan2h  34766  poimirlem7  34781  poimirlem9  34783  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  itg2addnclem  34825  isbnd2  34944  isbnd3  34945  heiborlem7  34978  oexpreposd  39059  remul02  39115  sn-0ne2  39116  remul01  39117  rabren3dioph  39292  pellexlem2  39307  pellexlem5  39310  pell14qrgapw  39353  pellfundex  39363  rmspecsqrtnq  39383  jm2.24nn  39436  jm2.17a  39437  jm2.17b  39438  jm2.17c  39439  acongrep  39457  acongeq  39460  jm2.22  39472  jm2.23  39473  jm2.20nn  39474  jm3.1lem2  39495  expdiophlem1  39498  imo72b2lem0  40396  lhe4.4ex1a  40541  isosctrlem1ALT  41148  sineq0ALT  41151  lt3addmuld  41448  suplesup  41487  infleinflem2  41519  infleinf  41520  sumnnodd  41791  0ellimcdiv  41810  sinaover2ne0  42029  stoweidlem13  42179  stoweidlem14  42180  stoweidlem26  42192  stoweidlem49  42215  stoweidlem52  42218  wallispilem4  42234  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  wallispi2lem2  42238  wallispi2  42239  stirlinglem1  42240  stirlinglem3  42242  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem10  42249  stirlinglem11  42250  stirlinglem15  42254  stirlingr  42256  dirker2re  42258  dirkerval2  42260  dirkerre  42261  dirkerper  42262  dirkertrigeqlem1  42264  dirkertrigeqlem3  42266  dirkercncflem1  42269  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem24  42297  fourierdlem43  42316  fourierdlem44  42317  fourierdlem57  42329  fourierdlem58  42330  fourierdlem62  42334  fourierdlem66  42338  fourierdlem68  42340  fourierdlem72  42344  fourierdlem76  42348  fourierdlem78  42350  fourierdlem79  42351  fourierdlem94  42366  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem113  42385  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  etransclem23  42423  salexct2  42503  salexct3  42506  salgencntex  42507  salgensscntex  42508  sge0ad2en  42594  ovnsubaddlem1  42733  smfmullem4  42950  smf2id  42957  2leaddle2  43379  p1lep2  43381  fmtnoge3  43539  fmtnof1  43544  fmtnoprmfac2lem1  43575  fmtno4prmfac  43581  fmtno4prm  43584  2pwp1prm  43598  31prm  43607  sfprmdvdsmersenne  43615  lighneallem2  43618  lighneallem4a  43620  lighneallem4b  43621  requad01  43633  requad1  43634  requad2  43635  dfodd4  43671  nn0o1gt2ALTV  43706  nnoALTV  43707  nn0oALTV  43708  nn0e  43709  nneven  43710  perfectALTVlem1  43733  perfectALTVlem2  43734  341fppr2  43746  9fppr8  43749  fpprel2  43753  nfermltl2rev  43755  gbowgt5  43774  sbgoldbalt  43793  sgoldbeven3prm  43795  mogoldbb  43797  nnsum3primes4  43800  nnsum3primesgbe  43804  nnsum3primesle9  43806  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  wtgoldbnnsum4prm  43814  bgoldbnnsum3prm  43816  cznnring  44125  ply1mulgsumlem2  44339  zlmodzxznm  44450  zlmodzxzldeplem  44451  difmodm1lt  44480  nn0eo  44486  flnn0div2ge  44491  rege1logbzge0  44517  fldivexpfllog2  44523  logbpw2m1  44525  fllog2  44526  blenpw2m1  44537  nnpw2blen  44538  nnolog2flm1  44548  blennngt2o2  44550  dig2nn1st  44563  dig2nn0  44569  dig2bits  44572  dignn0flhalflem1  44573  dignn0flhalflem2  44574  dignn0flhalf  44576  nn0sumshdiglemA  44577  rrx2xpref1o  44603  itscnhlc0yqe  44644  itsclquadb  44661  2itscp  44666  itscnhlinecirc02p  44670
  Copyright terms: Public domain W3C validator