Theorem 2re 12260

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 12249	. 2 ⊢ 2 = (1 + 1)
2		1re 11174	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11189	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2824	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071  2c2 12241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249

This theorem is referenced by:  2cnALT  12262  3re  12266  3pos  12291  2lt3  12353  1lt3  12354  2lt4  12356  1lt4  12357  2lt5  12360  2lt6  12365  1lt6  12366  2lt7  12371  1lt7  12372  2lt8  12378  1lt8  12379  2lt9  12386  1lt9  12387  1le2  12390  2rene0  12392  halfre  12395  halfgt0  12397  halflt1  12399  rehalfcl  12409  halfpos2  12411  halfnneg2  12413  addltmul  12418  nominpos  12419  avglt1  12420  avglt2  12421  div4p1lem1div2  12437  nn0lele2xi  12498  nn0n0n1ge2b  12511  nn0ge2m1nn  12512  nn0le2is012  12598  halfnz  12612  3halfnz  12613  2lt10  12787  1lt10  12788  uzuzle23  12843  uzuzle24  12844  uz3m2nn  12853  2rp  12956  ge2halflem1  13068  xnn0n0n1ge2b  13092  fztpval  13547  fz0to4untppr  13591  fz0to5un2tp  13592  fzo0to42pr  13714  flhalf  13792  fldiv4p1lem1div2  13797  2txmodxeq0  13896  expubnd  14143  expmulnbnd  14200  nn0opthlem2  14234  faclbnd2  14256  faclbnd4lem1  14258  faclbnd5  14263  4bc2eq6  14294  hashgt23el  14389  hashfun  14402  hashge2el2dif  14445  hashge2el2difr  14446  hash3tpde  14458  wrdlenge2n0  14517  f1oun2prg  14883  01sqrexlem7  15214  sqrt4  15238  sqrt2gt1lt2  15240  abstri  15297  sqreulem  15326  amgm2  15336  caucvgrlem  15639  climcndslem1  15815  climcndslem2  15816  climcnds  15817  efcllem  16043  ege2le3  16056  ef01bndlem  16152  cos01bnd  16154  cos2bnd  16156  cos01gt0  16159  sin02gt0  16160  sincos2sgn  16162  sin4lt0  16163  eirrlem  16172  egt2lt3  16174  epos  16175  ene1  16178  sqrt2re  16218  mod2eq1n2dvds  16317  oddge22np1  16319  evennn2n  16321  nn0o1gt2  16351  nno  16352  nn0o  16353  nnoddm1d2  16356  bitsp1o  16403  bitsfzolem  16404  bitsfzo  16405  bitsfi  16407  6gcd4e2  16508  2mulprm  16663  ge2nprmge4  16671  isprm7  16678  3lcm2e6  16702  prmreclem2  16888  prmreclem6  16892  4sqlem11  16926  4sqlem12  16927  prmgaplem7  17028  2expltfac  17063  plusgndxnmulrndx  17260  starvndxnplusgndx  17268  scandxnplusgndx  17280  vscandxnplusgndx  17285  ipndxnplusgndx  17296  tsetndxnplusgndx  17320  plendxnplusgndx  17334  dsndxnplusgndx  17353  slotsdifunifndx  17364  efgredleme  19673  zringndrg  21378  chfacfscmul0  22745  chfacfpmmul0  22749  psmetge0  24200  xmetge0  24232  bl2in  24288  metnrmlem3  24750  iihalf1  24825  iihalf2  24828  pcoass  24924  tcphcphlem1  25135  csbren  25299  trirn  25300  minveclem2  25326  minveclem4  25332  pjthlem1  25337  ovolunlem1a  25397  dyadss  25495  opnmbllem  25502  vitalilem2  25510  vitalilem4  25512  mbfi1fseqlem5  25620  lhop1lem  25918  aaliou3lem2  26251  aaliou3lem8  26253  pilem2  26362  pilem3  26363  pipos  26368  sinhalfpilem  26372  sincosq1lem  26406  sincosq4sgn  26410  tangtx  26414  sinq12gt0  26416  sincos4thpi  26422  tan4thpi  26423  tan4thpiOLD  26424  sincos6thpi  26425  sineq0  26433  cos02pilt1  26435  cosq34lt1  26436  cosordlem  26439  cos0pilt1  26441  tanord1  26446  efif1olem1  26451  efif1olem2  26452  efif1olem4  26454  efif1o  26455  efifo  26456  2irrexpq  26640  cxpcn3lem  26657  root1id  26664  root1eq1  26665  root1cj  26666  cxpeq  26667  2logb9irr  26705  2logb3irr  26707  ang180lem1  26719  ang180lem2  26720  chordthmlem2  26743  1cubrlem  26751  atancj  26820  atantan  26833  atanbndlem  26835  atans2  26841  leibpi  26852  log2tlbnd  26855  log2ublem2  26857  log2ub  26859  divsqrtsumlem  26890  harmonicbnd3  26918  zetacvg  26925  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem6  26944  lgamucov  26948  basellem1  26991  basellem2  26992  basellem3  26993  basellem5  26995  chtdif  27068  ppidif  27073  ppinncl  27084  chtrpcl  27085  ppieq0  27086  ppiltx  27087  ppiublem1  27113  ppiub  27115  chpeq0  27119  chteq0  27120  chtublem  27122  chtub  27123  chpval2  27129  chpub  27131  mersenne  27138  perfectlem1  27140  perfectlem2  27141  dchrptlem1  27175  dchrptlem2  27176  bcmono  27188  bclbnd  27191  bpos1lem  27193  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem7  27201  bposlem8  27202  bposlem9  27203  lgslem1  27208  lgsdirprm  27242  gausslemma2dlem0c  27269  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem3  27279  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  m1lgs  27299  2lgslem1a1  27300  2lgslem1a2  27301  2lgslem1c  27304  2lgslem4  27317  2sqlem11  27340  2sq2  27344  2sqreultlem  27358  2sqreunnltlem  27361  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chtppilimlem2  27385  chtppilim  27386  chto1ub  27387  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ub  27391  chpo1ubb  27392  rplogsumlem1  27395  rplogsumlem2  27396  dchrisumlem2  27401  dchrisumlem3  27402  dchrvmasumiflem1  27412  dchrisum0fno1  27422  dchrisum0re  27424  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2  27429  rplogsum  27438  mulog2sumlem1  27445  mulog2sumlem2  27446  log2sumbnd  27455  selberglem2  27457  selbergb  27460  selberg2b  27463  chpdifbndlem1  27464  logdivbnd  27467  selberg3lem1  27468  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrmax  27475  pntrsumbnd2  27478  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntpbnd  27499  pntibndlem2  27502  pntibndlem3  27503  pntibnd  27504  pntlemb  27508  pntlemg  27509  pntlemh  27510  pntlemr  27513  pntlemk  27517  pntlemo  27518  pnt2  27524  pnt  27525  ostth2lem1  27529  ostth3  27549  slotsinbpsd  28368  slotslnbpsd  28369  istrkg3ld  28388  tgldimor  28429  trgcgrg  28442  tgcgr4  28458  axlowdimlem6  28874  axlowdimlem16  28884  axlowdimlem17  28885  axlowdim  28888  upgrfi  29018  umgrupgr  29030  umgrislfupgrlem  29049  umgrislfupgr  29050  lfgrnloop  29052  usgruspgr  29107  usgrislfuspgr  29114  lfuhgr1v0e  29181  usgrexmpldifpr  29185  usgrexmplef  29186  nbusgrvtxm1  29306  vdegp1bi  29465  upgrewlkle2  29534  lfgrwlkprop  29615  upgr2pthnlp  29662  usgr2pthlem  29693  pthdlem1  29696  wwlksm1edg  29811  wwlksnextwrd  29827  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextproplem3  29841  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a2  29922  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlk2  29932  clwlkclwwlkf  29937  clwwlkext2edg  29985  konigsbergiedgw  30177  konigsbergssiedgw  30179  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  konigsberg  30186  frgrreggt1  30322  ex-pss  30357  ex-res  30370  ex-fv  30372  ex-fl  30376  ex-mod  30378  ex-abs  30384  nrt2irr  30402  ipidsq  30639  minvecolem2  30804  minvecolem4  30809  normlem7  31045  norm-ii-i  31066  norm3lemt  31081  normpar2i  31085  bcsiALT  31108  pjhthlem1  31320  opsqrlem6  32074  cdj3lem1  32363  addltmulALT  32375  nexple  32769  2exple2exp  32770  threehalves  32835  pfx1s2  32860  wrdt2ind  32875  cyc3conja  33114  drngidlhash  33405  evl1deg3  33547  rtelextdg2lem  33716  fldext2chn  33718  constraddcl  33752  iconstr  33756  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpinconstrlem1  33779  cos9thpinconstrlem2  33780  sqsscirc1  33898  dya2iocucvr  34275  omssubadd  34291  oddpwdc  34345  eulerpartlemgc  34353  fibp1  34392  coinfliplem  34470  coinflipspace  34472  ballotlem2  34480  signstfveq0  34568  prodfzo03  34594  hgt750lemd  34639  logdivsqrle  34641  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  lfuhgr2  35106  usgrcyclgt2v  35118  acycgr2v  35137  subfacp1lem1  35166  subfacp1lem5  35171  subfacval3  35176  problem2  35653  problem5  35656  circum  35661  nn0prpwlem  36310  dnibndlem10  36475  knoppcnlem2  36482  knoppcnlem4  36484  knoppcnlem10  36490  unbdqndv2lem1  36497  knoppndvlem1  36500  knoppndvlem10  36509  knoppndvlem11  36510  knoppndvlem12  36511  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem18  36517  knoppndvlem19  36518  knoppndvlem20  36519  knoppndvlem21  36520  cnndvlem1  36525  taupi  37311  iccioo01  37315  relowlpssretop  37352  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem7  37621  poimirlem9  37623  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  itg2addnclem  37665  isbnd2  37777  isbnd3  37778  heiborlem7  37811  12gcd5e1  41991  lcm2un  42002  lcmineqlem19  42035  lcmineqlem20  42036  lcmineqlem22  42038  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  aks6d1c3  42111  2np3bcnp1  42132  2ap1caineq  42133  aks6d1c6lem4  42161  aks6d1c7lem1  42168  aks6d1c7lem2  42169  oexpreposd  42310  asin1half  42345  remul02  42393  sn-0ne2  42394  remul01  42395  flt4lem7  42647  rabren3dioph  42803  pellexlem2  42818  pellexlem5  42821  pell14qrgapw  42864  pellfundex  42874  rmspecsqrtnq  42894  jm2.24nn  42948  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  acongrep  42969  acongeq  42972  jm2.22  42984  jm2.23  42985  jm2.20nn  42986  jm3.1lem2  43007  expdiophlem1  43010  sqrtcval  43630  imo72b2lem0  44154  lhe4.4ex1a  44318  isosctrlem1ALT  44923  sineq0ALT  44926  lt3addmuld  45299  suplesup  45335  infleinflem2  45367  infleinf  45368  sumnnodd  45628  0ellimcdiv  45647  sinaover2ne0  45866  stoweidlem13  46011  stoweidlem14  46012  stoweidlem26  46024  stoweidlem49  46047  stoweidlem52  46050  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem15  46086  stirlingr  46088  dirker2re  46090  dirkerval2  46092  dirkerre  46093  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem24  46129  fourierdlem43  46148  fourierdlem44  46149  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem66  46170  fourierdlem68  46172  fourierdlem72  46176  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem113  46217  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  etransclem23  46255  salexct2  46337  salexct3  46340  salgencntex  46341  salgensscntex  46342  sge0ad2en  46429  ovnsubaddlem1  46568  smfmullem4  46792  smf2id  46799  2leaddle2  47299  p1lep2  47301  2ltceilhalf  47329  ceilhalfgt1  47330  2tceilhalfelfzo1  47333  rehalfge1  47336  ceilhalfnn  47337  ceil5half3  47341  difmodm1lt  47360  fmtnoge3  47531  fmtnof1  47536  fmtnoprmfac2lem1  47567  fmtno4prmfac  47573  fmtno4prm  47576  2pwp1prm  47590  31prm  47598  sfprmdvdsmersenne  47604  lighneallem2  47607  lighneallem4a  47609  lighneallem4b  47610  requad01  47622  requad1  47623  requad2  47624  dfodd4  47660  nn0o1gt2ALTV  47695  nnoALTV  47696  nn0oALTV  47697  nn0e  47698  nneven  47699  perfectALTVlem1  47722  perfectALTVlem2  47723  341fppr2  47735  9fppr8  47738  fpprel2  47742  nfermltl2rev  47744  gbowgt5  47763  sbgoldbalt  47782  sgoldbeven3prm  47784  mogoldbb  47786  nnsum3primes4  47789  nnsum3primesgbe  47793  nnsum3primesle9  47795  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  cycl3grtri  47946  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  gpgprismgrusgra  48049  gpg5nbgrvtx13starlem2  48063  gpg3nbgrvtx0  48067  gpg3kgrtriexlem1  48074  cznnring  48250  ply1mulgsumlem2  48376  zlmodzxznm  48486  zlmodzxzldeplem  48487  nn0eo  48517  flnn0div2ge  48522  rege1logbzge0  48548  fldivexpfllog2  48554  logbpw2m1  48556  fllog2  48557  blenpw2m1  48568  nnpw2blen  48569  nnolog2flm1  48579  blennngt2o2  48581  dig2nn1st  48594  dig2nn0  48600  dig2bits  48603  dignn0flhalflem1  48604  dignn0flhalflem2  48605  dignn0flhalf  48607  nn0sumshdiglemA  48608  ackval42  48685  rrx2xpref1o  48707  itscnhlc0yqe  48748  itsclquadb  48765  2itscp  48770  itscnhlinecirc02p  48774  sepfsepc  48916