Theorem 2re 12236

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043  1c1 11045   + caddc 11047  2c2 12217

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 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225

This theorem is referenced by:  2cnALT  12238  3re  12242  3pos  12267  2lt3  12329  1lt3  12330  2lt4  12332  1lt4  12333  2lt5  12336  2lt6  12341  1lt6  12342  2lt7  12347  1lt7  12348  2lt8  12354  1lt8  12355  2lt9  12362  1lt9  12363  1le2  12366  2rene0  12368  halfre  12371  halfgt0  12373  halflt1  12375  rehalfcl  12385  halfpos2  12387  halfnneg2  12389  addltmul  12394  nominpos  12395  avglt1  12396  avglt2  12397  div4p1lem1div2  12413  nn0lele2xi  12474  nn0n0n1ge2b  12487  nn0ge2m1nn  12488  nn0le2is012  12574  halfnz  12588  3halfnz  12589  2lt10  12763  1lt10  12764  uzuzle23  12819  uzuzle24  12820  uz3m2nn  12829  2rp  12932  ge2halflem1  13044  xnn0n0n1ge2b  13068  fztpval  13523  fz0to4untppr  13567  fz0to5un2tp  13568  fzo0to42pr  13690  flhalf  13768  fldiv4p1lem1div2  13773  2txmodxeq0  13872  expubnd  14119  expmulnbnd  14176  nn0opthlem2  14210  faclbnd2  14232  faclbnd4lem1  14234  faclbnd5  14239  4bc2eq6  14270  hashgt23el  14365  hashfun  14378  hashge2el2dif  14421  hashge2el2difr  14422  hash3tpde  14434  wrdlenge2n0  14493  f1oun2prg  14859  01sqrexlem7  15190  sqrt4  15214  sqrt2gt1lt2  15216  abstri  15273  sqreulem  15302  amgm2  15312  caucvgrlem  15615  climcndslem1  15791  climcndslem2  15792  climcnds  15793  efcllem  16019  ege2le3  16032  ef01bndlem  16128  cos01bnd  16130  cos2bnd  16132  cos01gt0  16135  sin02gt0  16136  sincos2sgn  16138  sin4lt0  16139  eirrlem  16148  egt2lt3  16150  epos  16151  ene1  16154  sqrt2re  16194  mod2eq1n2dvds  16293  oddge22np1  16295  evennn2n  16297  nn0o1gt2  16327  nno  16328  nn0o  16329  nnoddm1d2  16332  bitsp1o  16379  bitsfzolem  16380  bitsfzo  16381  bitsfi  16383  6gcd4e2  16484  2mulprm  16639  ge2nprmge4  16647  isprm7  16654  3lcm2e6  16678  prmreclem2  16864  prmreclem6  16868  4sqlem11  16902  4sqlem12  16903  prmgaplem7  17004  2expltfac  17039  plusgndxnmulrndx  17236  starvndxnplusgndx  17244  scandxnplusgndx  17256  vscandxnplusgndx  17261  ipndxnplusgndx  17272  tsetndxnplusgndx  17296  plendxnplusgndx  17310  dsndxnplusgndx  17329  slotsdifunifndx  17340  efgredleme  19657  zringndrg  21410  chfacfscmul0  22778  chfacfpmmul0  22782  psmetge0  24233  xmetge0  24265  bl2in  24321  metnrmlem3  24783  iihalf1  24858  iihalf2  24861  pcoass  24957  tcphcphlem1  25168  csbren  25332  trirn  25333  minveclem2  25359  minveclem4  25365  pjthlem1  25370  ovolunlem1a  25430  dyadss  25528  opnmbllem  25535  vitalilem2  25543  vitalilem4  25545  mbfi1fseqlem5  25653  lhop1lem  25951  aaliou3lem2  26284  aaliou3lem8  26286  pilem2  26395  pilem3  26396  pipos  26401  sinhalfpilem  26405  sincosq1lem  26439  sincosq4sgn  26443  tangtx  26447  sinq12gt0  26449  sincos4thpi  26455  tan4thpi  26456  tan4thpiOLD  26457  sincos6thpi  26458  sineq0  26466  cos02pilt1  26468  cosq34lt1  26469  cosordlem  26472  cos0pilt1  26474  tanord1  26479  efif1olem1  26484  efif1olem2  26485  efif1olem4  26487  efif1o  26488  efifo  26489  2irrexpq  26673  cxpcn3lem  26690  root1id  26697  root1eq1  26698  root1cj  26699  cxpeq  26700  2logb9irr  26738  2logb3irr  26740  ang180lem1  26752  ang180lem2  26753  chordthmlem2  26776  1cubrlem  26784  atancj  26853  atantan  26866  atanbndlem  26868  atans2  26874  leibpi  26885  log2tlbnd  26888  log2ublem2  26890  log2ub  26892  divsqrtsumlem  26923  harmonicbnd3  26951  zetacvg  26958  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamgulmlem4  26975  lgamgulmlem6  26977  lgamucov  26981  basellem1  27024  basellem2  27025  basellem3  27026  basellem5  27028  chtdif  27101  ppidif  27106  ppinncl  27117  chtrpcl  27118  ppieq0  27119  ppiltx  27120  ppiublem1  27146  ppiub  27148  chpeq0  27152  chteq0  27153  chtublem  27155  chtub  27156  chpval2  27162  chpub  27164  mersenne  27171  perfectlem1  27173  perfectlem2  27174  dchrptlem1  27208  dchrptlem2  27209  bcmono  27221  bclbnd  27224  bpos1lem  27226  bposlem1  27228  bposlem2  27229  bposlem3  27230  bposlem4  27231  bposlem5  27232  bposlem6  27233  bposlem7  27234  bposlem8  27235  bposlem9  27236  lgslem1  27241  lgsdirprm  27275  gausslemma2dlem0c  27302  gausslemma2dlem1a  27309  gausslemma2dlem2  27311  gausslemma2dlem3  27312  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgseisen  27323  lgsquadlem1  27324  lgsquadlem2  27325  m1lgs  27332  2lgslem1a1  27333  2lgslem1a2  27334  2lgslem1c  27337  2lgslem4  27350  2sqlem11  27373  2sq2  27377  2sqreultlem  27391  2sqreunnltlem  27394  chebbnd1lem1  27413  chebbnd1lem2  27414  chebbnd1lem3  27415  chebbnd1  27416  chtppilimlem1  27417  chtppilimlem2  27418  chtppilim  27419  chto1ub  27420  chebbnd2  27421  chto1lb  27422  chpchtlim  27423  chpo1ub  27424  chpo1ubb  27425  rplogsumlem1  27428  rplogsumlem2  27429  dchrisumlem2  27434  dchrisumlem3  27435  dchrvmasumiflem1  27445  dchrisum0fno1  27455  dchrisum0re  27457  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2  27462  rplogsum  27471  mulog2sumlem1  27478  mulog2sumlem2  27479  log2sumbnd  27488  selberglem2  27490  selbergb  27493  selberg2b  27496  chpdifbndlem1  27497  logdivbnd  27500  selberg3lem1  27501  selberg3  27503  selberg4lem1  27504  selberg4  27505  pntrmax  27508  pntrsumbnd2  27511  selberg3r  27513  selberg4r  27514  selberg34r  27515  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntpbnd  27532  pntibndlem2  27535  pntibndlem3  27536  pntibnd  27537  pntlemb  27541  pntlemg  27542  pntlemh  27543  pntlemr  27546  pntlemk  27550  pntlemo  27551  pnt2  27557  pnt  27558  ostth2lem1  27562  ostth3  27582  slotsinbpsd  28421  slotslnbpsd  28422  istrkg3ld  28441  tgldimor  28482  trgcgrg  28495  tgcgr4  28511  axlowdimlem6  28927  axlowdimlem16  28937  axlowdimlem17  28938  axlowdim  28941  upgrfi  29071  umgrupgr  29083  umgrislfupgrlem  29102  umgrislfupgr  29103  lfgrnloop  29105  usgruspgr  29160  usgrislfuspgr  29167  lfuhgr1v0e  29234  usgrexmpldifpr  29238  usgrexmplef  29239  nbusgrvtxm1  29359  vdegp1bi  29518  upgrewlkle2  29587  lfgrwlkprop  29666  upgr2pthnlp  29712  usgr2pthlem  29743  pthdlem1  29746  wwlksm1edg  29861  wwlksnextwrd  29877  wwlksnextfun  29878  wwlksnextinj  29879  wwlksnextproplem3  29891  clwlkclwwlklem2a1  29971  clwlkclwwlklem2a2  29972  clwlkclwwlklem2fv1  29974  clwlkclwwlklem2fv2  29975  clwlkclwwlklem2a4  29976  clwlkclwwlklem2a  29977  clwlkclwwlklem2  29979  clwlkclwwlk2  29982  clwlkclwwlkf  29987  clwwlkext2edg  30035  konigsbergiedgw  30227  konigsbergssiedgw  30229  konigsberglem1  30231  konigsberglem2  30232  konigsberglem3  30233  konigsberg  30236  frgrreggt1  30372  ex-pss  30407  ex-res  30420  ex-fv  30422  ex-fl  30426  ex-mod  30428  ex-abs  30434  nrt2irr  30452  ipidsq  30689  minvecolem2  30854  minvecolem4  30859  normlem7  31095  norm-ii-i  31116  norm3lemt  31131  normpar2i  31135  bcsiALT  31158  pjhthlem1  31370  opsqrlem6  32124  cdj3lem1  32413  addltmulALT  32425  nexple  32819  2exple2exp  32820  threehalves  32885  pfx1s2  32910  wrdt2ind  32925  cyc3conja  33129  drngidlhash  33398  evl1deg3  33540  rtelextdg2lem  33709  fldext2chn  33711  constraddcl  33745  iconstr  33749  2sqr3minply  33763  2sqr3nconstr  33764  cos9thpinconstrlem1  33772  cos9thpinconstrlem2  33773  sqsscirc1  33891  dya2iocucvr  34268  omssubadd  34284  oddpwdc  34338  eulerpartlemgc  34346  fibp1  34385  coinfliplem  34463  coinflipspace  34465  ballotlem2  34473  signstfveq0  34561  prodfzo03  34587  hgt750lemd  34632  logdivsqrle  34634  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  lfuhgr2  35099  usgrcyclgt2v  35111  acycgr2v  35130  subfacp1lem1  35159  subfacp1lem5  35164  subfacval3  35169  problem2  35646  problem5  35649  circum  35654  nn0prpwlem  36303  dnibndlem10  36468  knoppcnlem2  36475  knoppcnlem4  36477  knoppcnlem10  36483  unbdqndv2lem1  36490  knoppndvlem1  36493  knoppndvlem10  36502  knoppndvlem11  36503  knoppndvlem12  36504  knoppndvlem14  36506  knoppndvlem15  36507  knoppndvlem17  36509  knoppndvlem18  36510  knoppndvlem19  36511  knoppndvlem20  36512  knoppndvlem21  36513  cnndvlem1  36518  taupi  37304  iccioo01  37308  relowlpssretop  37345  sin2h  37597  cos2h  37598  tan2h  37599  poimirlem7  37614  poimirlem9  37616  opnmbllem0  37643  mblfinlem1  37644  mblfinlem2  37645  itg2addnclem  37658  isbnd2  37770  isbnd3  37771  heiborlem7  37804  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  oexpreposd  42303  asin1half  42338  remul02  42386  sn-0ne2  42387  remul01  42388  flt4lem7  42640  rabren3dioph  42796  pellexlem2  42811  pellexlem5  42814  pell14qrgapw  42857  pellfundex  42867  rmspecsqrtnq  42887  jm2.24nn  42941  jm2.17a  42942  jm2.17b  42943  jm2.17c  42944  acongrep  42962  acongeq  42965  jm2.22  42977  jm2.23  42978  jm2.20nn  42979  jm3.1lem2  43000  expdiophlem1  43003  sqrtcval  43623  imo72b2lem0  44147  lhe4.4ex1a  44311  isosctrlem1ALT  44916  sineq0ALT  44919  lt3addmuld  45292  suplesup  45328  infleinflem2  45360  infleinf  45361  sumnnodd  45621  0ellimcdiv  45640  sinaover2ne0  45859  stoweidlem13  46004  stoweidlem14  46005  stoweidlem26  46017  stoweidlem49  46040  stoweidlem52  46043  wallispilem4  46059  wallispilem5  46060  wallispi  46061  wallispi2lem1  46062  wallispi2lem2  46063  wallispi2  46064  stirlinglem1  46065  stirlinglem3  46067  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem10  46074  stirlinglem11  46075  stirlinglem15  46079  stirlingr  46081  dirker2re  46083  dirkerval2  46085  dirkerre  46086  dirkerper  46087  dirkertrigeqlem1  46089  dirkertrigeqlem3  46091  dirkercncflem1  46094  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem24  46122  fourierdlem43  46141  fourierdlem44  46142  fourierdlem57  46154  fourierdlem58  46155  fourierdlem62  46159  fourierdlem66  46163  fourierdlem68  46165  fourierdlem72  46169  fourierdlem76  46173  fourierdlem78  46175  fourierdlem79  46176  fourierdlem94  46191  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem113  46210  sqwvfoura  46219  sqwvfourb  46220  fourierswlem  46221  fouriersw  46222  etransclem23  46248  salexct2  46330  salexct3  46333  salgencntex  46334  salgensscntex  46335  sge0ad2en  46422  ovnsubaddlem1  46561  smfmullem4  46785  smf2id  46792  2leaddle2  47292  p1lep2  47294  2ltceilhalf  47322  ceilhalfgt1  47323  2tceilhalfelfzo1  47326  rehalfge1  47329  ceilhalfnn  47330  ceil5half3  47334  difmodm1lt  47353  fmtnoge3  47524  fmtnof1  47529  fmtnoprmfac2lem1  47560  fmtno4prmfac  47566  fmtno4prm  47569  2pwp1prm  47583  31prm  47591  sfprmdvdsmersenne  47597  lighneallem2  47600  lighneallem4a  47602  lighneallem4b  47603  requad01  47615  requad1  47616  requad2  47617  dfodd4  47653  nn0o1gt2ALTV  47688  nnoALTV  47689  nn0oALTV  47690  nn0e  47691  nneven  47692  perfectALTVlem1  47715  perfectALTVlem2  47716  341fppr2  47728  9fppr8  47731  fpprel2  47735  nfermltl2rev  47737  gbowgt5  47756  sbgoldbalt  47775  sgoldbeven3prm  47777  mogoldbb  47779  nnsum3primes4  47782  nnsum3primesgbe  47786  nnsum3primesle9  47788  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  cycl3grtri  47939  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb2  48017  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpgprismgrusgra  48042  gpg5nbgrvtx13starlem2  48056  gpg3nbgrvtx0  48060  gpg3kgrtriexlem1  48067  cznnring  48243  ply1mulgsumlem2  48369  zlmodzxznm  48479  zlmodzxzldeplem  48480  nn0eo  48510  flnn0div2ge  48515  rege1logbzge0  48541  fldivexpfllog2  48547  logbpw2m1  48549  fllog2  48550  blenpw2m1  48561  nnpw2blen  48562  nnolog2flm1  48572  blennngt2o2  48574  dig2nn1st  48587  dig2nn0  48593  dig2bits  48596  dignn0flhalflem1  48597  dignn0flhalflem2  48598  dignn0flhalf  48600  nn0sumshdiglemA  48601  ackval42  48678  rrx2xpref1o  48700  itscnhlc0yqe  48741  itsclquadb  48758  2itscp  48763  itscnhlinecirc02p  48767  sepfsepc  48909