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

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

Proof of Theorem 2re
StepHypRef Expression
1 df-2 10619 . 2
2 1re 9616 . . 3
32, 2readdcli 9630 . 2
41, 3eqeltri 2541 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  (class class class)co 6296   cr 9512  1c1 9514   caddc 9516  2c2 10610
This theorem is referenced by:  2cn  10631  3re  10634  2ne0  10653  3pos  10654  2lt3  10728  1lt3  10729  2lt4  10731  1lt4  10732  2lt5  10735  2lt6  10740  1lt6  10741  2lt7  10746  1lt7  10747  2lt8  10753  1lt8  10754  2lt9  10761  1lt9  10762  2lt10  10770  1lt10  10771  1le2  10774  2rene0  10776  halfre  10779  halfgt0  10781  halflt1  10782  rehalfcl  10790  halfpos2  10793  halfnneg2  10795  addltmul  10799  nominpos  10800  avglt1  10801  avglt2  10802  nn0lele2xi  10873  nn0n0n1ge2b  10885  nn0ge2m1nn  10886  halfnz  10966  uzuzle23  11150  uz3m2nn  11152  2rp  11254  fztpval  11770  fzo0to42pr  11901  flhalf  11962  2txmodxeq0  12047  expubnd  12226  expmulnbnd  12298  nn0opthlem2  12349  faclbnd2  12369  faclbnd4lem1  12371  faclbnd5  12376  hashfun  12495  hashge2el2dif  12521  wrdlenge2n0  12577  ccatw2s1p1  12640  f1oun2prg  12865  2swrd2eqwrdeq  12891  sqrlem7  13082  sqrt4  13106  sqrt2gt1lt2  13108  abstri  13163  sqreulem  13192  amgm2  13202  caucvgrlem  13495  iseralt  13507  climcndslem1  13661  climcndslem2  13662  climcnds  13663  geoihalfsum  13691  efcllem  13813  ege2le3  13825  ef01bndlem  13919  cos01bnd  13921  cos2bnd  13923  cos01gt0  13926  sin02gt0  13927  sincos2sgn  13929  sin4lt0  13930  eirrlem  13937  egt2lt3  13939  epos  13940  sqrt2re  13983  n2dvds1  14035  oexpneg  14049  bitsp1o  14083  bitsfzolem  14084  bitsfzo  14085  bitsfi  14087  prmn2uzge3  14237  oddprm  14339  iserodd  14359  prmreclem2  14435  prmreclem6  14439  4sqlem11  14473  4sqlem12  14474  2expltfac  14577  oppgtset  16387  efgredleme  16761  mgpsca  17148  mgptset  17149  mgpds  17151  matplusg  18916  chfacfscmul0  19359  chfacfpmmul0  19363  psmetge0  20816  xmetge0  20847  bl2in  20903  metnrmlem3  21365  iihalf1  21431  iihalf2  21433  pcoass  21524  tchcphlem1  21678  csbren  21826  trirn  21827  minveclem2  21841  minveclem4  21847  pjthlem1  21852  ovolunlem1a  21907  dyadss  22003  opnmbllem  22010  vitalilem2  22018  vitalilem4  22020  mbfi1fseqlem5  22126  lhop1lem  22414  aaliou3lem2  22739  aaliou3lem8  22741  pilem2  22847  pilem3  22848  pipos  22853  sinhalfpilem  22856  sincosq1lem  22890  sincosq4sgn  22894  tangtx  22898  sinq12gt0  22900  sincos4thpi  22906  tan4thpi  22907  sincos6thpi  22908  sineq0  22914  cosordlem  22918  tanord1  22924  efif1olem1  22929  efif1olem2  22930  efif1olem4  22932  efif1o  22933  efifo  22934  cxpcn3lem  23121  root1id  23128  root1eq1  23129  root1cj  23130  cxpeq  23131  ang180lem1  23141  ang180lem2  23142  chordthmlem2  23164  1cubrlem  23172  atancj  23241  atantan  23254  atanbndlem  23256  atans2  23262  leibpilem1  23271  leibpi  23273  log2tlbnd  23276  log2ublem2  23278  log2ub  23280  divsqrtsumlem  23309  harmonicbnd3  23337  basellem1  23354  basellem2  23355  basellem3  23356  basellem5  23358  chtdif  23432  ppidif  23437  ppinncl  23448  chtrpcl  23449  ppieq0  23450  ppiltx  23451  ppiublem1  23477  ppiub  23479  chpeq0  23483  chteq0  23484  chtublem  23486  chtub  23487  chpval2  23493  chpub  23495  mersenne  23502  perfectlem1  23504  perfectlem2  23505  dchrptlem1  23539  dchrptlem2  23540  bcmono  23552  bclbnd  23555  bpos1lem  23557  bposlem1  23559  bposlem2  23560  bposlem3  23561  bposlem4  23562  bposlem5  23563  bposlem6  23564  bposlem7  23565  bposlem8  23566  bposlem9  23567  lgslem1  23571  lgsdirprm  23604  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgseisen  23628  lgsquadlem1  23629  lgsquadlem2  23630  m1lgs  23637  2sqlem11  23650  chebbnd1lem1  23654  chebbnd1lem2  23655  chebbnd1lem3  23656  chebbnd1  23657  chtppilimlem1  23658  chtppilimlem2  23659  chtppilim  23660  chto1ub  23661  chebbnd2  23662  chto1lb  23663  chpchtlim  23664  chpo1ub  23665  chpo1ubb  23666  rplogsumlem1  23669  rplogsumlem2  23670  dchrisumlem2  23675  dchrisumlem3  23676  dchrvmasumiflem1  23686  dchrisum0fno1  23696  dchrisum0re  23698  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2  23703  rplogsum  23712  mulog2sumlem1  23719  mulog2sumlem2  23720  log2sumbnd  23729  selberglem2  23731  selbergb  23734  selberg2b  23737  chpdifbndlem1  23738  logdivbnd  23741  selberg3lem1  23742  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrmax  23749  pntrsumbnd2  23752  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntpbnd  23773  pntibndlem2  23776  pntibndlem3  23777  pntibnd  23778  pntlemb  23782  pntlemg  23783  pntlemh  23784  pntlemr  23787  pntlemk  23791  pntlemo  23792  pnt2  23798  pnt  23799  ostth2lem1  23803  ostth3  23823  tgldimor  23893  trgcgrg  23906  axlowdimlem6  24250  axlowdimlem16  24260  axlowdimlem17  24261  axlowdim  24264  umgrafi  24322  usisuslgra  24365  usgraexvlem  24395  usgraex2elv  24398  usgraexmpldifpr  24400  constr3lem4  24647  constr3trllem3  24652  constr3pthlem1  24655  constr3pthlem3  24657  wwlkextwrd  24728  wwlkextfun  24729  wwlkextinj  24730  wwlkm1edg  24735  wwlkextproplem3  24743  clwwlkgt0  24771  clwwlkn0  24774  clwlkisclwwlklem2a1  24779  clwlkisclwwlklem2a2  24780  clwlkisclwwlklem2fv1  24782  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwlkisclwwlk2  24790  clwwlkext2edg  24802  usg2cwwkdifex  24821  clwlkfclwwlk  24844  konigsberg  24987  vdgfrgragt2  25027  extwwlkfablem2  25078  numclwwlkovf2ex  25086  frgrareggt1  25116  frgrareg  25117  frgraregord013  25118  ex-pss  25149  ex-res  25162  ex-fv  25164  ex-fl  25168  nvge0  25577  ipidsq  25623  minvecolem2  25791  minvecolem4  25796  normlem7  26033  norm-ii-i  26054  norm3lemt  26069  normpar2i  26073  bcsiALT  26096  pjhthlem1  26309  opsqrlem6  27064  cdj3lem1  27353  addltmulALT  27365  oppgle  27641  resvplusg  27823  sqsscirc1  27890  nexple  28005  rnlogblem  28015  dya2iocucvr  28255  oddpwdc  28293  eulerpartlemgc  28301  fibp1  28340  coinfliplem  28417  coinflipspace  28419  ballotlem2  28427  signstfveq0  28534  zetacvg  28557  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem6  28576  lgamucov  28580  subfacp1lem1  28623  subfacp1lem5  28628  subfacval3  28633  problem2  29020  problem5  29023  circum  29040  4bc2eq6  29112  sin2h  30045  cos2h  30046  tan2h  30047  opnmbllem0  30050  mblfinlem1  30051  mblfinlem2  30052  itg2addnclem  30066  nn0prpwlem  30140  isbnd2  30279  isbnd3  30280  heiborlem7  30313  rabren3dioph  30749  pellexlem2  30766  pellexlem5  30769  pell14qrgapw  30812  pellfundex  30822  rmspecsqrtnq  30842  jm2.24nn  30897  jm2.17a  30898  jm2.17b  30899  jm2.17c  30900  acongrep  30918  acongeq  30921  jm2.22  30937  jm2.23  30938  jm2.20nn  30939  jm3.1lem2  30960  expdiophlem1  30963  isprm7  31192  3lcm2e6  31219  lhe4.4ex1a  31234  lt3addmuld  31501  sumnnodd  31636  0ellimcdiv  31655  sinaover2ne0  31668  stoweidlem13  31795  stoweidlem14  31796  stoweidlem26  31808  stoweidlem49  31831  stoweidlem52  31834  wallispilem4  31850  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  wallispi2  31855  stirlinglem1  31856  stirlinglem3  31858  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem10  31865  stirlinglem11  31866  stirlinglem15  31870  stirlingr  31872  dirker2re  31874  dirkerval2  31876  dirkerre  31877  dirkerper  31878  dirkertrigeqlem1  31880  dirkertrigeqlem3  31882  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem24  31913  fourierdlem43  31932  fourierdlem44  31933  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  fourierdlem66  31955  fourierdlem68  31957  fourierdlem72  31961  fourierdlem76  31965  fourierdlem78  31967  fourierdlem79  31968  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem113  32002  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  etransclem23  32040  2leaddle2  32320  p1lep2  32322  usgra2pthlem1  32353  plusgndxnmulrndx  32759  cznnring  32764  nn0le2is012  32956  ply1mulgsumlem2  32987  zlmodzxznm  33098  zlmodzxzldeplem  33099  ene1  33168  isosctrlem1ALT  33734  sineq0ALT  33737  taupi  37698  imo72b2lem0  37982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-2 10619
  Copyright terms: Public domain W3C validator