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

Theorem 2re 11035
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 11024 . 2 2 = (1 + 1)
2 1re 9984 . . 3 1 ∈ ℝ
32, 2readdcli 9998 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2700 1 2 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1992  (class class class)co 6605  cr 9880  1c1 9882   + caddc 9884  2c2 11015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-i2m1 9949  ax-1ne0 9950  ax-rrecex 9953  ax-cnre 9954
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608  df-2 11024
This theorem is referenced by:  2cn  11036  3re  11039  2ne0  11058  3pos  11059  2lt3  11140  1lt3  11141  2lt4  11143  1lt4  11144  2lt5  11147  2lt6  11152  1lt6  11153  2lt7  11158  1lt7  11159  2lt8  11165  1lt8  11166  2lt9  11173  1lt9  11174  2lt10OLD  11182  1lt10OLD  11183  1le2  11186  2rene0  11188  halfre  11191  halfgt0  11193  halflt1  11195  rehalfcl  11203  halfpos2  11206  halfnneg2  11208  addltmul  11213  nominpos  11214  avglt1  11215  avglt2  11216  div4p1lem1div2  11232  nn0lele2xi  11293  nn0n0n1ge2b  11304  nn0ge2m1nn  11305  halfnz  11399  3halfnz  11400  2lt10  11624  1lt10  11625  uzuzle23  11673  uz3m2nn  11675  2rp  11781  zgt1rpn0n1  11815  xnn0n0n1ge2b  11909  fztpval  12341  fz0to4untppr  12380  fzo0to42pr  12493  2tnp1ge0ge0  12567  flhalf  12568  fldiv4p1lem1div2  12573  fldiv4lem1div2uz2  12574  2txmodxeq0  12667  expubnd  12858  expmulnbnd  12933  nn0opthlem2  12993  faclbnd2  13015  faclbnd4lem1  13017  faclbnd5  13022  4bc2eq6  13053  hashfun  13161  hashge2el2dif  13195  hashge2el2difr  13196  wrdlenge2n0  13275  f1oun2prg  13593  2swrd2eqwrdeq  13625  sqrlem7  13918  sqrt4  13942  sqrt2gt1lt2  13944  abstri  13999  sqreulem  14028  amgm2  14038  caucvgrlem  14332  iseralt  14344  climcndslem1  14501  climcndslem2  14502  climcnds  14503  geoihalfsum  14534  efcllem  14728  ege2le3  14740  ef01bndlem  14834  cos01bnd  14836  cos2bnd  14838  cos01gt0  14841  sin02gt0  14842  sincos2sgn  14844  sin4lt0  14845  eirrlem  14852  egt2lt3  14854  epos  14855  ene1  14858  sqrt2re  14899  oexpneg  14988  mod2eq1n2dvds  14990  oddge22np1  14992  evennn02n  14993  evennn2n  14994  nn0ehalf  15014  nn0o1gt2  15016  nno  15017  nn0o  15018  nn0oddm1d2  15020  nnoddm1d2  15021  n2dvds1  15023  flodddiv4t2lthalf  15059  bitsp1o  15074  bitsfzolem  15075  bitsfzo  15076  bitsfi  15078  6gcd4e2  15174  isprm7  15339  3lcm2e6  15359  oddprm  15434  iserodd  15459  prmreclem2  15540  prmreclem6  15544  4sqlem11  15578  4sqlem12  15579  prmgaplem7  15680  2expltfac  15718  plusgndxnmulrndx  15914  oppgtset  17698  efgredleme  18072  mgpsca  18412  mgptset  18413  mgpds  18415  cnfldfun  19672  zringndrg  19752  matplusg  20134  chfacfscmul0  20577  chfacfpmmul0  20581  psmetge0  22022  xmetge0  22054  bl2in  22110  metnrmlem3  22567  iihalf1  22633  iihalf2  22635  pcoass  22727  tchcphlem1  22937  csbren  23085  trirn  23086  minveclem2  23100  minveclem4  23106  pjthlem1  23111  ovolunlem1a  23166  dyadss  23263  opnmbllem  23270  vitalilem2  23279  vitalilem4  23281  mbfi1fseqlem5  23387  lhop1lem  23675  aaliou3lem2  23997  aaliou3lem8  23999  pilem2  24105  pilem3  24106  pipos  24111  sinhalfpilem  24114  sincosq1lem  24148  sincosq4sgn  24152  tangtx  24156  sinq12gt0  24158  sincos4thpi  24164  tan4thpi  24165  sincos6thpi  24166  sineq0  24172  cosordlem  24176  tanord1  24182  efif1olem1  24187  efif1olem2  24188  efif1olem4  24190  efif1o  24191  efifo  24192  cxpcn3lem  24383  root1id  24390  root1eq1  24391  root1cj  24392  cxpeq  24393  logblog  24425  ang180lem1  24434  ang180lem2  24435  chordthmlem2  24455  1cubrlem  24463  atancj  24532  atantan  24545  atanbndlem  24547  atans2  24553  leibpilem1  24562  leibpi  24564  log2tlbnd  24567  log2ublem2  24569  log2ub  24571  divsqrtsumlem  24601  harmonicbnd3  24629  zetacvg  24636  lgamgulmlem2  24651  lgamgulmlem3  24652  lgamgulmlem4  24653  lgamgulmlem6  24655  lgamucov  24659  basellem1  24702  basellem2  24703  basellem3  24704  basellem5  24706  chtdif  24779  ppidif  24784  ppinncl  24795  chtrpcl  24796  ppieq0  24797  ppiltx  24798  ppiublem1  24822  ppiub  24824  chpeq0  24828  chteq0  24829  chtublem  24831  chtub  24832  chpval2  24838  chpub  24840  mersenne  24847  perfectlem1  24849  perfectlem2  24850  dchrptlem1  24884  dchrptlem2  24885  bcmono  24897  bclbnd  24900  bpos1lem  24902  bposlem1  24904  bposlem2  24905  bposlem3  24906  bposlem4  24907  bposlem5  24908  bposlem6  24909  bposlem7  24910  bposlem8  24911  bposlem9  24912  lgslem1  24917  lgsdirprm  24951  gausslemma2dlem0c  24978  gausslemma2dlem1a  24985  gausslemma2dlem2  24987  gausslemma2dlem3  24988  lgseisenlem1  24995  lgseisenlem2  24996  lgseisenlem3  24997  lgseisen  24999  lgsquadlem1  25000  lgsquadlem2  25001  m1lgs  25008  2lgslem1a1  25009  2lgslem1a2  25010  2lgslem1c  25013  2lgslem4  25026  2sqlem11  25049  chebbnd1lem1  25053  chebbnd1lem2  25054  chebbnd1lem3  25055  chebbnd1  25056  chtppilimlem1  25057  chtppilimlem2  25058  chtppilim  25059  chto1ub  25060  chebbnd2  25061  chto1lb  25062  chpchtlim  25063  chpo1ub  25064  chpo1ubb  25065  rplogsumlem1  25068  rplogsumlem2  25069  dchrisumlem2  25074  dchrisumlem3  25075  dchrvmasumiflem1  25085  dchrisum0fno1  25095  dchrisum0re  25097  dchrisum0lem1b  25099  dchrisum0lem1  25100  dchrisum0lem2  25102  rplogsum  25111  mulog2sumlem1  25118  mulog2sumlem2  25119  log2sumbnd  25128  selberglem2  25130  selbergb  25133  selberg2b  25136  chpdifbndlem1  25137  logdivbnd  25140  selberg3lem1  25141  selberg3  25143  selberg4lem1  25144  selberg4  25145  pntrmax  25148  pntrsumbnd2  25151  selberg3r  25153  selberg4r  25154  selberg34r  25155  pntrlog2bndlem2  25162  pntrlog2bndlem3  25163  pntrlog2bndlem4  25164  pntrlog2bndlem5  25165  pntrlog2bndlem6  25167  pntrlog2bnd  25168  pntpbnd1a  25169  pntpbnd1  25170  pntpbnd2  25171  pntpbnd  25172  pntibndlem2  25175  pntibndlem3  25176  pntibnd  25177  pntlemb  25181  pntlemg  25182  pntlemh  25183  pntlemr  25186  pntlemk  25190  pntlemo  25191  pnt2  25197  pnt  25198  ostth2lem1  25202  ostth3  25222  istrkg3ld  25255  tgldimor  25292  trgcgrg  25305  tgcgr4  25321  axlowdimlem6  25722  axlowdimlem16  25732  axlowdimlem17  25733  axlowdim  25736  upgrfi  25877  umgrupgr  25888  umgrislfupgrlem  25907  umgrislfupgr  25908  lfgrnloop  25910  upgredg  25922  usgruspgr  25960  usgrislfuspgr  25966  lfuhgr1v0e  26033  usgrexmpldifpr  26037  usgrexmplef  26038  nbusgrvtxm1  26162  vdegp1bi  26313  upgrewlkle2  26366  lfgrwlkprop  26447  upgr2pthnlp  26491  usgr2pthlem  26522  pthdlem1  26525  wwlksm1edg  26630  wwlksnextwrd  26655  wwlksnextfun  26656  wwlksnextinj  26657  wwlksnextproplem3  26669  clwlkclwwlklem2a1  26754  clwlkclwwlklem2a2  26755  clwlkclwwlklem2fv1  26757  clwlkclwwlklem2fv2  26758  clwlkclwwlklem2a4  26759  clwlkclwwlklem2a  26760  clwlkclwwlklem2  26762  clwlkclwwlk2  26765  clwwlksext2edg  26783  clwlksfclwwlk  26822  konigsbergiedgw  26968  konigsbergiedgwOLD  26969  konigsbergssiedgw  26971  konigsberglem1  26974  konigsberglem2  26975  konigsberglem3  26976  konigsberg  26979  frgrwopreglem2  27034  extwwlkfablem2  27062  numclwwlkovf2ex  27069  frgrreggt1  27099  ex-pss  27133  ex-res  27146  ex-fv  27148  ex-fl  27152  ex-mod  27154  ex-abs  27160  nvge0  27368  ipidsq  27405  minvecolem2  27571  minvecolem4  27576  normlem7  27813  norm-ii-i  27834  norm3lemt  27849  normpar2i  27853  bcsiALT  27876  pjhthlem1  28090  opsqrlem6  28844  cdj3lem1  29133  addltmulALT  29145  oppgle  29430  resvplusg  29610  sqsscirc1  29728  nexple  29845  dya2iocucvr  30119  omssubadd  30135  oddpwdc  30189  eulerpartlemgc  30197  fibp1  30236  coinfliplem  30313  coinflipspace  30315  ballotlem2  30323  signstfveq0  30426  subfacp1lem1  30861  subfacp1lem5  30866  subfacval3  30871  problem2  31259  problem2OLD  31260  problem5  31263  circum  31268  nn0prpwlem  31932  dnibndlem10  32092  knoppcnlem2  32099  knoppcnlem4  32101  knoppcnlem10  32107  unbdqndv2lem1  32115  knoppndvlem1  32118  knoppndvlem10  32127  knoppndvlem11  32128  knoppndvlem12  32129  knoppndvlem14  32131  knoppndvlem15  32132  knoppndvlem17  32134  knoppndvlem18  32135  knoppndvlem19  32136  knoppndvlem20  32137  knoppndvlem21  32138  cnndvlem1  32143  taupi  32775  relowlpssretop  32817  sin2h  32998  cos2h  32999  tan2h  33000  poimirlem7  33015  poimirlem9  33017  opnmbllem0  33044  mblfinlem1  33045  mblfinlem2  33046  itg2addnclem  33060  isbnd2  33181  isbnd3  33182  heiborlem7  33215  rabren3dioph  36826  pellexlem2  36841  pellexlem5  36844  pell14qrgapw  36887  pellfundex  36897  rmspecsqrtnq  36917  rmspecsqrtnqOLD  36918  jm2.24nn  36973  jm2.17a  36974  jm2.17b  36975  jm2.17c  36976  acongrep  36994  acongeq  36997  jm2.22  37009  jm2.23  37010  jm2.20nn  37011  jm3.1lem2  37032  expdiophlem1  37035  imo72b2lem0  37914  lhe4.4ex1a  37977  isosctrlem1ALT  38620  sineq0ALT  38623  lt3addmuld  38947  suplesup  38987  infleinflem2  39019  infleinf  39020  sumnnodd  39234  0ellimcdiv  39253  sinaover2ne0  39350  stoweidlem13  39505  stoweidlem14  39506  stoweidlem26  39518  stoweidlem49  39541  stoweidlem52  39544  wallispilem4  39560  wallispilem5  39561  wallispi  39562  wallispi2lem1  39563  wallispi2lem2  39564  wallispi2  39565  stirlinglem1  39566  stirlinglem3  39568  stirlinglem5  39570  stirlinglem6  39571  stirlinglem7  39572  stirlinglem10  39575  stirlinglem11  39576  stirlinglem15  39580  stirlingr  39582  dirker2re  39584  dirkerval2  39586  dirkerre  39587  dirkerper  39588  dirkertrigeqlem1  39590  dirkertrigeqlem3  39592  dirkercncflem1  39595  dirkercncflem2  39596  dirkercncflem4  39598  fourierdlem24  39623  fourierdlem43  39642  fourierdlem44  39643  fourierdlem57  39655  fourierdlem58  39656  fourierdlem62  39660  fourierdlem66  39664  fourierdlem68  39666  fourierdlem72  39670  fourierdlem76  39674  fourierdlem78  39676  fourierdlem79  39677  fourierdlem94  39692  fourierdlem103  39701  fourierdlem104  39702  fourierdlem111  39709  fourierdlem113  39711  sqwvfoura  39720  sqwvfourb  39721  fourierswlem  39722  fouriersw  39723  etransclem23  39749  salexct2  39832  salexct3  39835  salgencntex  39836  salgensscntex  39837  sge0ad2en  39923  ovnsubaddlem1  40059  smfmullem4  40276  smf2id  40283  2leaddle2  40578  p1lep2  40580  pfx2  40680  fmtnoge3  40710  fmtnof1  40715  fmtnoprmfac2lem1  40746  fmtno4prmfac  40752  fmtno4prm  40755  2pwp1prm  40771  31prm  40780  sfprmdvdsmersenne  40788  lighneallem2  40791  lighneallem4a  40793  lighneallem4b  40794  dfodd4  40839  oexpnegALTV  40856  nn0o1gt2ALTV  40873  nnoALTV  40874  nn0oALTV  40875  nn0e  40876  perfectALTVlem1  40894  perfectALTVlem2  40895  gbogt5  40914  sgoldbalt  40933  nnsum3primes4  40934  nnsum3primesgbe  40938  nnsum3primesle9  40940  nnsum4primesodd  40942  nnsum4primesoddALTV  40943  wtgoldbnnsum4prm  40948  bgoldbnnsum3prm  40950  cznnring  41198  nn0le2is012  41387  ply1mulgsumlem2  41418  zlmodzxznm  41529  zlmodzxzldeplem  41530  difmodm1lt  41560  nn0eo  41565  flnn0div2ge  41570  rege1logbzge0  41600  fldivexpfllog2  41606  logbpw2m1  41608  fllog2  41609  blenpw2m1  41620  nnpw2blen  41621  nnolog2flm1  41631  blennngt2o2  41633  dig2nn1st  41646  dig2nn0  41652  dig2bits  41655  dignn0flhalflem1  41656  dignn0flhalflem2  41657  dignn0flhalf  41659  nn0sumshdiglemA  41660
  Copyright terms: Public domain W3C validator