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

Theorem 2re 11075
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 11064 . 2 2 = (1 + 1)
2 1re 10024 . . 3 1 ∈ ℝ
32, 2readdcli 10038 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2695 1 2 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1988  (class class class)co 6635  cr 9920  1c1 9922   + caddc 9924  2c2 11055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-i2m1 9989  ax-1ne0 9990  ax-rrecex 9993  ax-cnre 9994
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-2 11064
This theorem is referenced by:  2cn  11076  3re  11079  2ne0  11098  3pos  11099  2lt3  11180  1lt3  11181  2lt4  11183  1lt4  11184  2lt5  11187  2lt6  11192  1lt6  11193  2lt7  11198  1lt7  11199  2lt8  11205  1lt8  11206  2lt9  11213  1lt9  11214  2lt10OLD  11222  1lt10OLD  11223  1le2  11226  2rene0  11228  halfre  11231  halfgt0  11233  halflt1  11235  rehalfcl  11243  halfpos2  11246  halfnneg2  11248  addltmul  11253  nominpos  11254  avglt1  11255  avglt2  11256  div4p1lem1div2  11272  nn0lele2xi  11333  nn0n0n1ge2b  11344  nn0ge2m1nn  11345  nn0le2is012  11426  halfnz  11440  3halfnz  11441  2lt10  11665  1lt10  11666  uzuzle23  11714  uz3m2nn  11716  2rp  11822  zgt1rpn0n1  11856  xnn0n0n1ge2b  11950  fztpval  12387  fz0to4untppr  12426  fzo0to42pr  12539  2tnp1ge0ge0  12613  flhalf  12614  fldiv4p1lem1div2  12619  fldiv4lem1div2uz2  12620  2txmodxeq0  12713  expubnd  12904  expmulnbnd  12979  nn0opthlem2  13039  faclbnd2  13061  faclbnd4lem1  13063  faclbnd5  13068  4bc2eq6  13099  hashfun  13207  hashge2el2dif  13245  hashge2el2difr  13246  wrdlenge2n0  13324  f1oun2prg  13643  2swrd2eqwrdeq  13677  sqrlem7  13970  sqrt4  13994  sqrt2gt1lt2  13996  abstri  14051  sqreulem  14080  amgm2  14090  caucvgrlem  14384  iseralt  14396  climcndslem1  14562  climcndslem2  14563  climcnds  14564  geoihalfsum  14595  efcllem  14789  ege2le3  14801  ef01bndlem  14895  cos01bnd  14897  cos2bnd  14899  cos01gt0  14902  sin02gt0  14903  sincos2sgn  14905  sin4lt0  14906  eirrlem  14913  egt2lt3  14915  epos  14916  ene1  14919  sqrt2re  14961  oexpneg  15050  mod2eq1n2dvds  15052  oddge22np1  15054  evennn02n  15055  evennn2n  15056  nn0ehalf  15076  nn0o1gt2  15078  nno  15079  nn0o  15080  nn0oddm1d2  15082  nnoddm1d2  15083  n2dvds1  15085  flodddiv4t2lthalf  15121  bitsp1o  15136  bitsfzolem  15137  bitsfzo  15138  bitsfi  15140  6gcd4e2  15236  isprm7  15401  3lcm2e6  15421  oddprm  15496  iserodd  15521  prmreclem2  15602  prmreclem6  15606  4sqlem11  15640  4sqlem12  15641  prmgaplem7  15742  2expltfac  15780  plusgndxnmulrndx  15979  oppgtset  17763  efgredleme  18137  mgpsca  18477  mgptset  18478  mgpds  18480  rmodislmod  18912  cnfldfun  19739  zringndrg  19819  matplusg  20201  chfacfscmul0  20644  chfacfpmmul0  20648  psmetge0  22098  xmetge0  22130  bl2in  22186  metnrmlem3  22645  iihalf1  22711  iihalf2  22713  pcoass  22805  tchcphlem1  23015  csbren  23163  trirn  23164  minveclem2  23178  minveclem4  23184  pjthlem1  23189  ovolunlem1a  23245  dyadss  23343  opnmbllem  23350  vitalilem2  23359  vitalilem4  23361  mbfi1fseqlem5  23467  lhop1lem  23757  aaliou3lem2  24079  aaliou3lem8  24081  pilem2  24187  pilem3  24188  pipos  24193  sinhalfpilem  24196  sincosq1lem  24230  sincosq4sgn  24234  tangtx  24238  sinq12gt0  24240  sincos4thpi  24246  tan4thpi  24247  sincos6thpi  24248  sineq0  24254  cosordlem  24258  tanord1  24264  efif1olem1  24269  efif1olem2  24270  efif1olem4  24272  efif1o  24273  efifo  24274  cxpcn3lem  24469  root1id  24476  root1eq1  24477  root1cj  24478  cxpeq  24479  logblog  24511  ang180lem1  24520  ang180lem2  24521  chordthmlem2  24541  1cubrlem  24549  atancj  24618  atantan  24631  atanbndlem  24633  atans2  24639  leibpilem1  24648  leibpi  24650  log2tlbnd  24653  log2ublem2  24655  log2ub  24657  divsqrtsumlem  24687  harmonicbnd3  24715  zetacvg  24722  lgamgulmlem2  24737  lgamgulmlem3  24738  lgamgulmlem4  24739  lgamgulmlem6  24741  lgamucov  24745  basellem1  24788  basellem2  24789  basellem3  24790  basellem5  24792  chtdif  24865  ppidif  24870  ppinncl  24881  chtrpcl  24882  ppieq0  24883  ppiltx  24884  ppiublem1  24908  ppiub  24910  chpeq0  24914  chteq0  24915  chtublem  24917  chtub  24918  chpval2  24924  chpub  24926  mersenne  24933  perfectlem1  24935  perfectlem2  24936  dchrptlem1  24970  dchrptlem2  24971  bcmono  24983  bclbnd  24986  bpos1lem  24988  bposlem1  24990  bposlem2  24991  bposlem3  24992  bposlem4  24993  bposlem5  24994  bposlem6  24995  bposlem7  24996  bposlem8  24997  bposlem9  24998  lgslem1  25003  lgsdirprm  25037  gausslemma2dlem0c  25064  gausslemma2dlem1a  25071  gausslemma2dlem2  25073  gausslemma2dlem3  25074  lgseisenlem1  25081  lgseisenlem2  25082  lgseisenlem3  25083  lgseisen  25085  lgsquadlem1  25086  lgsquadlem2  25087  m1lgs  25094  2lgslem1a1  25095  2lgslem1a2  25096  2lgslem1c  25099  2lgslem4  25112  2sqlem11  25135  chebbnd1lem1  25139  chebbnd1lem2  25140  chebbnd1lem3  25141  chebbnd1  25142  chtppilimlem1  25143  chtppilimlem2  25144  chtppilim  25145  chto1ub  25146  chebbnd2  25147  chto1lb  25148  chpchtlim  25149  chpo1ub  25150  chpo1ubb  25151  rplogsumlem1  25154  rplogsumlem2  25155  dchrisumlem2  25160  dchrisumlem3  25161  dchrvmasumiflem1  25171  dchrisum0fno1  25181  dchrisum0re  25183  dchrisum0lem1b  25185  dchrisum0lem1  25186  dchrisum0lem2  25188  rplogsum  25197  mulog2sumlem1  25204  mulog2sumlem2  25205  log2sumbnd  25214  selberglem2  25216  selbergb  25219  selberg2b  25222  chpdifbndlem1  25223  logdivbnd  25226  selberg3lem1  25227  selberg3  25229  selberg4lem1  25230  selberg4  25231  pntrmax  25234  pntrsumbnd2  25237  selberg3r  25239  selberg4r  25240  selberg34r  25241  pntrlog2bndlem2  25248  pntrlog2bndlem3  25249  pntrlog2bndlem4  25250  pntrlog2bndlem5  25251  pntrlog2bndlem6  25253  pntrlog2bnd  25254  pntpbnd1a  25255  pntpbnd1  25256  pntpbnd2  25257  pntpbnd  25258  pntibndlem2  25261  pntibndlem3  25262  pntibnd  25263  pntlemb  25267  pntlemg  25268  pntlemh  25269  pntlemr  25272  pntlemk  25276  pntlemo  25277  pnt2  25283  pnt  25284  ostth2lem1  25288  ostth3  25308  istrkg3ld  25341  tgldimor  25378  trgcgrg  25391  tgcgr4  25407  axlowdimlem6  25808  axlowdimlem16  25818  axlowdimlem17  25819  axlowdim  25822  upgrfi  25967  umgrupgr  25979  umgrislfupgrlem  25998  umgrislfupgr  25999  lfgrnloop  26001  usgruspgr  26054  usgrislfuspgr  26060  lfuhgr1v0e  26127  usgrexmpldifpr  26131  usgrexmplef  26132  nbusgrvtxm1  26262  vdegp1bi  26414  upgrewlkle2  26483  lfgrwlkprop  26565  upgr2pthnlp  26609  usgr2pthlem  26640  pthdlem1  26643  wwlksm1edg  26748  wwlksnextwrd  26773  wwlksnextfun  26774  wwlksnextinj  26775  wwlksnextproplem3  26787  clwlkclwwlklem2a1  26874  clwlkclwwlklem2a2  26875  clwlkclwwlklem2fv1  26877  clwlkclwwlklem2fv2  26878  clwlkclwwlklem2a4  26879  clwlkclwwlklem2a  26880  clwlkclwwlklem2  26882  clwlkclwwlk2  26885  clwwlksext2edg  26903  clwlksfclwwlk  26942  konigsbergiedgw  27088  konigsbergiedgwOLD  27089  konigsbergssiedgw  27091  konigsberglem1  27094  konigsberglem2  27095  konigsberglem3  27096  konigsberg  27099  extwwlkfablem2  27184  numclwwlkovf2ex  27191  frgrreggt1  27221  ex-pss  27255  ex-res  27268  ex-fv  27270  ex-fl  27274  ex-mod  27276  ex-abs  27282  nvge0  27498  ipidsq  27535  minvecolem2  27701  minvecolem4  27706  normlem7  27943  norm-ii-i  27964  norm3lemt  27979  normpar2i  27983  bcsiALT  28006  pjhthlem1  28220  opsqrlem6  28974  cdj3lem1  29263  addltmulALT  29275  threehalves  29597  oppgle  29627  resvplusg  29807  sqsscirc1  29928  nexple  30045  dya2iocucvr  30320  omssubadd  30336  oddpwdc  30390  eulerpartlemgc  30398  fibp1  30437  coinfliplem  30514  coinflipspace  30516  ballotlem2  30524  signstfveq0  30628  prodfzo03  30655  hgt750lemd  30700  logdivsqrle  30702  hgt750lem  30703  hgt750lem2  30704  hgt750leme  30710  subfacp1lem1  31135  subfacp1lem5  31140  subfacval3  31145  problem2  31533  problem2OLD  31534  problem5  31537  circum  31542  nn0prpwlem  32292  dnibndlem10  32452  knoppcnlem2  32459  knoppcnlem4  32461  knoppcnlem10  32467  unbdqndv2lem1  32475  knoppndvlem1  32478  knoppndvlem10  32487  knoppndvlem11  32488  knoppndvlem12  32489  knoppndvlem14  32491  knoppndvlem15  32492  knoppndvlem17  32494  knoppndvlem18  32495  knoppndvlem19  32496  knoppndvlem20  32497  knoppndvlem21  32498  cnndvlem1  32503  taupi  33140  relowlpssretop  33183  sin2h  33370  cos2h  33371  tan2h  33372  poimirlem7  33387  poimirlem9  33389  opnmbllem0  33416  mblfinlem1  33417  mblfinlem2  33418  itg2addnclem  33432  isbnd2  33553  isbnd3  33554  heiborlem7  33587  rabren3dioph  37198  pellexlem2  37213  pellexlem5  37216  pell14qrgapw  37259  pellfundex  37269  rmspecsqrtnq  37289  rmspecsqrtnqOLD  37290  jm2.24nn  37345  jm2.17a  37346  jm2.17b  37347  jm2.17c  37348  acongrep  37366  acongeq  37369  jm2.22  37381  jm2.23  37382  jm2.20nn  37383  jm3.1lem2  37404  expdiophlem1  37407  imo72b2lem0  38285  lhe4.4ex1a  38348  isosctrlem1ALT  38990  sineq0ALT  38993  lt3addmuld  39328  suplesup  39368  infleinflem2  39400  infleinf  39401  sumnnodd  39662  0ellimcdiv  39681  sinaover2ne0  39842  stoweidlem13  39993  stoweidlem14  39994  stoweidlem26  40006  stoweidlem49  40029  stoweidlem52  40032  wallispilem4  40048  wallispilem5  40049  wallispi  40050  wallispi2lem1  40051  wallispi2lem2  40052  wallispi2  40053  stirlinglem1  40054  stirlinglem3  40056  stirlinglem5  40058  stirlinglem6  40059  stirlinglem7  40060  stirlinglem10  40063  stirlinglem11  40064  stirlinglem15  40068  stirlingr  40070  dirker2re  40072  dirkerval2  40074  dirkerre  40075  dirkerper  40076  dirkertrigeqlem1  40078  dirkertrigeqlem3  40080  dirkercncflem1  40083  dirkercncflem2  40084  dirkercncflem4  40086  fourierdlem24  40111  fourierdlem43  40130  fourierdlem44  40131  fourierdlem57  40143  fourierdlem58  40144  fourierdlem62  40148  fourierdlem66  40152  fourierdlem68  40154  fourierdlem72  40158  fourierdlem76  40162  fourierdlem78  40164  fourierdlem79  40165  fourierdlem94  40180  fourierdlem103  40189  fourierdlem104  40190  fourierdlem111  40197  fourierdlem113  40199  sqwvfoura  40208  sqwvfourb  40209  fourierswlem  40210  fouriersw  40211  etransclem23  40237  salexct2  40320  salexct3  40323  salgencntex  40324  salgensscntex  40325  sge0ad2en  40411  ovnsubaddlem1  40547  smfmullem4  40764  smf2id  40771  2leaddle2  41075  p1lep2  41077  pfx2  41177  fmtnoge3  41207  fmtnof1  41212  fmtnoprmfac2lem1  41243  fmtno4prmfac  41249  fmtno4prm  41252  2pwp1prm  41268  31prm  41277  sfprmdvdsmersenne  41285  lighneallem2  41288  lighneallem4a  41290  lighneallem4b  41291  dfodd4  41336  oexpnegALTV  41353  nn0o1gt2ALTV  41370  nnoALTV  41371  nn0oALTV  41372  nn0e  41373  perfectALTVlem1  41395  perfectALTVlem2  41396  gbowgt5  41415  sbgoldbalt  41434  sgoldbeven3prm  41436  mogoldbb  41438  nnsum3primes4  41441  nnsum3primesgbe  41445  nnsum3primesle9  41447  nnsum4primesodd  41449  nnsum4primesoddALTV  41450  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  cznnring  41721  ply1mulgsumlem2  41940  zlmodzxznm  42051  zlmodzxzldeplem  42052  difmodm1lt  42082  nn0eo  42087  flnn0div2ge  42092  rege1logbzge0  42118  fldivexpfllog2  42124  logbpw2m1  42126  fllog2  42127  blenpw2m1  42138  nnpw2blen  42139  nnolog2flm1  42149  blennngt2o2  42151  dig2nn1st  42164  dig2nn0  42170  dig2bits  42173  dignn0flhalflem1  42174  dignn0flhalflem2  42175  dignn0flhalf  42177  nn0sumshdiglemA  42178
  Copyright terms: Public domain W3C validator