Theorem 2re 12199

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 12188	. 2 ⊢ 2 = (1 + 1)
2		1re 11112	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11127	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2827	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005  1c1 11007   + caddc 11009  2c2 12180

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-2 12188

This theorem is referenced by:  2cnALT  12201  3re  12205  3pos  12230  2lt3  12292  1lt3  12293  2lt4  12295  1lt4  12296  2lt5  12299  2lt6  12304  1lt6  12305  2lt7  12310  1lt7  12311  2lt8  12317  1lt8  12318  2lt9  12325  1lt9  12326  1le2  12329  2rene0  12331  halfre  12334  halfgt0  12336  halflt1  12338  rehalfcl  12348  halfpos2  12350  halfnneg2  12352  addltmul  12357  nominpos  12358  avglt1  12359  avglt2  12360  div4p1lem1div2  12376  nn0lele2xi  12437  nn0n0n1ge2b  12450  nn0ge2m1nn  12451  nn0le2is012  12537  halfnz  12551  3halfnz  12552  2lt10  12726  1lt10  12727  uzuzle23  12782  uzuzle24  12783  uz3m2nn  12792  2rp  12895  ge2halflem1  13007  xnn0n0n1ge2b  13031  fztpval  13486  fz0to4untppr  13530  fz0to5un2tp  13531  fzo0to42pr  13653  flhalf  13734  fldiv4p1lem1div2  13739  2txmodxeq0  13838  expubnd  14085  expmulnbnd  14142  nn0opthlem2  14176  faclbnd2  14198  faclbnd4lem1  14200  faclbnd5  14205  4bc2eq6  14236  hashgt23el  14331  hashfun  14344  hashge2el2dif  14387  hashge2el2difr  14388  hash3tpde  14400  wrdlenge2n0  14459  f1oun2prg  14824  01sqrexlem7  15155  sqrt4  15179  sqrt2gt1lt2  15181  abstri  15238  sqreulem  15267  amgm2  15277  caucvgrlem  15580  climcndslem1  15756  climcndslem2  15757  climcnds  15758  efcllem  15984  ege2le3  15997  ef01bndlem  16093  cos01bnd  16095  cos2bnd  16097  cos01gt0  16100  sin02gt0  16101  sincos2sgn  16103  sin4lt0  16104  eirrlem  16113  egt2lt3  16115  epos  16116  ene1  16119  sqrt2re  16159  mod2eq1n2dvds  16258  oddge22np1  16260  evennn2n  16262  nn0o1gt2  16292  nno  16293  nn0o  16294  nnoddm1d2  16297  bitsp1o  16344  bitsfzolem  16345  bitsfzo  16346  bitsfi  16348  6gcd4e2  16449  2mulprm  16604  ge2nprmge4  16612  isprm7  16619  3lcm2e6  16643  prmreclem2  16829  prmreclem6  16833  4sqlem11  16867  4sqlem12  16868  prmgaplem7  16969  2expltfac  17004  plusgndxnmulrndx  17201  starvndxnplusgndx  17209  scandxnplusgndx  17221  vscandxnplusgndx  17226  ipndxnplusgndx  17237  tsetndxnplusgndx  17261  plendxnplusgndx  17275  dsndxnplusgndx  17294  slotsdifunifndx  17305  efgredleme  19655  zringndrg  21405  chfacfscmul0  22773  chfacfpmmul0  22777  psmetge0  24227  xmetge0  24259  bl2in  24315  metnrmlem3  24777  iihalf1  24852  iihalf2  24855  pcoass  24951  tcphcphlem1  25162  csbren  25326  trirn  25327  minveclem2  25353  minveclem4  25359  pjthlem1  25364  ovolunlem1a  25424  dyadss  25522  opnmbllem  25529  vitalilem2  25537  vitalilem4  25539  mbfi1fseqlem5  25647  lhop1lem  25945  aaliou3lem2  26278  aaliou3lem8  26280  pilem2  26389  pilem3  26390  pipos  26395  sinhalfpilem  26399  sincosq1lem  26433  sincosq4sgn  26437  tangtx  26441  sinq12gt0  26443  sincos4thpi  26449  tan4thpi  26450  tan4thpiOLD  26451  sincos6thpi  26452  sineq0  26460  cos02pilt1  26462  cosq34lt1  26463  cosordlem  26466  cos0pilt1  26468  tanord1  26473  efif1olem1  26478  efif1olem2  26479  efif1olem4  26481  efif1o  26482  efifo  26483  2irrexpq  26667  cxpcn3lem  26684  root1id  26691  root1eq1  26692  root1cj  26693  cxpeq  26694  2logb9irr  26732  2logb3irr  26734  ang180lem1  26746  ang180lem2  26747  chordthmlem2  26770  1cubrlem  26778  atancj  26847  atantan  26860  atanbndlem  26862  atans2  26868  leibpi  26879  log2tlbnd  26882  log2ublem2  26884  log2ub  26886  divsqrtsumlem  26917  harmonicbnd3  26945  zetacvg  26952  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem4  26969  lgamgulmlem6  26971  lgamucov  26975  basellem1  27018  basellem2  27019  basellem3  27020  basellem5  27022  chtdif  27095  ppidif  27100  ppinncl  27111  chtrpcl  27112  ppieq0  27113  ppiltx  27114  ppiublem1  27140  ppiub  27142  chpeq0  27146  chteq0  27147  chtublem  27149  chtub  27150  chpval2  27156  chpub  27158  mersenne  27165  perfectlem1  27167  perfectlem2  27168  dchrptlem1  27202  dchrptlem2  27203  bcmono  27215  bclbnd  27218  bpos1lem  27220  bposlem1  27222  bposlem2  27223  bposlem3  27224  bposlem4  27225  bposlem5  27226  bposlem6  27227  bposlem7  27228  bposlem8  27229  bposlem9  27230  lgslem1  27235  lgsdirprm  27269  gausslemma2dlem0c  27296  gausslemma2dlem1a  27303  gausslemma2dlem2  27305  gausslemma2dlem3  27306  lgseisenlem1  27313  lgseisenlem2  27314  lgseisenlem3  27315  lgseisen  27317  lgsquadlem1  27318  lgsquadlem2  27319  m1lgs  27326  2lgslem1a1  27327  2lgslem1a2  27328  2lgslem1c  27331  2lgslem4  27344  2sqlem11  27367  2sq2  27371  2sqreultlem  27385  2sqreunnltlem  27388  chebbnd1lem1  27407  chebbnd1lem2  27408  chebbnd1lem3  27409  chebbnd1  27410  chtppilimlem1  27411  chtppilimlem2  27412  chtppilim  27413  chto1ub  27414  chebbnd2  27415  chto1lb  27416  chpchtlim  27417  chpo1ub  27418  chpo1ubb  27419  rplogsumlem1  27422  rplogsumlem2  27423  dchrisumlem2  27428  dchrisumlem3  27429  dchrvmasumiflem1  27439  dchrisum0fno1  27449  dchrisum0re  27451  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2  27456  rplogsum  27465  mulog2sumlem1  27472  mulog2sumlem2  27473  log2sumbnd  27482  selberglem2  27484  selbergb  27487  selberg2b  27490  chpdifbndlem1  27491  logdivbnd  27494  selberg3lem1  27495  selberg3  27497  selberg4lem1  27498  selberg4  27499  pntrmax  27502  pntrsumbnd2  27505  selberg3r  27507  selberg4r  27508  selberg34r  27509  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntpbnd  27526  pntibndlem2  27529  pntibndlem3  27530  pntibnd  27531  pntlemb  27535  pntlemg  27536  pntlemh  27537  pntlemr  27540  pntlemk  27544  pntlemo  27545  pnt2  27551  pnt  27552  ostth2lem1  27556  ostth3  27576  slotsinbpsd  28419  slotslnbpsd  28420  istrkg3ld  28439  tgldimor  28480  trgcgrg  28493  tgcgr4  28509  axlowdimlem6  28925  axlowdimlem16  28935  axlowdimlem17  28936  axlowdim  28939  upgrfi  29069  umgrupgr  29081  umgrislfupgrlem  29100  umgrislfupgr  29101  lfgrnloop  29103  usgruspgr  29158  usgrislfuspgr  29165  lfuhgr1v0e  29232  usgrexmpldifpr  29236  usgrexmplef  29237  nbusgrvtxm1  29357  vdegp1bi  29516  upgrewlkle2  29585  lfgrwlkprop  29664  upgr2pthnlp  29710  usgr2pthlem  29741  pthdlem1  29744  wwlksm1edg  29859  wwlksnextwrd  29875  wwlksnextfun  29876  wwlksnextinj  29877  wwlksnextproplem3  29889  clwlkclwwlklem2a1  29972  clwlkclwwlklem2a2  29973  clwlkclwwlklem2fv1  29975  clwlkclwwlklem2fv2  29976  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  clwlkclwwlklem2  29980  clwlkclwwlk2  29983  clwlkclwwlkf  29988  clwwlkext2edg  30036  konigsbergiedgw  30228  konigsbergssiedgw  30230  konigsberglem1  30232  konigsberglem2  30233  konigsberglem3  30234  konigsberg  30237  frgrreggt1  30373  ex-pss  30408  ex-res  30421  ex-fv  30423  ex-fl  30427  ex-mod  30429  ex-abs  30435  nrt2irr  30453  ipidsq  30690  minvecolem2  30855  minvecolem4  30860  normlem7  31096  norm-ii-i  31117  norm3lemt  31132  normpar2i  31136  bcsiALT  31159  pjhthlem1  31371  opsqrlem6  32125  cdj3lem1  32414  addltmulALT  32426  nexple  32827  2exple2exp  32828  threehalves  32895  pfx1s2  32920  wrdt2ind  32934  cyc3conja  33126  drngidlhash  33399  evl1deg3  33541  rtelextdg2lem  33739  fldext2chn  33741  constraddcl  33775  iconstr  33779  2sqr3minply  33793  2sqr3nconstr  33794  cos9thpinconstrlem1  33802  cos9thpinconstrlem2  33803  sqsscirc1  33921  dya2iocucvr  34297  omssubadd  34313  oddpwdc  34367  eulerpartlemgc  34375  fibp1  34414  coinfliplem  34492  coinflipspace  34494  ballotlem2  34502  signstfveq0  34590  prodfzo03  34616  hgt750lemd  34661  logdivsqrle  34663  hgt750lem  34664  hgt750lem2  34665  hgt750leme  34671  lfuhgr2  35163  usgrcyclgt2v  35175  acycgr2v  35194  subfacp1lem1  35223  subfacp1lem5  35228  subfacval3  35233  problem2  35710  problem5  35713  circum  35718  nn0prpwlem  36364  dnibndlem10  36529  knoppcnlem2  36536  knoppcnlem4  36538  knoppcnlem10  36544  unbdqndv2lem1  36551  knoppndvlem1  36554  knoppndvlem10  36563  knoppndvlem11  36564  knoppndvlem12  36565  knoppndvlem14  36567  knoppndvlem15  36568  knoppndvlem17  36570  knoppndvlem18  36571  knoppndvlem19  36572  knoppndvlem20  36573  knoppndvlem21  36574  cnndvlem1  36579  taupi  37365  iccioo01  37369  relowlpssretop  37406  sin2h  37658  cos2h  37659  tan2h  37660  poimirlem7  37675  poimirlem9  37677  opnmbllem0  37704  mblfinlem1  37705  mblfinlem2  37706  itg2addnclem  37719  isbnd2  37831  isbnd3  37832  heiborlem7  37865  12gcd5e1  42044  lcm2un  42055  lcmineqlem19  42088  lcmineqlem20  42089  lcmineqlem22  42091  3lexlogpow5ineq2  42096  3lexlogpow5ineq4  42097  3lexlogpow5ineq3  42098  3lexlogpow2ineq1  42099  3lexlogpow2ineq2  42100  3lexlogpow5ineq5  42101  aks4d1lem1  42103  aks4d1p1p3  42110  aks4d1p1p2  42111  aks4d1p1p4  42112  aks4d1p1p6  42114  aks4d1p1p7  42115  aks4d1p1p5  42116  aks4d1p1  42117  aks4d1p2  42118  aks4d1p3  42119  aks4d1p5  42121  aks4d1p6  42122  aks4d1p7d1  42123  aks4d1p7  42124  aks4d1p8  42128  aks4d1p9  42129  posbezout  42141  aks6d1c3  42164  2np3bcnp1  42185  2ap1caineq  42186  aks6d1c6lem4  42214  aks6d1c7lem1  42221  aks6d1c7lem2  42222  oexpreposd  42363  asin1half  42398  remul02  42446  sn-0ne2  42447  remul01  42448  flt4lem7  42700  rabren3dioph  42856  pellexlem2  42871  pellexlem5  42874  pell14qrgapw  42917  pellfundex  42927  rmspecsqrtnq  42947  jm2.24nn  43000  jm2.17a  43001  jm2.17b  43002  jm2.17c  43003  acongrep  43021  acongeq  43024  jm2.22  43036  jm2.23  43037  jm2.20nn  43038  jm3.1lem2  43059  expdiophlem1  43062  sqrtcval  43682  imo72b2lem0  44206  lhe4.4ex1a  44370  isosctrlem1ALT  44974  sineq0ALT  44977  lt3addmuld  45350  suplesup  45386  infleinflem2  45417  infleinf  45418  sumnnodd  45678  0ellimcdiv  45695  sinaover2ne0  45914  stoweidlem13  46059  stoweidlem14  46060  stoweidlem26  46072  stoweidlem49  46095  stoweidlem52  46098  wallispilem4  46114  wallispilem5  46115  wallispi  46116  wallispi2lem1  46117  wallispi2lem2  46118  wallispi2  46119  stirlinglem1  46120  stirlinglem3  46122  stirlinglem5  46124  stirlinglem6  46125  stirlinglem7  46126  stirlinglem10  46129  stirlinglem11  46130  stirlinglem15  46134  stirlingr  46136  dirker2re  46138  dirkerval2  46140  dirkerre  46141  dirkerper  46142  dirkertrigeqlem1  46144  dirkertrigeqlem3  46146  dirkercncflem1  46149  dirkercncflem2  46150  dirkercncflem4  46152  fourierdlem24  46177  fourierdlem43  46196  fourierdlem44  46197  fourierdlem57  46209  fourierdlem58  46210  fourierdlem62  46214  fourierdlem66  46218  fourierdlem68  46220  fourierdlem72  46224  fourierdlem76  46228  fourierdlem78  46230  fourierdlem79  46231  fourierdlem94  46246  fourierdlem103  46255  fourierdlem104  46256  fourierdlem111  46263  fourierdlem113  46265  sqwvfoura  46274  sqwvfourb  46275  fourierswlem  46276  fouriersw  46277  etransclem23  46303  salexct2  46385  salexct3  46388  salgencntex  46389  salgensscntex  46390  sge0ad2en  46477  ovnsubaddlem1  46616  smfmullem4  46840  smf2id  46847  2leaddle2  47337  p1lep2  47339  2ltceilhalf  47367  ceilhalfgt1  47368  2tceilhalfelfzo1  47371  rehalfge1  47374  ceilhalfnn  47375  ceil5half3  47379  difmodm1lt  47398  fmtnoge3  47569  fmtnof1  47574  fmtnoprmfac2lem1  47605  fmtno4prmfac  47611  fmtno4prm  47614  2pwp1prm  47628  31prm  47636  sfprmdvdsmersenne  47642  lighneallem2  47645  lighneallem4a  47647  lighneallem4b  47648  requad01  47660  requad1  47661  requad2  47662  dfodd4  47698  nn0o1gt2ALTV  47733  nnoALTV  47734  nn0oALTV  47735  nn0e  47736  nneven  47737  perfectALTVlem1  47760  perfectALTVlem2  47761  341fppr2  47773  9fppr8  47776  fpprel2  47780  nfermltl2rev  47782  gbowgt5  47801  sbgoldbalt  47820  sgoldbeven3prm  47822  mogoldbb  47824  nnsum3primes4  47827  nnsum3primesgbe  47831  nnsum3primesle9  47833  nnsum4primesodd  47835  nnsum4primesoddALTV  47836  wtgoldbnnsum4prm  47841  bgoldbnnsum3prm  47843  cycl3grtri  47986  usgrexmpl1lem  48060  usgrexmpl2lem  48065  usgrexmpl2nb2  48072  usgrexmpl2nb3  48073  usgrexmpl2nb4  48074  usgrexmpl2nb5  48075  usgrexmpl2trifr  48076  gpgprismgrusgra  48097  gpg5nbgrvtx13starlem2  48111  gpg3nbgrvtx0  48115  gpg3kgrtriexlem1  48122  cznnring  48301  ply1mulgsumlem2  48427  zlmodzxznm  48537  zlmodzxzldeplem  48538  nn0eo  48568  flnn0div2ge  48573  rege1logbzge0  48599  fldivexpfllog2  48605  logbpw2m1  48607  fllog2  48608  blenpw2m1  48619  nnpw2blen  48620  nnolog2flm1  48630  blennngt2o2  48632  dig2nn1st  48645  dig2nn0  48651  dig2bits  48654  dignn0flhalflem1  48655  dignn0flhalflem2  48656  dignn0flhalf  48658  nn0sumshdiglemA  48659  ackval42  48736  rrx2xpref1o  48758  itscnhlc0yqe  48799  itsclquadb  48816  2itscp  48821  itscnhlinecirc02p  48825  sepfsepc  48967