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

Theorem 2re 10768
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 10757 . 2 2 = (1 + 1)
2 1re 9727 . . 3 1 ∈ ℝ
32, 2readdcli 9741 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2579 1 2 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1937  (class class class)co 6363  cr 9623  1c1 9625   + caddc 9627  2c2 10748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-addrcl 9685  ax-mulcl 9686  ax-mulrcl 9687  ax-i2m1 9692  ax-1ne0 9693  ax-rrecex 9696  ax-cnre 9697
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-iota 5597  df-fv 5641  df-ov 6366  df-2 10757
This theorem is referenced by:  2cn  10769  3re  10772  2ne0  10791  3pos  10792  2lt3  10867  1lt3  10868  2lt4  10870  1lt4  10871  2lt5  10874  2lt6  10879  1lt6  10880  2lt7  10885  1lt7  10886  2lt8  10892  1lt8  10893  2lt9  10900  1lt9  10901  2lt10  10909  1lt10  10910  1le2  10913  2rene0  10915  halfre  10918  halfgt0  10920  halflt1  10921  rehalfcl  10929  halfpos2  10932  halfnneg2  10934  addltmul  10938  nominpos  10939  avglt1  10940  avglt2  10941  nn0lele2xi  11013  nn0n0n1ge2b  11024  nn0ge2m1nn  11025  halfnz  11104  uzuzle23  11290  uz3m2nn  11292  2rp  11398  zgt1rpn0n1  11431  fztpval  11955  fzo0to42pr  12104  flhalf  12170  2txmodxeq0  12259  expubnd  12447  expmulnbnd  12518  nn0opthlem2  12569  faclbnd2  12590  faclbnd4lem1  12592  faclbnd5  12597  4bc2eq6  12628  hashfun  12729  hashge2el2dif  12760  hashge2el2difr  12761  wrdlenge2n0  12835  f1oun2prg  13150  2swrd2eqwrdeq  13182  sqrlem7  13472  sqrt4  13496  sqrt2gt1lt2  13498  abstri  13553  sqreulem  13582  amgm2  13592  caucvgrlem  13896  caucvgrlemOLD  13897  iseralt  13911  climcndslem1  14067  climcndslem2  14068  climcnds  14069  geoihalfsum  14098  efcllem  14292  ege2le3  14304  ef01bndlem  14398  cos01bnd  14400  cos2bnd  14402  cos01gt0  14405  sin02gt0  14406  sincos2sgn  14408  sin4lt0  14409  eirrlem  14416  egt2lt3  14418  epos  14419  ene1  14422  sqrt2re  14462  n2dvds1  14514  oexpneg  14529  bitsp1o  14568  bitsfzolem  14569  bitsfzolemOLD  14570  bitsfzo  14571  bitsfi  14573  6gcd4e2  14664  prmn2uzge3  14806  3lcm2e6  14843  oddprm  14927  iserodd  14947  prmreclem2  15023  prmreclem6  15027  4sqlem11  15061  4sqlem12  15062  prmgaplem7  15189  2expltfac  15224  oppgtset  17164  efgredleme  17554  mgpsca  17890  mgptset  17891  mgpds  17893  matplusg  19597  chfacfscmul0  20040  chfacfpmmul0  20044  psmetge0  21486  xmetge0  21517  bl2in  21573  metnrmlem3  22036  metnrmlem3OLD  22051  iihalf1  22117  iihalf2  22119  pcoass  22214  tchcphlem1  22368  csbren  22512  trirn  22513  minveclem2  22527  minveclem4  22533  minveclem2OLD  22539  minveclem4OLD  22545  pjthlem1  22550  ovolunlem1a  22608  dyadss  22712  opnmbllem  22719  vitalilem2  22728  vitalilem4  22730  mbfi1fseqlem5  22838  lhop1lem  23126  aaliou3lem2  23460  aaliou3lem8  23462  pilem2  23568  pilem2OLD  23569  pilem3  23570  pilem3OLD  23571  pipos  23576  sinhalfpilem  23579  sincosq1lem  23613  sincosq4sgn  23617  tangtx  23621  sinq12gt0  23623  sincos4thpi  23629  tan4thpi  23630  sincos6thpi  23631  sineq0  23637  cosordlem  23641  tanord1  23647  efif1olem1  23652  efif1olem2  23653  efif1olem4  23655  efif1o  23656  efifo  23657  cxpcn3lem  23848  root1id  23855  root1eq1  23856  root1cj  23857  cxpeq  23858  logblog  23890  ang180lem1  23899  ang180lem2  23900  chordthmlem2  23920  1cubrlem  23928  atancj  23997  atantan  24010  atanbndlem  24012  atans2  24018  leibpilem1  24027  leibpi  24029  log2tlbnd  24032  log2ublem2  24034  log2ub  24036  divsqrtsumlem  24066  harmonicbnd3  24094  zetacvg  24101  lgamgulmlem2  24116  lgamgulmlem3  24117  lgamgulmlem4  24118  lgamgulmlem6  24120  lgamucov  24124  basellem1  24168  basellem2  24169  basellem3  24170  basellem5  24172  chtdif  24246  ppidif  24251  ppinncl  24262  chtrpcl  24263  ppieq0  24264  ppiltx  24265  ppiublem1  24291  ppiub  24293  chpeq0  24297  chteq0  24298  chtublem  24300  chtub  24301  chpval2  24307  chpub  24309  mersenne  24316  perfectlem1  24318  perfectlem2  24319  dchrptlem1  24353  dchrptlem2  24354  bcmono  24366  bclbnd  24369  bpos1lem  24371  bposlem1  24373  bposlem2  24374  bposlem3  24375  bposlem4  24376  bposlem5  24377  bposlem6  24378  bposlem7  24379  bposlem8  24380  bposlem9  24381  lgslem1  24385  lgsdirprm  24418  lgseisenlem1  24438  lgseisenlem2  24439  lgseisenlem3  24440  lgseisen  24442  lgsquadlem1  24443  lgsquadlem2  24444  m1lgs  24451  2sqlem11  24464  chebbnd1lem1  24468  chebbnd1lem2  24469  chebbnd1lem3  24470  chebbnd1  24471  chtppilimlem1  24472  chtppilimlem2  24473  chtppilim  24474  chto1ub  24475  chebbnd2  24476  chto1lb  24477  chpchtlim  24478  chpo1ub  24479  chpo1ubb  24480  rplogsumlem1  24483  rplogsumlem2  24484  dchrisumlem2  24489  dchrisumlem3  24490  dchrvmasumiflem1  24500  dchrisum0fno1  24510  dchrisum0re  24512  dchrisum0lem1b  24514  dchrisum0lem1  24515  dchrisum0lem2  24517  rplogsum  24526  mulog2sumlem1  24533  mulog2sumlem2  24534  log2sumbnd  24543  selberglem2  24545  selbergb  24548  selberg2b  24551  chpdifbndlem1  24552  logdivbnd  24555  selberg3lem1  24556  selberg3  24558  selberg4lem1  24559  selberg4  24560  pntrmax  24563  pntrsumbnd2  24566  selberg3r  24568  selberg4r  24569  selberg34r  24570  pntrlog2bndlem2  24577  pntrlog2bndlem3  24578  pntrlog2bndlem4  24579  pntrlog2bndlem5  24580  pntrlog2bndlem6  24582  pntrlog2bnd  24583  pntpbnd1a  24584  pntpbnd1  24585  pntpbnd2  24586  pntpbnd  24587  pntibndlem2  24590  pntibndlem3  24591  pntibnd  24592  pntlemb  24596  pntlemg  24597  pntlemh  24598  pntlemr  24601  pntlemk  24605  pntlemo  24606  pnt2  24612  pnt  24613  ostth2lem1  24617  ostth3  24637  istrkg3ld  24670  tgldimor  24707  trgcgrg  24721  tgcgr4  24737  axlowdimlem6  25138  axlowdimlem16  25148  axlowdimlem17  25149  axlowdim  25152  umgrafi  25210  usisuslgra  25253  usgraexmplvtxlem  25283  usgraex2elv  25286  usgraexmpldifpr  25288  constr3lem4  25536  constr3trllem3  25541  constr3pthlem1  25544  constr3pthlem3  25546  wwlkextwrd  25617  wwlkextfun  25618  wwlkextinj  25619  wwlkm1edg  25624  wwlkextproplem3  25632  clwwlkgt0  25660  clwwlkn0  25663  clwlkisclwwlklem2a1  25668  clwlkisclwwlklem2a2  25669  clwlkisclwwlklem2fv1  25671  clwlkisclwwlklem2fv2  25672  clwlkisclwwlklem2a4  25673  clwlkisclwwlklem2a  25674  clwlkisclwwlklem1  25676  clwlkisclwwlk2  25679  clwwlkext2edg  25691  usg2cwwkdifex  25710  clwlkfclwwlk  25732  konigsberg  25875  vdgfrgragt2  25915  extwwlkfablem2  25966  numclwwlkovf2ex  25974  frgrareggt1  26004  frgrareg  26005  frgraregord013  26006  ex-pss  26038  ex-res  26051  ex-fv  26053  ex-fl  26057  nvge0  26466  ipidsq  26512  minvecolem2  26680  minvecolem4  26685  minvecolem2OLD  26690  minvecolem4OLD  26695  normlem7  26932  norm-ii-i  26953  norm3lemt  26968  normpar2i  26972  bcsiALT  26995  pjhthlem1  27207  opsqrlem6  27961  cdj3lem1  28250  addltmulALT  28262  oppgle  28570  resvplusg  28751  sqsscirc1  28869  nexple  28986  dya2iocucvr  29260  omssubadd  29282  omssubaddOLD  29286  oddpwdc  29341  eulerpartlemgc  29349  fibp1  29388  coinfliplem  29465  coinflipspace  29467  ballotlem2  29475  signstfveq0  29619  subfacp1lem1  30054  subfacp1lem5  30059  subfacval3  30064  problem2  30450  problem5  30453  circum  30470  nn0prpwlem  31127  dnibndlem10  31285  knoppcnlem2  31292  knoppcnlem4  31294  knoppcnlem10  31300  unbdqndv2lem1  31307  taupi  31945  relowlpssretop  31988  sin2h  32168  cos2h  32169  tan2h  32170  poimirlem7  32185  poimirlem9  32187  opnmbllem0  32214  mblfinlem1  32215  mblfinlem2  32216  itg2addnclem  32231  isbnd2  32352  isbnd3  32353  heiborlem7  32386  rabren3dioph  35898  pellexlem2  35914  pellexlem5  35917  pell14qrgapw  35962  pellfundex  35974  rmspecsqrtnq  35994  jm2.24nn  36049  jm2.17a  36050  jm2.17b  36051  jm2.17c  36052  acongrep  36070  acongeq  36073  jm2.22  36090  jm2.23  36091  jm2.20nn  36092  jm3.1lem2  36113  expdiophlem1  36116  imo72b2lem0  36965  isprm7  37017  lhe4.4ex1a  37035  isosctrlem1ALT  37679  sineq0ALT  37682  lt3addmuld  37896  suplesup  37938  infleinflem2  37970  infleinf  37971  sumnnodd  38114  0ellimcdiv  38134  sinaover2ne0  38152  stoweidlem13  38309  stoweidlem14  38310  stoweidlem26  38322  stoweidlem49  38346  stoweidlem52  38349  wallispilem4  38366  wallispilem5  38367  wallispi  38368  wallispi2lem1  38369  wallispi2lem2  38370  wallispi2  38371  stirlinglem1  38372  stirlinglem3  38374  stirlinglem5  38376  stirlinglem6  38377  stirlinglem7  38378  stirlinglem10  38381  stirlinglem11  38382  stirlinglem15  38386  stirlingr  38388  dirker2re  38390  dirkerval2  38392  dirkerre  38393  dirkerper  38394  dirkertrigeqlem1  38396  dirkertrigeqlem3  38398  dirkercncflem1  38401  dirkercncflem2  38402  dirkercncflem4  38404  fourierdlem24  38429  fourierdlem43  38450  fourierdlem44  38451  fourierdlem57  38463  fourierdlem58  38464  fourierdlem62  38468  fourierdlem66  38472  fourierdlem68  38474  fourierdlem72  38478  fourierdlem76  38482  fourierdlem78  38484  fourierdlem79  38485  fourierdlem94  38500  fourierdlem103  38509  fourierdlem104  38510  fourierdlem111  38517  fourierdlem113  38519  sqwvfoura  38528  sqwvfourb  38529  fourierswlem  38530  fouriersw  38531  etransclem23  38558  salexct2  38642  salexct3  38645  salgencntex  38646  salgensscntex  38647  sge0ad2en  38719  ovnsubaddlem1  38855  mod2eq1n2dvds  39245  dfodd4  39308  oexpnegALTV  39326  nn0o1gt2ALTV  39343  nnoALTV  39344  nn0oALTV  39345  nn0e  39346  perfectALTVlem1  39363  perfectALTVlem2  39364  gbogt5  39383  sgoldbalt  39402  nnsum3primes4  39403  nnsum3primesgbe  39407  nnsum3primesle9  39409  nnsum4primesodd  39411  nnsum4primesoddALTV  39412  evengpoap3  39414  wtgoldbnnsum4prm  39417  bgoldbnnsum3prm  39419  pfx2  39475  2leaddle2  39567  p1lep2  39569  xnn0n0n1ge2b  39616  upgrfi  39717  umgrupgr  39728  umgrislfupgrlem  39747  umgrislfupgr  39748  lfgrnloop  39750  upgredg  39770  usgruspgr  39808  usgrislfuspgr  39814  lfuhgr1v0e  39880  nbusgrvtxm1  40007  vdegp1bi-av  40153  upgrewlkle2  40208  lfgrwlkprop  40296  upgr2pthnlp  40338  usgr2pthlem  40369  pthdlem1  40372  wwlksm1edg  40478  wwlksnextwrd  40503  wwlksnextfun  40504  wwlksnextinj  40505  wwlksnextproplem3  40517  clwlkclwwlklem2a1  40601  clwlkclwwlklem2a2  40602  clwlkclwwlklem2fv1  40604  clwlkclwwlklem2fv2  40605  clwlkclwwlklem2a4  40606  clwlkclwwlklem2a  40607  clwlkclwwlklem2  40609  clwlkclwwlk2  40612  clwwlksext2edg  40630  clwlksfclwwlk  40669  konigsbergiedgw  40816  konigsbergiedgwOLD  40817  konigsbergssiedgw  40819  konigsberglem1  40822  konigsberglem2  40823  konigsberglem3  40824  konigsberg-av  40827  frgrwopreglem2  40882  av-extwwlkfablem2  40910  av-numclwwlkovf2ex  40917  av-frgrareggt1  40947  plusgndxnmulrndx  41143  cznnring  41148  nn0le2is012  41338  ply1mulgsumlem2  41369  zlmodzxznm  41480  zlmodzxzldeplem  41481  3halfnz  41506  difmodm1lt  41514  nn0o1gt2  41516  nno  41517  nn0o  41518  nn0eo  41524  flnn0div2ge  41529  rege1logbzge0  41559  fldivexpfllog2  41565  logbpw2m1  41567  fllog2  41568  blenpw2m1  41579  nnpw2blen  41580  nnolog2flm1  41590  blennngt2o2  41592  dig2nn1st  41605  dig2nn0  41611  dig2bits  41614  dignn0flhalflem1  41615  dignn0flhalflem2  41616  dignn0flhalf  41618  nn0sumshdiglemA  41619
  Copyright terms: Public domain W3C validator