Theorem 2re 11712

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	⊢ 2 ∈ ℝ

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 11701	. 2 ⊢ 2 = (1 + 1)
2		1re 10641	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 10656	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2909	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7156  ℝcr 10536  1c1 10538   + caddc 10540  2c2 11693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  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 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-2 11701

This theorem is referenced by:  2cnALT  11714  3re  11718  2ne0  11742  3pos  11743  2lt3  11810  1lt3  11811  2lt4  11813  1lt4  11814  2lt5  11817  2lt6  11822  1lt6  11823  2lt7  11828  1lt7  11829  2lt8  11835  1lt8  11836  2lt9  11843  1lt9  11844  1le2  11847  2rene0  11849  halfre  11852  halfgt0  11854  halflt1  11856  rehalfcl  11864  halfpos2  11867  halfnneg2  11869  addltmul  11874  nominpos  11875  avglt1  11876  avglt2  11877  div4p1lem1div2  11893  nn0lele2xi  11953  nn0n0n1ge2b  11964  nn0ge2m1nn  11965  nn0le2is012  12047  halfnz  12061  3halfnz  12062  2lt10  12237  1lt10  12238  eluz4eluz2  12286  uzuzle23  12290  uz3m2nn  12292  2rp  12395  xnn0n0n1ge2b  12527  fztpval  12970  fz0to4untppr  13011  fzo0to42pr  13125  flhalf  13201  fldiv4p1lem1div2  13206  2txmodxeq0  13300  expubnd  13542  expmulnbnd  13597  nn0opthlem2  13630  faclbnd2  13652  faclbnd4lem1  13654  faclbnd5  13659  4bc2eq6  13690  hashgt23el  13786  hashfun  13799  hashge2el2dif  13839  hashge2el2difr  13840  wrdlenge2n0  13904  f1oun2prg  14279  sqrlem7  14608  sqrt4  14632  sqrt2gt1lt2  14634  abstri  14690  sqreulem  14719  amgm2  14729  caucvgrlem  15029  climcndslem1  15204  climcndslem2  15205  climcnds  15206  efcllem  15431  ege2le3  15443  ef01bndlem  15537  cos01bnd  15539  cos2bnd  15541  cos01gt0  15544  sin02gt0  15545  sincos2sgn  15547  sin4lt0  15548  eirrlem  15557  egt2lt3  15559  epos  15560  ene1  15563  sqrt2re  15603  mod2eq1n2dvds  15696  oddge22np1  15698  evennn2n  15700  n2dvds1OLD  15718  nn0o1gt2  15732  nno  15733  nn0o  15734  nnoddm1d2  15737  bitsp1o  15782  bitsfzolem  15783  bitsfzo  15784  bitsfi  15786  6gcd4e2  15886  2mulprm  16037  ge2nprmge4  16045  isprm7  16052  3lcm2e6  16072  prmreclem2  16253  prmreclem6  16257  4sqlem11  16291  4sqlem12  16292  prmgaplem7  16393  2expltfac  16426  plusgndxnmulrndx  16617  oppgtset  18480  efgredleme  18869  mgpsca  19246  mgptset  19247  mgpds  19249  rmodislmod  19702  cnfldfun  20557  zringndrg  20637  chfacfscmul0  21466  chfacfpmmul0  21470  psmetge0  22922  xmetge0  22954  bl2in  23010  metnrmlem3  23469  iihalf1  23535  iihalf2  23537  pcoass  23628  tcphcphlem1  23838  csbren  24002  trirn  24003  minveclem2  24029  minveclem4  24035  pjthlem1  24040  ovolunlem1a  24097  dyadss  24195  opnmbllem  24202  vitalilem2  24210  vitalilem4  24212  mbfi1fseqlem5  24320  lhop1lem  24610  aaliou3lem2  24932  aaliou3lem8  24934  pilem2  25040  pilem3  25041  pipos  25046  sinhalfpilem  25049  sincosq1lem  25083  sincosq4sgn  25087  tangtx  25091  sinq12gt0  25093  sincos4thpi  25099  tan4thpi  25100  sincos6thpi  25101  sineq0  25109  cos02pilt1  25111  cosq34lt1  25112  cosordlem  25115  tanord1  25121  efif1olem1  25126  efif1olem2  25127  efif1olem4  25129  efif1o  25130  efifo  25131  2irrexpq  25313  cxpcn3lem  25328  root1id  25335  root1eq1  25336  root1cj  25337  cxpeq  25338  2logb9irr  25373  2logb3irr  25375  ang180lem1  25387  ang180lem2  25388  chordthmlem2  25411  1cubrlem  25419  atancj  25488  atantan  25501  atanbndlem  25503  atans2  25509  leibpi  25520  log2tlbnd  25523  log2ublem2  25525  log2ub  25527  divsqrtsumlem  25557  harmonicbnd3  25585  zetacvg  25592  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem6  25611  lgamucov  25615  basellem1  25658  basellem2  25659  basellem3  25660  basellem5  25662  chtdif  25735  ppidif  25740  ppinncl  25751  chtrpcl  25752  ppieq0  25753  ppiltx  25754  ppiublem1  25778  ppiub  25780  chpeq0  25784  chteq0  25785  chtublem  25787  chtub  25788  chpval2  25794  chpub  25796  mersenne  25803  perfectlem1  25805  perfectlem2  25806  dchrptlem1  25840  dchrptlem2  25841  bcmono  25853  bclbnd  25856  bpos1lem  25858  bposlem1  25860  bposlem2  25861  bposlem3  25862  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem7  25866  bposlem8  25867  bposlem9  25868  lgslem1  25873  lgsdirprm  25907  gausslemma2dlem0c  25934  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem3  25944  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  m1lgs  25964  2lgslem1a1  25965  2lgslem1a2  25966  2lgslem1c  25969  2lgslem4  25982  2sqlem11  26005  2sq2  26009  2sqreultlem  26023  2sqreunnltlem  26026  chebbnd1lem1  26045  chebbnd1lem2  26046  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  chtppilimlem2  26050  chtppilim  26051  chto1ub  26052  chebbnd2  26053  chto1lb  26054  chpchtlim  26055  chpo1ub  26056  chpo1ubb  26057  rplogsumlem1  26060  rplogsumlem2  26061  dchrisumlem2  26066  dchrisumlem3  26067  dchrvmasumiflem1  26077  dchrisum0fno1  26087  dchrisum0re  26089  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2  26094  rplogsum  26103  mulog2sumlem1  26110  mulog2sumlem2  26111  log2sumbnd  26120  selberglem2  26122  selbergb  26125  selberg2b  26128  chpdifbndlem1  26129  logdivbnd  26132  selberg3lem1  26133  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrmax  26140  pntrsumbnd2  26143  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntpbnd  26164  pntibndlem2  26167  pntibndlem3  26168  pntibnd  26169  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemr  26178  pntlemk  26182  pntlemo  26183  pnt2  26189  pnt  26190  ostth2lem1  26194  ostth3  26214  istrkg3ld  26247  tgldimor  26288  trgcgrg  26301  tgcgr4  26317  axlowdimlem6  26733  axlowdimlem16  26743  axlowdimlem17  26744  axlowdim  26747  upgrfi  26876  umgrupgr  26888  umgrislfupgrlem  26907  umgrislfupgr  26908  lfgrnloop  26910  usgruspgr  26963  usgrislfuspgr  26969  lfuhgr1v0e  27036  usgrexmpldifpr  27040  usgrexmplef  27041  nbusgrvtxm1  27161  vdegp1bi  27319  upgrewlkle2  27388  lfgrwlkprop  27469  upgr2pthnlp  27513  usgr2pthlem  27544  pthdlem1  27547  wwlksm1edg  27659  wwlksnextwrd  27675  wwlksnextfun  27676  wwlksnextinj  27677  wwlksnextproplem3  27690  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a2  27771  clwlkclwwlklem2fv1  27773  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlk2  27781  clwlkclwwlkf  27786  clwwlkext2edg  27835  konigsbergiedgw  28027  konigsbergssiedgw  28029  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033  konigsberg  28036  frgrreggt1  28172  ex-pss  28207  ex-res  28220  ex-fv  28222  ex-fl  28226  ex-mod  28228  ex-abs  28234  ipidsq  28487  minvecolem2  28652  minvecolem4  28657  normlem7  28893  norm-ii-i  28914  norm3lemt  28929  normpar2i  28933  bcsiALT  28956  pjhthlem1  29168  opsqrlem6  29922  cdj3lem1  30211  addltmulALT  30223  threehalves  30591  pfx1s2  30615  wrdt2ind  30627  oppgle  30640  cyc3conja  30799  resvplusg  30906  sqsscirc1  31151  nexple  31268  dya2iocucvr  31542  omssubadd  31558  oddpwdc  31612  eulerpartlemgc  31620  fibp1  31659  coinfliplem  31736  coinflipspace  31738  ballotlem2  31746  signstfveq0  31847  prodfzo03  31874  hgt750lemd  31919  logdivsqrle  31921  hgt750lem  31922  hgt750lem2  31923  hgt750leme  31929  lfuhgr2  32365  usgrcyclgt2v  32378  acycgr2v  32397  subfacp1lem1  32426  subfacp1lem5  32431  subfacval3  32436  problem2  32909  problem5  32912  circum  32917  nn0prpwlem  33670  dnibndlem10  33826  knoppcnlem2  33833  knoppcnlem4  33835  knoppcnlem10  33841  unbdqndv2lem1  33848  knoppndvlem1  33851  knoppndvlem10  33860  knoppndvlem11  33861  knoppndvlem12  33862  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem18  33868  knoppndvlem19  33869  knoppndvlem20  33870  knoppndvlem21  33871  cnndvlem1  33876  taupi  34607  relowlpssretop  34648  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem7  34914  poimirlem9  34916  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  itg2addnclem  34958  isbnd2  35076  isbnd3  35077  heiborlem7  35110  12gcd5e1  39124  lcm2un  39135  2xp3dxp2ge1d  39146  oexpreposd  39228  remul02  39284  sn-0ne2  39285  remul01  39286  rabren3dioph  39461  pellexlem2  39476  pellexlem5  39479  pell14qrgapw  39522  pellfundex  39532  rmspecsqrtnq  39552  jm2.24nn  39605  jm2.17a  39606  jm2.17b  39607  jm2.17c  39608  acongrep  39626  acongeq  39629  jm2.22  39641  jm2.23  39642  jm2.20nn  39643  jm3.1lem2  39664  expdiophlem1  39667  imo72b2lem0  40565  lhe4.4ex1a  40710  isosctrlem1ALT  41317  sineq0ALT  41320  lt3addmuld  41617  suplesup  41656  infleinflem2  41688  infleinf  41689  sumnnodd  41960  0ellimcdiv  41979  sinaover2ne0  42198  stoweidlem13  42347  stoweidlem14  42348  stoweidlem26  42360  stoweidlem49  42383  stoweidlem52  42386  wallispilem4  42402  wallispilem5  42403  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  wallispi2  42407  stirlinglem1  42408  stirlinglem3  42410  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem10  42417  stirlinglem11  42418  stirlinglem15  42422  stirlingr  42424  dirker2re  42426  dirkerval2  42428  dirkerre  42429  dirkerper  42430  dirkertrigeqlem1  42432  dirkertrigeqlem3  42434  dirkercncflem1  42437  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem24  42465  fourierdlem43  42484  fourierdlem44  42485  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem66  42506  fourierdlem68  42508  fourierdlem72  42512  fourierdlem76  42516  fourierdlem78  42518  fourierdlem79  42519  fourierdlem94  42534  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem113  42553  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  etransclem23  42591  salexct2  42671  salexct3  42674  salgencntex  42675  salgensscntex  42676  sge0ad2en  42762  ovnsubaddlem1  42901  smfmullem4  43118  smf2id  43125  2leaddle2  43547  p1lep2  43549  fmtnoge3  43741  fmtnof1  43746  fmtnoprmfac2lem1  43777  fmtno4prmfac  43783  fmtno4prm  43786  2pwp1prm  43800  31prm  43809  sfprmdvdsmersenne  43817  lighneallem2  43820  lighneallem4a  43822  lighneallem4b  43823  requad01  43835  requad1  43836  requad2  43837  dfodd4  43873  nn0o1gt2ALTV  43908  nnoALTV  43909  nn0oALTV  43910  nn0e  43911  nneven  43912  perfectALTVlem1  43935  perfectALTVlem2  43936  341fppr2  43948  9fppr8  43951  fpprel2  43955  nfermltl2rev  43957  gbowgt5  43976  sbgoldbalt  43995  sgoldbeven3prm  43997  mogoldbb  43999  nnsum3primes4  44002  nnsum3primesgbe  44006  nnsum3primesle9  44008  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  wtgoldbnnsum4prm  44016  bgoldbnnsum3prm  44018  cznnring  44276  ply1mulgsumlem2  44490  zlmodzxznm  44601  zlmodzxzldeplem  44602  difmodm1lt  44631  nn0eo  44637  flnn0div2ge  44642  rege1logbzge0  44668  fldivexpfllog2  44674  logbpw2m1  44676  fllog2  44677  blenpw2m1  44688  nnpw2blen  44689  nnolog2flm1  44699  blennngt2o2  44701  dig2nn1st  44714  dig2nn0  44720  dig2bits  44723  dignn0flhalflem1  44724  dignn0flhalflem2  44725  dignn0flhalf  44727  nn0sumshdiglemA  44728  rrx2xpref1o  44754  itscnhlc0yqe  44795  itsclquadb  44812  2itscp  44817  itscnhlinecirc02p  44821