Theorem 2re 12312

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 12301	. 2 ⊢ 2 = (1 + 1)
2		1re 11233	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11248	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2830	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126  1c1 11128   + caddc 11130  2c2 12293

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301

This theorem is referenced by:  2cnALT  12314  3re  12318  3pos  12343  2lt3  12410  1lt3  12411  2lt4  12413  1lt4  12414  2lt5  12417  2lt6  12422  1lt6  12423  2lt7  12428  1lt7  12429  2lt8  12435  1lt8  12436  2lt9  12443  1lt9  12444  1le2  12447  2rene0  12449  halfre  12452  halfgt0  12454  halflt1  12456  rehalfcl  12466  halfpos2  12468  halfnneg2  12470  addltmul  12475  nominpos  12476  avglt1  12477  avglt2  12478  div4p1lem1div2  12494  nn0lele2xi  12555  nn0n0n1ge2b  12568  nn0ge2m1nn  12569  nn0le2is012  12655  halfnz  12669  3halfnz  12670  2lt10  12844  1lt10  12845  eluz4eluz2  12897  uzuzle23  12903  uz3m2nn  12905  2rp  13011  ge2halflem1  13122  xnn0n0n1ge2b  13146  fztpval  13601  fz0to4untppr  13645  fz0to5un2tp  13646  fzo0to42pr  13767  flhalf  13845  fldiv4p1lem1div2  13850  2txmodxeq0  13947  expubnd  14194  expmulnbnd  14251  nn0opthlem2  14285  faclbnd2  14307  faclbnd4lem1  14309  faclbnd5  14314  4bc2eq6  14345  hashgt23el  14440  hashfun  14453  hashge2el2dif  14496  hashge2el2difr  14497  hash3tpde  14509  wrdlenge2n0  14568  f1oun2prg  14934  01sqrexlem7  15265  sqrt4  15289  sqrt2gt1lt2  15291  abstri  15347  sqreulem  15376  amgm2  15386  caucvgrlem  15687  climcndslem1  15863  climcndslem2  15864  climcnds  15865  efcllem  16091  ege2le3  16104  ef01bndlem  16200  cos01bnd  16202  cos2bnd  16204  cos01gt0  16207  sin02gt0  16208  sincos2sgn  16210  sin4lt0  16211  eirrlem  16220  egt2lt3  16222  epos  16223  ene1  16226  sqrt2re  16266  mod2eq1n2dvds  16364  oddge22np1  16366  evennn2n  16368  nn0o1gt2  16398  nno  16399  nn0o  16400  nnoddm1d2  16403  bitsp1o  16450  bitsfzolem  16451  bitsfzo  16452  bitsfi  16454  6gcd4e2  16555  2mulprm  16710  ge2nprmge4  16718  isprm7  16725  3lcm2e6  16749  prmreclem2  16935  prmreclem6  16939  4sqlem11  16973  4sqlem12  16974  prmgaplem7  17075  2expltfac  17110  plusgndxnmulrndx  17309  starvndxnplusgndx  17317  scandxnplusgndx  17329  vscandxnplusgndx  17334  ipndxnplusgndx  17345  tsetndxnplusgndx  17369  plendxnplusgndx  17383  dsndxnplusgndx  17402  slotsdifunifndx  17413  efgredleme  19722  zringndrg  21427  chfacfscmul0  22794  chfacfpmmul0  22798  psmetge0  24249  xmetge0  24281  bl2in  24337  metnrmlem3  24799  iihalf1  24874  iihalf2  24877  pcoass  24973  tcphcphlem1  25185  csbren  25349  trirn  25350  minveclem2  25376  minveclem4  25382  pjthlem1  25387  ovolunlem1a  25447  dyadss  25545  opnmbllem  25552  vitalilem2  25560  vitalilem4  25562  mbfi1fseqlem5  25670  lhop1lem  25968  aaliou3lem2  26301  aaliou3lem8  26303  pilem2  26412  pilem3  26413  pipos  26418  sinhalfpilem  26422  sincosq1lem  26456  sincosq4sgn  26460  tangtx  26464  sinq12gt0  26466  sincos4thpi  26472  tan4thpi  26473  tan4thpiOLD  26474  sincos6thpi  26475  sineq0  26483  cos02pilt1  26485  cosq34lt1  26486  cosordlem  26489  cos0pilt1  26491  tanord1  26496  efif1olem1  26501  efif1olem2  26502  efif1olem4  26504  efif1o  26505  efifo  26506  2irrexpq  26690  cxpcn3lem  26707  root1id  26714  root1eq1  26715  root1cj  26716  cxpeq  26717  2logb9irr  26755  2logb3irr  26757  ang180lem1  26769  ang180lem2  26770  chordthmlem2  26793  1cubrlem  26801  atancj  26870  atantan  26883  atanbndlem  26885  atans2  26891  leibpi  26902  log2tlbnd  26905  log2ublem2  26907  log2ub  26909  divsqrtsumlem  26940  harmonicbnd3  26968  zetacvg  26975  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem6  26994  lgamucov  26998  basellem1  27041  basellem2  27042  basellem3  27043  basellem5  27045  chtdif  27118  ppidif  27123  ppinncl  27134  chtrpcl  27135  ppieq0  27136  ppiltx  27137  ppiublem1  27163  ppiub  27165  chpeq0  27169  chteq0  27170  chtublem  27172  chtub  27173  chpval2  27179  chpub  27181  mersenne  27188  perfectlem1  27190  perfectlem2  27191  dchrptlem1  27225  dchrptlem2  27226  bcmono  27238  bclbnd  27241  bpos1lem  27243  bposlem1  27245  bposlem2  27246  bposlem3  27247  bposlem4  27248  bposlem5  27249  bposlem6  27250  bposlem7  27251  bposlem8  27252  bposlem9  27253  lgslem1  27258  lgsdirprm  27292  gausslemma2dlem0c  27319  gausslemma2dlem1a  27326  gausslemma2dlem2  27328  gausslemma2dlem3  27329  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  m1lgs  27349  2lgslem1a1  27350  2lgslem1a2  27351  2lgslem1c  27354  2lgslem4  27367  2sqlem11  27390  2sq2  27394  2sqreultlem  27408  2sqreunnltlem  27411  chebbnd1lem1  27430  chebbnd1lem2  27431  chebbnd1lem3  27432  chebbnd1  27433  chtppilimlem1  27434  chtppilimlem2  27435  chtppilim  27436  chto1ub  27437  chebbnd2  27438  chto1lb  27439  chpchtlim  27440  chpo1ub  27441  chpo1ubb  27442  rplogsumlem1  27445  rplogsumlem2  27446  dchrisumlem2  27451  dchrisumlem3  27452  dchrvmasumiflem1  27462  dchrisum0fno1  27472  dchrisum0re  27474  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2  27479  rplogsum  27488  mulog2sumlem1  27495  mulog2sumlem2  27496  log2sumbnd  27505  selberglem2  27507  selbergb  27510  selberg2b  27513  chpdifbndlem1  27514  logdivbnd  27517  selberg3lem1  27518  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrmax  27525  pntrsumbnd2  27528  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntpbnd  27549  pntibndlem2  27552  pntibndlem3  27553  pntibnd  27554  pntlemb  27558  pntlemg  27559  pntlemh  27560  pntlemr  27563  pntlemk  27567  pntlemo  27568  pnt2  27574  pnt  27575  ostth2lem1  27579  ostth3  27599  slotsinbpsd  28366  slotslnbpsd  28367  istrkg3ld  28386  tgldimor  28427  trgcgrg  28440  tgcgr4  28456  axlowdimlem6  28872  axlowdimlem16  28882  axlowdimlem17  28883  axlowdim  28886  upgrfi  29016  umgrupgr  29028  umgrislfupgrlem  29047  umgrislfupgr  29048  lfgrnloop  29050  usgruspgr  29105  usgrislfuspgr  29112  lfuhgr1v0e  29179  usgrexmpldifpr  29183  usgrexmplef  29184  nbusgrvtxm1  29304  vdegp1bi  29463  upgrewlkle2  29532  lfgrwlkprop  29613  upgr2pthnlp  29660  usgr2pthlem  29691  pthdlem1  29694  wwlksm1edg  29809  wwlksnextwrd  29825  wwlksnextfun  29826  wwlksnextinj  29827  wwlksnextproplem3  29839  clwlkclwwlklem2a1  29919  clwlkclwwlklem2a2  29920  clwlkclwwlklem2fv1  29922  clwlkclwwlklem2fv2  29923  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  clwlkclwwlk2  29930  clwlkclwwlkf  29935  clwwlkext2edg  29983  konigsbergiedgw  30175  konigsbergssiedgw  30177  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  konigsberg  30184  frgrreggt1  30320  ex-pss  30355  ex-res  30368  ex-fv  30370  ex-fl  30374  ex-mod  30376  ex-abs  30382  nrt2irr  30400  ipidsq  30637  minvecolem2  30802  minvecolem4  30807  normlem7  31043  norm-ii-i  31064  norm3lemt  31079  normpar2i  31083  bcsiALT  31106  pjhthlem1  31318  opsqrlem6  32072  cdj3lem1  32361  addltmulALT  32373  nexple  32769  2exple2exp  32770  threehalves  32835  pfx1s2  32860  wrdt2ind  32875  cyc3conja  33114  drngidlhash  33395  evl1deg3  33537  rtelextdg2lem  33706  fldext2chn  33708  constraddcl  33742  iconstr  33746  2sqr3minply  33760  2sqr3nconstr  33761  cos9thpinconstrlem1  33769  sqsscirc1  33885  dya2iocucvr  34262  omssubadd  34278  oddpwdc  34332  eulerpartlemgc  34340  fibp1  34379  coinfliplem  34457  coinflipspace  34459  ballotlem2  34467  signstfveq0  34555  prodfzo03  34581  hgt750lemd  34626  logdivsqrle  34628  hgt750lem  34629  hgt750lem2  34630  hgt750leme  34636  lfuhgr2  35087  usgrcyclgt2v  35099  acycgr2v  35118  subfacp1lem1  35147  subfacp1lem5  35152  subfacval3  35157  problem2  35634  problem5  35637  circum  35642  nn0prpwlem  36286  dnibndlem10  36451  knoppcnlem2  36458  knoppcnlem4  36460  knoppcnlem10  36466  unbdqndv2lem1  36473  knoppndvlem1  36476  knoppndvlem10  36485  knoppndvlem11  36486  knoppndvlem12  36487  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem18  36493  knoppndvlem19  36494  knoppndvlem20  36495  knoppndvlem21  36496  cnndvlem1  36501  taupi  37287  iccioo01  37291  relowlpssretop  37328  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem7  37597  poimirlem9  37599  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  itg2addnclem  37641  isbnd2  37753  isbnd3  37754  heiborlem7  37787  12gcd5e1  41962  lcm2un  41973  lcmineqlem19  42006  lcmineqlem20  42007  lcmineqlem22  42009  3lexlogpow5ineq2  42014  3lexlogpow5ineq4  42015  3lexlogpow5ineq3  42016  3lexlogpow2ineq1  42017  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1lem1  42021  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p2  42036  aks4d1p3  42037  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  aks4d1p9  42047  posbezout  42059  aks6d1c3  42082  2np3bcnp1  42103  2ap1caineq  42104  aks6d1c6lem4  42132  aks6d1c7lem1  42139  aks6d1c7lem2  42140  2xp3dxp2ge1d  42200  oexpreposd  42318  asin1half  42347  remul02  42395  sn-0ne2  42396  remul01  42397  flt4lem7  42629  rabren3dioph  42785  pellexlem2  42800  pellexlem5  42803  pell14qrgapw  42846  pellfundex  42856  rmspecsqrtnq  42876  jm2.24nn  42930  jm2.17a  42931  jm2.17b  42932  jm2.17c  42933  acongrep  42951  acongeq  42954  jm2.22  42966  jm2.23  42967  jm2.20nn  42968  jm3.1lem2  42989  expdiophlem1  42992  sqrtcval  43612  imo72b2lem0  44136  lhe4.4ex1a  44301  isosctrlem1ALT  44906  sineq0ALT  44909  lt3addmuld  45278  suplesup  45314  infleinflem2  45346  infleinf  45347  sumnnodd  45607  0ellimcdiv  45626  sinaover2ne0  45845  stoweidlem13  45990  stoweidlem14  45991  stoweidlem26  46003  stoweidlem49  46026  stoweidlem52  46029  wallispilem4  46045  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  stirlinglem3  46053  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  stirlinglem15  46065  stirlingr  46067  dirker2re  46069  dirkerval2  46071  dirkerre  46072  dirkerper  46073  dirkertrigeqlem1  46075  dirkertrigeqlem3  46077  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem24  46108  fourierdlem43  46127  fourierdlem44  46128  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem66  46149  fourierdlem68  46151  fourierdlem72  46155  fourierdlem76  46159  fourierdlem78  46161  fourierdlem79  46162  fourierdlem94  46177  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem113  46196  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  etransclem23  46234  salexct2  46316  salexct3  46319  salgencntex  46320  salgensscntex  46321  sge0ad2en  46408  ovnsubaddlem1  46547  smfmullem4  46771  smf2id  46778  2leaddle2  47275  p1lep2  47277  2ltceilhalf  47305  ceilhalfgt1  47306  2tceilhalfelfzo1  47309  rehalfge1  47312  ceilhalfnn  47313  ceil5half3  47317  fmtnoge3  47492  fmtnof1  47497  fmtnoprmfac2lem1  47528  fmtno4prmfac  47534  fmtno4prm  47537  2pwp1prm  47551  31prm  47559  sfprmdvdsmersenne  47565  lighneallem2  47568  lighneallem4a  47570  lighneallem4b  47571  requad01  47583  requad1  47584  requad2  47585  dfodd4  47621  nn0o1gt2ALTV  47656  nnoALTV  47657  nn0oALTV  47658  nn0e  47659  nneven  47660  perfectALTVlem1  47683  perfectALTVlem2  47684  341fppr2  47696  9fppr8  47699  fpprel2  47703  nfermltl2rev  47705  gbowgt5  47724  sbgoldbalt  47743  sgoldbeven3prm  47745  mogoldbb  47747  nnsum3primes4  47750  nnsum3primesgbe  47754  nnsum3primesle9  47756  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  cycl3grtri  47907  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  usgrexmpl2trifr  47989  gpgprismgrusgra  48010  gpg5nbgrvtx13starlem2  48022  gpg3nbgrvtx0  48026  gpg3kgrtriexlem1  48033  cznnring  48185  ply1mulgsumlem2  48311  zlmodzxznm  48421  zlmodzxzldeplem  48422  difmodm1lt  48450  nn0eo  48456  flnn0div2ge  48461  rege1logbzge0  48487  fldivexpfllog2  48493  logbpw2m1  48495  fllog2  48496  blenpw2m1  48507  nnpw2blen  48508  nnolog2flm1  48518  blennngt2o2  48520  dig2nn1st  48533  dig2nn0  48539  dig2bits  48542  dignn0flhalflem1  48543  dignn0flhalflem2  48544  dignn0flhalf  48546  nn0sumshdiglemA  48547  ackval42  48624  rrx2xpref1o  48646  itscnhlc0yqe  48687  itsclquadb  48704  2itscp  48709  itscnhlinecirc02p  48713  sepfsepc  48850