Theorem 2re 12310

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 12298	. 2 ⊢ 2 = (1 + 1)
2		1re 11203	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11219	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2859	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098  2c2 12290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298

This theorem is referenced by:  2cnALT  12312  3re  12316  0le2  12338  2lt3  12409  2le3  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  12850  1lt10OLD  12852  uzuzle23  12903  uzuzle24  12904  uz3m2nn  12913  2rp  13016  ge2halflem1  13128  xnn0n0n1ge2b  13152  fztpval  13610  fz0to4untppr  13654  fz0to5un2tp  13655  fzo0to42pr  13778  flhalf  13859  fldiv4p1lem1div2  13864  2txmodxeq0  13963  expubnd  14210  expmulnbnd  14267  nn0opthlem2  14301  faclbnd2  14323  faclbnd4lem1  14325  faclbnd5  14330  4bc2eq6  14361  hashgt23el  14457  hashfun  14470  hashge2el2dif  14513  hashge2el2difr  14514  hash3tpde  14526  wrdlenge2n0  14585  f1oun2prg  14950  01sqrexlem7  15295  sqrt4  15319  sqrt2gt1lt2  15321  abstri  15378  sqreulem  15407  amgm2  15417  caucvgrlem  15720  climcndslem1  15899  climcndslem2  15900  climcnds  15901  efcllem  16126  ege2le3  16139  ef01bndlem  16235  cos01bnd  16237  cos2bnd  16239  cos01gt0  16242  sin02gt0  16243  sincos2sgn  16245  sin4lt0  16246  eirrlem  16255  egt2lt3  16257  epos  16258  ene1  16261  sqrt2re  16301  mod2eq1n2dvds  16400  oddge22np1  16402  evennn2n  16404  nn0o1gt2  16434  nno  16435  nn0o  16436  nnoddm1d2  16439  bitsp1o  16486  bitsfzolem  16487  bitsfzo  16488  bitsfi  16490  6gcd4e2  16591  2mulprm  16746  ge2nprmge4  16755  isprm7  16762  3lcm2e6  16786  prmreclem2  16972  prmreclem6  16976  4sqlem11  17010  4sqlem12  17011  prmgaplem7  17112  2expltfac  17147  plusgndxnmulrndx  17345  starvndxnplusgndx  17353  scandxnplusgndx  17365  vscandxnplusgndx  17370  ipndxnplusgndx  17381  tsetndxnplusgndx  17405  plendxnplusgndx  17419  dsndxnplusgndx  17438  slotsdifunifndx  17449  efgredleme  19808  zringndrg  21618  chfacfscmul0  23015  chfacfpmmul0  23019  psmetge0  24469  xmetge0  24501  bl2in  24557  metnrmlem3  25019  iihalf1  25090  iihalf2  25092  pcoass  25183  tcphcphlem1  25394  csbren  25558  trirn  25559  minveclem2  25585  minveclem4  25591  pjthlem1  25596  ovolunlem1a  25655  dyadss  25753  opnmbllem  25760  vitalilem2  25768  vitalilem4  25770  mbfi1fseqlem5  25878  lhop1lem  26172  aaliou3lem2  26506  aaliou3lem8  26508  pilem2  26615  pilem3  26616  2pire  26620  pipos  26623  sinhalfpilem  26628  sincosq1lem  26662  sincosq4sgn  26666  tangtx  26670  sinq12gt0  26672  sincos4thpi  26678  tan4thpi  26679  tan4thpiOLD  26680  sincos6thpi  26681  sineq0  26689  cos02pilt1  26691  cosq34lt1  26692  cosordlem  26695  cos0pilt1  26697  tanord1  26702  efif1olem1  26707  efif1olem2  26708  efif1olem4  26710  efif1o  26711  efifo  26712  2irrexpq  26896  cxpcn3lem  26912  root1id  26919  root1eq1  26920  root1cj  26921  cxpeq  26922  2logb9irr  26960  2logb3irr  26962  ang180lem1  26974  ang180lem2  26975  chordthmlem2  26998  1cubrlem  27006  atancj  27075  atantan  27088  atanbndlem  27090  atans2  27096  leibpi  27107  log2tlbnd  27110  log2ublem2  27112  log2ub  27114  divsqrtsumlem  27144  harmonicbnd3  27172  zetacvg  27179  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem4  27196  lgamgulmlem6  27198  lgamucov  27202  basellem1  27245  basellem2  27246  basellem3  27247  basellem5  27249  chtdif  27322  ppidif  27327  ppinncl  27338  chtrpcl  27339  ppieq0  27340  ppiltx  27341  ppiublem1  27366  ppiub  27368  chpeq0  27372  chteq0  27373  chtublem  27375  chtub  27376  chpval2  27382  chpub  27384  mersenne  27391  perfectlem1  27393  perfectlem2  27394  dchrptlem1  27428  dchrptlem2  27429  bcmono  27441  bclbnd  27444  bpos1lem  27446  bposlem1  27448  bposlem2  27449  bposlem3  27450  bposlem4  27451  bposlem5  27452  bposlem6  27453  bposlem7  27454  bposlem8  27455  bposlem9  27456  lgslem1  27461  lgsdirprm  27495  gausslemma2dlem0c  27522  gausslemma2dlem1a  27529  gausslemma2dlem2  27531  gausslemma2dlem3  27532  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisen  27543  lgsquadlem1  27544  lgsquadlem2  27545  m1lgs  27552  2lgslem1a1  27553  2lgslem1a2  27554  2lgslem1c  27557  2lgslem4  27570  2sqlem11  27593  2sq2  27597  2sqreultlem  27611  2sqreunnltlem  27614  chebbnd1lem1  27633  chebbnd1lem2  27634  chebbnd1lem3  27635  chebbnd1  27636  chtppilimlem1  27637  chtppilimlem2  27638  chtppilim  27639  chto1ub  27640  chebbnd2  27641  chto1lb  27642  chpchtlim  27643  chpo1ub  27644  chpo1ubb  27645  rplogsumlem1  27648  rplogsumlem2  27649  dchrisumlem2  27654  dchrisumlem3  27655  dchrvmasumiflem1  27665  dchrisum0fno1  27675  dchrisum0re  27677  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2  27682  rplogsum  27691  mulog2sumlem1  27698  mulog2sumlem2  27699  log2sumbnd  27708  selberglem2  27710  selbergb  27713  selberg2b  27716  chpdifbndlem1  27717  logdivbnd  27720  selberg3lem1  27721  selberg3  27723  selberg4lem1  27724  selberg4  27725  pntrmax  27728  pntrsumbnd2  27731  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntpbnd  27752  pntibndlem2  27755  pntibndlem3  27756  pntibnd  27757  pntlemb  27761  pntlemg  27762  pntlemh  27763  pntlemr  27766  pntlemk  27770  pntlemo  27771  pnt2  27777  pnt  27778  ostth2lem1  27782  ostth3  27802  slotsinbpsd  28710  slotslnbpsd  28711  istrkg3ld  28730  tgldimor  28771  trgcgrg  28784  tgcgr4  28800  axlowdimlem6  29297  axlowdimlem16  29307  axlowdimlem17  29308  axlowdim  29311  upgrfi  29441  umgrupgr  29453  umgrislfupgrlem  29472  umgrislfupgr  29473  lfgrnloop  29475  usgruspgr  29530  usgrislfuspgr  29537  lfuhgr1v0e  29604  usgrexmpldifpr  29608  usgrexmplef  29609  nbusgrvtxm1  29729  vdegp1bi  29887  upgrewlkle2  29956  lfgrwlkprop  30035  upgr2pthnlp  30081  usgr2pthlem  30112  pthdlem1  30115  wwlksm1edg  30230  wwlksnextwrd  30246  wwlksnextfun  30247  wwlksnextinj  30248  wwlksnextproplem3  30260  clwlkclwwlklem2a1  30343  clwlkclwwlklem2a2  30344  clwlkclwwlklem2fv1  30346  clwlkclwwlklem2fv2  30347  clwlkclwwlklem2a4  30348  clwlkclwwlklem2a  30349  clwlkclwwlklem2  30351  clwlkclwwlk2  30354  clwlkclwwlkf  30359  clwwlkext2edg  30407  konigsbergiedgw  30599  konigsbergssiedgw  30601  konigsberglem1  30603  konigsberglem2  30604  konigsberglem3  30605  konigsberg  30608  frgrreggt1  30744  ex-pss  30779  ex-res  30792  ex-fv  30794  ex-fl  30798  ex-mod  30800  ex-abs  30806  nrt2irr  30824  ipidsq  31062  minvecolem2  31227  minvecolem4  31232  normlem7  31468  norm-ii-i  31489  norm3lemt  31504  normpar2i  31508  bcsiALT  31531  pjhthlem1  31743  opsqrlem6  32497  cdj3lem1  32786  addltmulALT  32798  nexple  33177  2exple2exp  33178  threehalves  33234  pfx1s2  33259  wrdt2ind  33273  cyc3conja  33477  drngidlhash  33741  evl1deg3  33868  rtelextdg2lem  34116  fldext2chn  34118  constraddcl  34152  iconstr  34156  2sqr3minply  34170  2sqr3nconstr  34171  cos9thpinconstrlem1  34179  cos9thpinconstrlem2  34180  sqsscirc1  34298  dya2iocucvr  34674  omssubadd  34690  oddpwdc  34744  eulerpartlemgc  34752  fibp1  34791  coinfliplem  34869  coinflipspace  34871  ballotlem2  34879  signstfveq0  34964  prodfzo03  34990  hgt750lemd  35035  logdivsqrle  35037  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  lfuhgr2  35611  usgrcyclgt2v  35623  acycgr2v  35642  subfacp1lem1  35671  subfacp1lem5  35676  subfacval3  35681  problem2  36158  problem5  36161  circum  36166  nn0prpwlem  36833  dnibndlem10  37076  knoppcnlem2  37083  knoppcnlem4  37085  knoppcnlem10  37091  unbdqndv2lem1  37098  knoppndvlem1  37101  knoppndvlem10  37110  knoppndvlem11  37111  knoppndvlem12  37112  knoppndvlem14  37114  knoppndvlem15  37115  knoppndvlem17  37117  knoppndvlem18  37118  knoppndvlem19  37119  knoppndvlem20  37120  knoppndvlem21  37121  cnndvlem1  37126  taupi  37967  iccioo01  37973  relowlpssretop  38010  sin2h  38261  cos2h  38262  tan2h  38263  poimirlem7  38278  poimirlem9  38280  opnmbllem0  38307  mblfinlem1  38308  mblfinlem2  38309  itg2addnclem  38322  isbnd2  38434  isbnd3  38435  heiborlem7  38468  12gcd5e1  42770  lcm2un  42781  lcmineqlem19  42814  lcmineqlem20  42815  lcmineqlem22  42817  3lexlogpow5ineq2  42822  3lexlogpow5ineq4  42823  3lexlogpow5ineq3  42824  3lexlogpow2ineq1  42825  3lexlogpow2ineq2  42826  3lexlogpow5ineq5  42827  aks4d1lem1  42829  aks4d1p1p3  42836  aks4d1p1p2  42837  aks4d1p1p4  42838  aks4d1p1p6  42840  aks4d1p1p7  42841  aks4d1p1p5  42842  aks4d1p1  42843  aks4d1p2  42844  aks4d1p3  42845  aks4d1p5  42847  aks4d1p6  42848  aks4d1p7d1  42849  aks4d1p7  42850  aks4d1p8  42854  aks4d1p9  42855  posbezout  42867  aks6d1c3  42890  2np3bcnp1  42911  2ap1caineq  42912  aks6d1c6lem4  42940  aks6d1c7lem1  42947  aks6d1c7lem2  42948  oexpreposd  43083  asin1half  43118  remul02  43166  sn-0ne2  43167  remul01  43168  flt4lem7  43391  rabren3dioph  43542  pellexlem2  43557  pellexlem5  43560  pell14qrgapw  43603  pellfundex  43613  rmspecsqrtnq  43633  jm2.24nn  43686  jm2.17a  43687  jm2.17b  43688  jm2.17c  43689  acongrep  43707  acongeq  43710  jm2.22  43722  jm2.23  43723  jm3.1lem2  43745  expdiophlem1  43748  sqrtcval  44367  imo72b2lem0  44891  lhe4.4ex1a  45039  isosctrlem1ALT  45642  sineq0ALT  45645  lt3addmuld  46020  suplesup  46055  infleinflem2  46086  infleinf  46087  sumnnodd  46346  0ellimcdiv  46363  sinaover2ne0  46582  stoweidlem13  46727  stoweidlem14  46728  stoweidlem26  46740  stoweidlem49  46763  stoweidlem52  46766  wallispilem4  46782  wallispilem5  46783  wallispi  46784  wallispi2lem1  46785  wallispi2lem2  46786  wallispi2  46787  stirlinglem1  46788  stirlinglem3  46790  stirlinglem5  46792  stirlinglem6  46793  stirlinglem7  46794  stirlinglem10  46797  stirlinglem11  46798  stirlinglem15  46802  stirlingr  46804  dirker2re  46806  dirkerval2  46808  dirkerre  46809  dirkertrigeqlem1  46812  dirkertrigeqlem3  46814  dirkercncflem1  46817  dirkercncflem4  46820  fourierdlem24  46845  fourierdlem43  46864  fourierdlem44  46865  fourierdlem57  46877  fourierdlem58  46878  fourierdlem62  46882  fourierdlem66  46886  fourierdlem68  46888  fourierdlem72  46892  fourierdlem76  46896  fourierdlem78  46898  fourierdlem79  46899  fourierdlem94  46914  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  sqwvfoura  46942  sqwvfourb  46943  fourierswlem  46944  fouriersw  46945  etransclem23  46971  salexct2  47053  salexct3  47056  salgencntex  47057  salgensscntex  47058  sge0ad2en  47145  ovnsubaddlem1  47284  smfmullem4  47508  smf2id  47515  goldrarr  47618  goldrapos  47620  2leaddle2  48035  p1lep2  48037  2ltceilhalf  48069  ceilhalfgt1  48070  2tceilhalfelfzo1  48073  rehalfge1  48076  ceilhalfnn  48077  ceil5half3  48083  difmodm1lt  48102  2timesltsq  48115  2timesltsqm1  48116  fmtnoge3  48282  fmtnof1  48287  fmtnoprmfac2lem1  48318  fmtno4prmfac  48324  fmtno4prm  48327  2pwp1prm  48341  31prm  48349  sfprmdvdsmersenne  48355  lighneallem2  48358  lighneallem4a  48360  lighneallem4b  48361  nprmdvdsfacm1lem2  48373  nprmdvdsfacm1lem4  48375  ppivalnnnprmge6  48378  requad01  48386  requad1  48387  requad2  48388  dfodd4  48424  nn0o1gt2ALTV  48459  nnoALTV  48460  nn0oALTV  48461  nn0e  48462  nneven  48463  perfectALTVlem1  48486  perfectALTVlem2  48487  341fppr2  48499  9fppr8  48502  fpprel2  48506  nfermltl2rev  48508  gbowgt5  48527  sbgoldbalt  48546  sgoldbeven3prm  48548  mogoldbb  48550  nnsum3primes4  48553  nnsum3primesgbe  48557  nnsum3primesle9  48559  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  cycl3grtri  48712  usgrexmpl1lem  48786  usgrexmpl2lem  48791  usgrexmpl2nb2  48798  usgrexmpl2nb3  48799  usgrexmpl2nb4  48800  usgrexmpl2nb5  48801  usgrexmpl2trifr  48802  gpgprismgrusgra  48823  gpg5nbgrvtx13starlem2  48837  gpg3nbgrvtx0  48841  gpg3kgrtriexlem1  48848  cznnring  49027  ply1mulgsumlem2  49167  zlmodzxznm  49277  zlmodzxzldeplem  49278  nn0eo  49308  flnn0div2ge  49313  rege1logbzge0  49339  fldivexpfllog2  49345  logbpw2m1  49347  fllog2  49348  blenpw2m1  49359  nnpw2blen  49360  nnolog2flm1  49370  blennngt2o2  49372  dig2nn1st  49385  dig2nn0  49391  dig2bits  49394  dignn0flhalflem1  49395  dignn0flhalflem2  49396  dignn0flhalf  49398  nn0sumshdiglemA  49399  ackval42  49476  rrx2xpref1o  49498  itscnhlc0yqe  49539  itsclquadb  49556  2itscp  49561  itscnhlinecirc02p  49565  sepfsepc  49706