Theorem 2re 12255

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 12244	. 2 ⊢ 2 = (1 + 1)
2		1re 11144	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11160	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2832	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  1c1 11039   + caddc 11041  2c2 12236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244

This theorem is referenced by:  2cnALT  12257  3re  12261  3pos  12286  2lt3  12348  1lt3  12349  2lt4  12351  1lt4  12352  2lt5  12355  2lt6  12360  1lt6  12361  2lt7  12366  1lt7  12367  2lt8  12373  1lt8  12374  2lt9  12381  1lt9  12382  1le2  12385  2rene0  12387  halfre  12390  halfgt0  12392  halflt1  12394  rehalfcl  12404  halfpos2  12406  halfnneg2  12408  addltmul  12413  nominpos  12414  avglt1  12415  avglt2  12416  div4p1lem1div2  12432  nn0lele2xi  12493  nn0n0n1ge2b  12506  nn0ge2m1nn  12507  nn0le2is012  12593  halfnz  12607  3halfnz  12608  2lt10  12782  1lt10  12783  uzuzle23  12834  uzuzle24  12835  uz3m2nn  12844  2rp  12947  ge2halflem1  13059  xnn0n0n1ge2b  13083  fztpval  13540  fz0to4untppr  13584  fz0to5un2tp  13585  fzo0to42pr  13708  flhalf  13789  fldiv4p1lem1div2  13794  2txmodxeq0  13893  expubnd  14140  expmulnbnd  14197  nn0opthlem2  14231  faclbnd2  14253  faclbnd4lem1  14255  faclbnd5  14260  4bc2eq6  14291  hashgt23el  14386  hashfun  14399  hashge2el2dif  14442  hashge2el2difr  14443  hash3tpde  14455  wrdlenge2n0  14514  f1oun2prg  14879  01sqrexlem7  15210  sqrt4  15234  sqrt2gt1lt2  15236  abstri  15293  sqreulem  15322  amgm2  15332  caucvgrlem  15635  climcndslem1  15814  climcndslem2  15815  climcnds  15816  efcllem  16042  ege2le3  16055  ef01bndlem  16151  cos01bnd  16153  cos2bnd  16155  cos01gt0  16158  sin02gt0  16159  sincos2sgn  16161  sin4lt0  16162  eirrlem  16171  egt2lt3  16173  epos  16174  ene1  16177  sqrt2re  16217  mod2eq1n2dvds  16316  oddge22np1  16318  evennn2n  16320  nn0o1gt2  16350  nno  16351  nn0o  16352  nnoddm1d2  16355  bitsp1o  16402  bitsfzolem  16403  bitsfzo  16404  bitsfi  16406  6gcd4e2  16507  2mulprm  16662  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  19718  zringndrg  21448  chfacfscmul0  22823  chfacfpmmul0  22827  psmetge0  24277  xmetge0  24309  bl2in  24365  metnrmlem3  24827  iihalf1  24898  iihalf2  24900  pcoass  24991  tcphcphlem1  25202  csbren  25366  trirn  25367  minveclem2  25393  minveclem4  25399  pjthlem1  25404  ovolunlem1a  25463  dyadss  25561  opnmbllem  25568  vitalilem2  25576  vitalilem4  25578  mbfi1fseqlem5  25686  lhop1lem  25980  aaliou3lem2  26309  aaliou3lem8  26311  pilem2  26417  pilem3  26418  pipos  26423  sinhalfpilem  26427  sincosq1lem  26461  sincosq4sgn  26465  tangtx  26469  sinq12gt0  26471  sincos4thpi  26477  tan4thpi  26478  tan4thpiOLD  26479  sincos6thpi  26480  sineq0  26488  cos02pilt1  26490  cosq34lt1  26491  cosordlem  26494  cos0pilt1  26496  tanord1  26501  efif1olem1  26506  efif1olem2  26507  efif1olem4  26509  efif1o  26510  efifo  26511  2irrexpq  26695  cxpcn3lem  26711  root1id  26718  root1eq1  26719  root1cj  26720  cxpeq  26721  2logb9irr  26759  2logb3irr  26761  ang180lem1  26773  ang180lem2  26774  chordthmlem2  26797  1cubrlem  26805  atancj  26874  atantan  26887  atanbndlem  26889  atans2  26895  leibpi  26906  log2tlbnd  26909  log2ublem2  26911  log2ub  26913  divsqrtsumlem  26943  harmonicbnd3  26971  zetacvg  26978  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem6  26997  lgamucov  27001  basellem1  27044  basellem2  27045  basellem3  27046  basellem5  27048  chtdif  27121  ppidif  27126  ppinncl  27137  chtrpcl  27138  ppieq0  27139  ppiltx  27140  ppiublem1  27165  ppiub  27167  chpeq0  27171  chteq0  27172  chtublem  27174  chtub  27175  chpval2  27181  chpub  27183  mersenne  27190  perfectlem1  27192  perfectlem2  27193  dchrptlem1  27227  dchrptlem2  27228  bcmono  27240  bclbnd  27243  bpos1lem  27245  bposlem1  27247  bposlem2  27248  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem7  27253  bposlem8  27254  bposlem9  27255  lgslem1  27260  lgsdirprm  27294  gausslemma2dlem0c  27321  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem3  27331  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisen  27342  lgsquadlem1  27343  lgsquadlem2  27344  m1lgs  27351  2lgslem1a1  27352  2lgslem1a2  27353  2lgslem1c  27356  2lgslem4  27369  2sqlem11  27392  2sq2  27396  2sqreultlem  27410  2sqreunnltlem  27413  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chtppilim  27438  chto1ub  27439  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ub  27443  chpo1ubb  27444  rplogsumlem1  27447  rplogsumlem2  27448  dchrisumlem2  27453  dchrisumlem3  27454  dchrvmasumiflem1  27464  dchrisum0fno1  27474  dchrisum0re  27476  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2  27481  rplogsum  27490  mulog2sumlem1  27497  mulog2sumlem2  27498  log2sumbnd  27507  selberglem2  27509  selbergb  27512  selberg2b  27515  chpdifbndlem1  27516  logdivbnd  27519  selberg3lem1  27520  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrmax  27527  pntrsumbnd2  27530  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntpbnd  27551  pntibndlem2  27554  pntibndlem3  27555  pntibnd  27556  pntlemb  27560  pntlemg  27561  pntlemh  27562  pntlemr  27565  pntlemk  27569  pntlemo  27570  pnt2  27576  pnt  27577  ostth2lem1  27581  ostth3  27601  slotsinbpsd  28509  slotslnbpsd  28510  istrkg3ld  28529  tgldimor  28570  trgcgrg  28583  tgcgr4  28599  axlowdimlem6  29016  axlowdimlem16  29026  axlowdimlem17  29027  axlowdim  29030  upgrfi  29160  umgrupgr  29172  umgrislfupgrlem  29191  umgrislfupgr  29192  lfgrnloop  29194  usgruspgr  29249  usgrislfuspgr  29256  lfuhgr1v0e  29323  usgrexmpldifpr  29327  usgrexmplef  29328  nbusgrvtxm1  29448  vdegp1bi  29606  upgrewlkle2  29675  lfgrwlkprop  29754  upgr2pthnlp  29800  usgr2pthlem  29831  pthdlem1  29834  wwlksm1edg  29949  wwlksnextwrd  29965  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextproplem3  29979  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a2  30063  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlk2  30073  clwlkclwwlkf  30078  clwwlkext2edg  30126  konigsbergiedgw  30318  konigsbergssiedgw  30320  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  konigsberg  30327  frgrreggt1  30463  ex-pss  30498  ex-res  30511  ex-fv  30513  ex-fl  30517  ex-mod  30519  ex-abs  30525  nrt2irr  30543  ipidsq  30781  minvecolem2  30946  minvecolem4  30951  normlem7  31187  norm-ii-i  31208  norm3lemt  31223  normpar2i  31227  bcsiALT  31250  pjhthlem1  31462  opsqrlem6  32216  cdj3lem1  32505  addltmulALT  32517  nexple  32917  2exple2exp  32918  threehalves  32974  pfx1s2  32999  wrdt2ind  33013  cyc3conja  33218  drngidlhash  33494  evl1deg3  33638  rtelextdg2lem  33870  fldext2chn  33872  constraddcl  33906  iconstr  33910  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpinconstrlem1  33933  cos9thpinconstrlem2  33934  sqsscirc1  34052  dya2iocucvr  34428  omssubadd  34444  oddpwdc  34498  eulerpartlemgc  34506  fibp1  34545  coinfliplem  34623  coinflipspace  34625  ballotlem2  34633  signstfveq0  34721  prodfzo03  34747  hgt750lemd  34792  logdivsqrle  34794  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  lfuhgr2  35301  usgrcyclgt2v  35313  acycgr2v  35332  subfacp1lem1  35361  subfacp1lem5  35366  subfacval3  35371  problem2  35848  problem5  35851  circum  35856  nn0prpwlem  36504  dnibndlem10  36747  knoppcnlem2  36754  knoppcnlem4  36756  knoppcnlem10  36762  unbdqndv2lem1  36769  knoppndvlem1  36772  knoppndvlem10  36781  knoppndvlem11  36782  knoppndvlem12  36783  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem18  36789  knoppndvlem19  36790  knoppndvlem20  36791  knoppndvlem21  36792  cnndvlem1  36797  taupi  37637  iccioo01  37643  relowlpssretop  37680  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem7  37948  poimirlem9  37950  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  itg2addnclem  37992  isbnd2  38104  isbnd3  38105  heiborlem7  38138  12gcd5e1  42442  lcm2un  42453  lcmineqlem19  42486  lcmineqlem20  42487  lcmineqlem22  42489  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1lem1  42501  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  aks6d1c3  42562  2np3bcnp1  42583  2ap1caineq  42584  aks6d1c6lem4  42612  aks6d1c7lem1  42619  aks6d1c7lem2  42620  oexpreposd  42754  asin1half  42789  remul02  42837  sn-0ne2  42838  remul01  42839  flt4lem7  43092  rabren3dioph  43243  pellexlem2  43258  pellexlem5  43261  pell14qrgapw  43304  pellfundex  43314  rmspecsqrtnq  43334  jm2.24nn  43387  jm2.17a  43388  jm2.17b  43389  jm2.17c  43390  acongrep  43408  acongeq  43411  jm2.22  43423  jm2.23  43424  jm2.20nn  43425  jm3.1lem2  43446  expdiophlem1  43449  sqrtcval  44068  imo72b2lem0  44592  lhe4.4ex1a  44756  isosctrlem1ALT  45360  sineq0ALT  45363  lt3addmuld  45734  suplesup  45769  infleinflem2  45800  infleinf  45801  sumnnodd  46060  0ellimcdiv  46077  sinaover2ne0  46296  stoweidlem13  46441  stoweidlem14  46442  stoweidlem26  46454  stoweidlem49  46477  stoweidlem52  46480  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  stirlinglem15  46516  stirlingr  46518  dirker2re  46520  dirkerval2  46522  dirkerre  46523  dirkerper  46524  dirkertrigeqlem1  46526  dirkertrigeqlem3  46528  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem24  46559  fourierdlem43  46578  fourierdlem44  46579  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem66  46600  fourierdlem68  46602  fourierdlem72  46606  fourierdlem76  46610  fourierdlem78  46612  fourierdlem79  46613  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem113  46647  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem23  46685  salexct2  46767  salexct3  46770  salgencntex  46771  salgensscntex  46772  sge0ad2en  46859  ovnsubaddlem1  46998  smfmullem4  47222  smf2id  47229  nthrucw  47316  goldrarr  47329  goldrapos  47331  2leaddle2  47746  p1lep2  47748  2ltceilhalf  47780  ceilhalfgt1  47781  2tceilhalfelfzo1  47784  rehalfge1  47787  ceilhalfnn  47788  ceil5half3  47794  difmodm1lt  47813  2timesltsq  47826  2timesltsqm1  47827  fmtnoge3  47993  fmtnof1  47998  fmtnoprmfac2lem1  48029  fmtno4prmfac  48035  fmtno4prm  48038  2pwp1prm  48052  31prm  48060  sfprmdvdsmersenne  48066  lighneallem2  48069  lighneallem4a  48071  lighneallem4b  48072  nprmdvdsfacm1lem2  48084  nprmdvdsfacm1lem4  48086  ppivalnnnprmge6  48089  requad01  48097  requad1  48098  requad2  48099  dfodd4  48135  nn0o1gt2ALTV  48170  nnoALTV  48171  nn0oALTV  48172  nn0e  48173  nneven  48174  perfectALTVlem1  48197  perfectALTVlem2  48198  341fppr2  48210  9fppr8  48213  fpprel2  48217  nfermltl2rev  48219  gbowgt5  48238  sbgoldbalt  48257  sgoldbeven3prm  48259  mogoldbb  48261  nnsum3primes4  48264  nnsum3primesgbe  48268  nnsum3primesle9  48270  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  cycl3grtri  48423  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  gpgprismgrusgra  48534  gpg5nbgrvtx13starlem2  48548  gpg3nbgrvtx0  48552  gpg3kgrtriexlem1  48559  cznnring  48738  ply1mulgsumlem2  48863  zlmodzxznm  48973  zlmodzxzldeplem  48974  nn0eo  49004  flnn0div2ge  49009  rege1logbzge0  49035  fldivexpfllog2  49041  logbpw2m1  49043  fllog2  49044  blenpw2m1  49055  nnpw2blen  49056  nnolog2flm1  49066  blennngt2o2  49068  dig2nn1st  49081  dig2nn0  49087  dig2bits  49090  dignn0flhalflem1  49091  dignn0flhalflem2  49092  dignn0flhalf  49094  nn0sumshdiglemA  49095  ackval42  49172  rrx2xpref1o  49194  itscnhlc0yqe  49235  itsclquadb  49252  2itscp  49257  itscnhlinecirc02p  49261  sepfsepc  49403