Theorem 2re 12337

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 12326	. 2 ⊢ 2 = (1 + 1)
2		1re 11258	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11273	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2834	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151  1c1 11153   + caddc 11155  2c2 12318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326

This theorem is referenced by:  2cnALT  12339  3re  12343  2ne0  12367  3pos  12368  2lt3  12435  1lt3  12436  2lt4  12438  1lt4  12439  2lt5  12442  2lt6  12447  1lt6  12448  2lt7  12453  1lt7  12454  2lt8  12460  1lt8  12461  2lt9  12468  1lt9  12469  1le2  12472  2rene0  12474  halfre  12477  halfgt0  12479  halflt1  12481  rehalfcl  12489  halfpos2  12492  halfnneg2  12494  addltmul  12499  nominpos  12500  avglt1  12501  avglt2  12502  div4p1lem1div2  12518  nn0lele2xi  12579  nn0n0n1ge2b  12592  nn0ge2m1nn  12593  nn0le2is012  12679  halfnz  12693  3halfnz  12694  2lt10  12868  1lt10  12869  eluz4eluz2  12922  uzuzle23  12928  uz3m2nn  12930  2rp  13036  ge2halflem1  13147  xnn0n0n1ge2b  13170  fztpval  13622  fz0to4untppr  13666  fz0to5un2tp  13667  fzo0to42pr  13788  flhalf  13866  fldiv4p1lem1div2  13871  2txmodxeq0  13968  expubnd  14213  expmulnbnd  14270  nn0opthlem2  14304  faclbnd2  14326  faclbnd4lem1  14328  faclbnd5  14333  4bc2eq6  14364  hashgt23el  14459  hashfun  14472  hashge2el2dif  14515  hashge2el2difr  14516  hash3tpde  14528  wrdlenge2n0  14586  f1oun2prg  14952  01sqrexlem7  15283  sqrt4  15307  sqrt2gt1lt2  15309  abstri  15365  sqreulem  15394  amgm2  15404  caucvgrlem  15705  climcndslem1  15881  climcndslem2  15882  climcnds  15883  efcllem  16109  ege2le3  16122  ef01bndlem  16216  cos01bnd  16218  cos2bnd  16220  cos01gt0  16223  sin02gt0  16224  sincos2sgn  16226  sin4lt0  16227  eirrlem  16236  egt2lt3  16238  epos  16239  ene1  16242  sqrt2re  16282  mod2eq1n2dvds  16380  oddge22np1  16382  evennn2n  16384  nn0o1gt2  16414  nno  16415  nn0o  16416  nnoddm1d2  16419  bitsp1o  16466  bitsfzolem  16467  bitsfzo  16468  bitsfi  16470  6gcd4e2  16571  2mulprm  16726  ge2nprmge4  16734  isprm7  16741  3lcm2e6  16765  prmreclem2  16950  prmreclem6  16954  4sqlem11  16988  4sqlem12  16989  prmgaplem7  17090  2expltfac  17126  plusgndxnmulrndx  17342  starvndxnplusgndx  17350  scandxnplusgndx  17362  vscandxnplusgndx  17367  ipndxnplusgndx  17378  tsetndxnplusgndx  17402  plendxnplusgndx  17416  dsndxnplusgndx  17435  slotsdifunifndx  17446  oppgtsetOLD  19385  efgredleme  19775  mgpscaOLD  20160  mgptsetOLD  20162  mgpdsOLD  20165  rmodislmodOLD  20945  cnfldfunALTOLDOLD  21410  zringndrg  21496  chfacfscmul0  22879  chfacfpmmul0  22883  psmetge0  24337  xmetge0  24369  bl2in  24425  metnrmlem3  24896  iihalf1  24971  iihalf2  24974  pcoass  25070  tcphcphlem1  25282  csbren  25446  trirn  25447  minveclem2  25473  minveclem4  25479  pjthlem1  25484  ovolunlem1a  25544  dyadss  25642  opnmbllem  25649  vitalilem2  25657  vitalilem4  25659  mbfi1fseqlem5  25768  lhop1lem  26066  aaliou3lem2  26399  aaliou3lem8  26401  pilem2  26510  pilem3  26511  pipos  26516  sinhalfpilem  26519  sincosq1lem  26553  sincosq4sgn  26557  tangtx  26561  sinq12gt0  26563  sincos4thpi  26569  tan4thpi  26570  tan4thpiOLD  26571  sincos6thpi  26572  sineq0  26580  cos02pilt1  26582  cosq34lt1  26583  cosordlem  26586  cos0pilt1  26588  tanord1  26593  efif1olem1  26598  efif1olem2  26599  efif1olem4  26601  efif1o  26602  efifo  26603  2irrexpq  26787  cxpcn3lem  26804  root1id  26811  root1eq1  26812  root1cj  26813  cxpeq  26814  2logb9irr  26852  2logb3irr  26854  ang180lem1  26866  ang180lem2  26867  chordthmlem2  26890  1cubrlem  26898  atancj  26967  atantan  26980  atanbndlem  26982  atans2  26988  leibpi  26999  log2tlbnd  27002  log2ublem2  27004  log2ub  27006  divsqrtsumlem  27037  harmonicbnd3  27065  zetacvg  27072  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem6  27091  lgamucov  27095  basellem1  27138  basellem2  27139  basellem3  27140  basellem5  27142  chtdif  27215  ppidif  27220  ppinncl  27231  chtrpcl  27232  ppieq0  27233  ppiltx  27234  ppiublem1  27260  ppiub  27262  chpeq0  27266  chteq0  27267  chtublem  27269  chtub  27270  chpval2  27276  chpub  27278  mersenne  27285  perfectlem1  27287  perfectlem2  27288  dchrptlem1  27322  dchrptlem2  27323  bcmono  27335  bclbnd  27338  bpos1lem  27340  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem7  27348  bposlem8  27349  bposlem9  27350  lgslem1  27355  lgsdirprm  27389  gausslemma2dlem0c  27416  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  gausslemma2dlem3  27426  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisen  27437  lgsquadlem1  27438  lgsquadlem2  27439  m1lgs  27446  2lgslem1a1  27447  2lgslem1a2  27448  2lgslem1c  27451  2lgslem4  27464  2sqlem11  27487  2sq2  27491  2sqreultlem  27505  2sqreunnltlem  27508  chebbnd1lem1  27527  chebbnd1lem2  27528  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem1  27531  chtppilimlem2  27532  chtppilim  27533  chto1ub  27534  chebbnd2  27535  chto1lb  27536  chpchtlim  27537  chpo1ub  27538  chpo1ubb  27539  rplogsumlem1  27542  rplogsumlem2  27543  dchrisumlem2  27548  dchrisumlem3  27549  dchrvmasumiflem1  27559  dchrisum0fno1  27569  dchrisum0re  27571  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2  27576  rplogsum  27585  mulog2sumlem1  27592  mulog2sumlem2  27593  log2sumbnd  27602  selberglem2  27604  selbergb  27607  selberg2b  27610  chpdifbndlem1  27611  logdivbnd  27614  selberg3lem1  27615  selberg3  27617  selberg4lem1  27618  selberg4  27619  pntrmax  27622  pntrsumbnd2  27625  selberg3r  27627  selberg4r  27628  selberg34r  27629  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntpbnd  27646  pntibndlem2  27649  pntibndlem3  27650  pntibnd  27651  pntlemb  27655  pntlemg  27656  pntlemh  27657  pntlemr  27660  pntlemk  27664  pntlemo  27665  pnt2  27671  pnt  27672  ostth2lem1  27676  ostth3  27696  slotsinbpsd  28463  slotslnbpsd  28464  istrkg3ld  28483  tgldimor  28524  trgcgrg  28537  tgcgr4  28553  axlowdimlem6  28976  axlowdimlem16  28986  axlowdimlem17  28987  axlowdim  28990  upgrfi  29122  umgrupgr  29134  umgrislfupgrlem  29153  umgrislfupgr  29154  lfgrnloop  29156  usgruspgr  29211  usgrislfuspgr  29218  lfuhgr1v0e  29285  usgrexmpldifpr  29289  usgrexmplef  29290  nbusgrvtxm1  29410  vdegp1bi  29569  upgrewlkle2  29638  lfgrwlkprop  29719  upgr2pthnlp  29764  usgr2pthlem  29795  pthdlem1  29798  wwlksm1edg  29910  wwlksnextwrd  29926  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextproplem3  29940  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a2  30021  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlk2  30031  clwlkclwwlkf  30036  clwwlkext2edg  30084  konigsbergiedgw  30276  konigsbergssiedgw  30278  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  konigsberg  30285  frgrreggt1  30421  ex-pss  30456  ex-res  30469  ex-fv  30471  ex-fl  30475  ex-mod  30477  ex-abs  30483  nrt2irr  30501  ipidsq  30738  minvecolem2  30903  minvecolem4  30908  normlem7  31144  norm-ii-i  31165  norm3lemt  31180  normpar2i  31184  bcsiALT  31207  pjhthlem1  31419  opsqrlem6  32173  cdj3lem1  32462  addltmulALT  32474  threehalves  32881  pfx1s2  32907  wrdt2ind  32922  oppgleOLD  32936  cyc3conja  33159  resvplusgOLD  33341  drngidlhash  33441  evl1deg3  33582  rtelextdg2lem  33731  fldext2chn  33733  2sqr3minply  33752  sqsscirc1  33868  nexple  33989  dya2iocucvr  34265  omssubadd  34281  oddpwdc  34335  eulerpartlemgc  34343  fibp1  34382  coinfliplem  34459  coinflipspace  34461  ballotlem2  34469  signstfveq0  34570  prodfzo03  34596  hgt750lemd  34641  logdivsqrle  34643  hgt750lem  34644  hgt750lem2  34645  hgt750leme  34651  lfuhgr2  35102  usgrcyclgt2v  35115  acycgr2v  35134  subfacp1lem1  35163  subfacp1lem5  35168  subfacval3  35173  problem2  35650  problem5  35653  circum  35658  nn0prpwlem  36304  dnibndlem10  36469  knoppcnlem2  36476  knoppcnlem4  36478  knoppcnlem10  36484  unbdqndv2lem1  36491  knoppndvlem1  36494  knoppndvlem10  36503  knoppndvlem11  36504  knoppndvlem12  36505  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem18  36511  knoppndvlem19  36512  knoppndvlem20  36513  knoppndvlem21  36514  cnndvlem1  36519  taupi  37305  iccioo01  37309  relowlpssretop  37346  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem7  37613  poimirlem9  37615  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  itg2addnclem  37657  isbnd2  37769  isbnd3  37770  heiborlem7  37803  12gcd5e1  41984  lcm2un  41995  lcmineqlem19  42028  lcmineqlem20  42029  lcmineqlem22  42031  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1lem1  42043  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  aks6d1c3  42104  2np3bcnp1  42125  2ap1caineq  42126  aks6d1c6lem4  42154  aks6d1c7lem1  42161  aks6d1c7lem2  42162  2xp3dxp2ge1d  42222  oexpreposd  42335  asin1half  42365  remul02  42411  sn-0ne2  42412  remul01  42413  flt4lem7  42645  rabren3dioph  42802  pellexlem2  42817  pellexlem5  42820  pell14qrgapw  42863  pellfundex  42873  rmspecsqrtnq  42893  jm2.24nn  42947  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  acongrep  42968  acongeq  42971  jm2.22  42983  jm2.23  42984  jm2.20nn  42985  jm3.1lem2  43006  expdiophlem1  43009  sqrtcval  43630  imo72b2lem0  44154  mnringaddgdOLD  44213  lhe4.4ex1a  44324  isosctrlem1ALT  44931  sineq0ALT  44934  lt3addmuld  45251  suplesup  45288  infleinflem2  45320  infleinf  45321  sumnnodd  45585  0ellimcdiv  45604  sinaover2ne0  45823  stoweidlem13  45968  stoweidlem14  45969  stoweidlem26  45981  stoweidlem49  46004  stoweidlem52  46007  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  stirlinglem11  46039  stirlinglem15  46043  stirlingr  46045  dirker2re  46047  dirkerval2  46049  dirkerre  46050  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem3  46055  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem24  46086  fourierdlem43  46105  fourierdlem44  46106  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem66  46127  fourierdlem68  46129  fourierdlem72  46133  fourierdlem76  46137  fourierdlem78  46139  fourierdlem79  46140  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem113  46174  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  etransclem23  46212  salexct2  46294  salexct3  46297  salgencntex  46298  salgensscntex  46299  sge0ad2en  46386  ovnsubaddlem1  46525  smfmullem4  46749  smf2id  46756  2leaddle2  47247  p1lep2  47249  ceil5half3  47279  fmtnoge3  47454  fmtnof1  47459  fmtnoprmfac2lem1  47490  fmtno4prmfac  47496  fmtno4prm  47499  2pwp1prm  47513  31prm  47521  sfprmdvdsmersenne  47527  lighneallem2  47530  lighneallem4a  47532  lighneallem4b  47533  requad01  47545  requad1  47546  requad2  47547  dfodd4  47583  nn0o1gt2ALTV  47618  nnoALTV  47619  nn0oALTV  47620  nn0e  47621  nneven  47622  perfectALTVlem1  47645  perfectALTVlem2  47646  341fppr2  47658  9fppr8  47661  fpprel2  47665  nfermltl2rev  47667  gbowgt5  47686  sbgoldbalt  47705  sgoldbeven3prm  47707  mogoldbb  47709  nnsum3primes4  47712  nnsum3primesgbe  47716  nnsum3primesle9  47718  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  usgrexmpl2trifr  47931  2ltceilhalf  47949  2tceilhalfelfzo1  47952  gpg5nbgrvtx13starlem2  47962  gpg3nbgrvtx0  47966  cznnring  48105  ply1mulgsumlem2  48232  zlmodzxznm  48342  zlmodzxzldeplem  48343  difmodm1lt  48371  nn0eo  48377  flnn0div2ge  48382  rege1logbzge0  48408  fldivexpfllog2  48414  logbpw2m1  48416  fllog2  48417  blenpw2m1  48428  nnpw2blen  48429  nnolog2flm1  48439  blennngt2o2  48441  dig2nn1st  48454  dig2nn0  48460  dig2bits  48463  dignn0flhalflem1  48464  dignn0flhalflem2  48465  dignn0flhalf  48467  nn0sumshdiglemA  48468  ackval42  48545  rrx2xpref1o  48567  itscnhlc0yqe  48608  itsclquadb  48625  2itscp  48630  itscnhlinecirc02p  48634  sepfsepc  48723