Theorem 2re 12219

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025  1c1 11027   + caddc 11029  2c2 12200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12208

This theorem is referenced by:  2cnALT  12221  3re  12225  3pos  12250  2lt3  12312  1lt3  12313  2lt4  12315  1lt4  12316  2lt5  12319  2lt6  12324  1lt6  12325  2lt7  12330  1lt7  12331  2lt8  12337  1lt8  12338  2lt9  12345  1lt9  12346  1le2  12349  2rene0  12351  halfre  12354  halfgt0  12356  halflt1  12358  rehalfcl  12368  halfpos2  12370  halfnneg2  12372  addltmul  12377  nominpos  12378  avglt1  12379  avglt2  12380  div4p1lem1div2  12396  nn0lele2xi  12457  nn0n0n1ge2b  12470  nn0ge2m1nn  12471  nn0le2is012  12556  halfnz  12570  3halfnz  12571  2lt10  12745  1lt10  12746  uzuzle23  12797  uzuzle24  12798  uz3m2nn  12807  2rp  12910  ge2halflem1  13022  xnn0n0n1ge2b  13046  fztpval  13502  fz0to4untppr  13546  fz0to5un2tp  13547  fzo0to42pr  13669  flhalf  13750  fldiv4p1lem1div2  13755  2txmodxeq0  13854  expubnd  14101  expmulnbnd  14158  nn0opthlem2  14192  faclbnd2  14214  faclbnd4lem1  14216  faclbnd5  14221  4bc2eq6  14252  hashgt23el  14347  hashfun  14360  hashge2el2dif  14403  hashge2el2difr  14404  hash3tpde  14416  wrdlenge2n0  14475  f1oun2prg  14840  01sqrexlem7  15171  sqrt4  15195  sqrt2gt1lt2  15197  abstri  15254  sqreulem  15283  amgm2  15293  caucvgrlem  15596  climcndslem1  15772  climcndslem2  15773  climcnds  15774  efcllem  16000  ege2le3  16013  ef01bndlem  16109  cos01bnd  16111  cos2bnd  16113  cos01gt0  16116  sin02gt0  16117  sincos2sgn  16119  sin4lt0  16120  eirrlem  16129  egt2lt3  16131  epos  16132  ene1  16135  sqrt2re  16175  mod2eq1n2dvds  16274  oddge22np1  16276  evennn2n  16278  nn0o1gt2  16308  nno  16309  nn0o  16310  nnoddm1d2  16313  bitsp1o  16360  bitsfzolem  16361  bitsfzo  16362  bitsfi  16364  6gcd4e2  16465  2mulprm  16620  ge2nprmge4  16628  isprm7  16635  3lcm2e6  16659  prmreclem2  16845  prmreclem6  16849  4sqlem11  16883  4sqlem12  16884  prmgaplem7  16985  2expltfac  17020  plusgndxnmulrndx  17217  starvndxnplusgndx  17225  scandxnplusgndx  17237  vscandxnplusgndx  17242  ipndxnplusgndx  17253  tsetndxnplusgndx  17277  plendxnplusgndx  17291  dsndxnplusgndx  17310  slotsdifunifndx  17321  efgredleme  19672  zringndrg  21423  chfacfscmul0  22802  chfacfpmmul0  22806  psmetge0  24256  xmetge0  24288  bl2in  24344  metnrmlem3  24806  iihalf1  24881  iihalf2  24884  pcoass  24980  tcphcphlem1  25191  csbren  25355  trirn  25356  minveclem2  25382  minveclem4  25388  pjthlem1  25393  ovolunlem1a  25453  dyadss  25551  opnmbllem  25558  vitalilem2  25566  vitalilem4  25568  mbfi1fseqlem5  25676  lhop1lem  25974  aaliou3lem2  26307  aaliou3lem8  26309  pilem2  26418  pilem3  26419  pipos  26424  sinhalfpilem  26428  sincosq1lem  26462  sincosq4sgn  26466  tangtx  26470  sinq12gt0  26472  sincos4thpi  26478  tan4thpi  26479  tan4thpiOLD  26480  sincos6thpi  26481  sineq0  26489  cos02pilt1  26491  cosq34lt1  26492  cosordlem  26495  cos0pilt1  26497  tanord1  26502  efif1olem1  26507  efif1olem2  26508  efif1olem4  26510  efif1o  26511  efifo  26512  2irrexpq  26696  cxpcn3lem  26713  root1id  26720  root1eq1  26721  root1cj  26722  cxpeq  26723  2logb9irr  26761  2logb3irr  26763  ang180lem1  26775  ang180lem2  26776  chordthmlem2  26799  1cubrlem  26807  atancj  26876  atantan  26889  atanbndlem  26891  atans2  26897  leibpi  26908  log2tlbnd  26911  log2ublem2  26913  log2ub  26915  divsqrtsumlem  26946  harmonicbnd3  26974  zetacvg  26981  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem4  26998  lgamgulmlem6  27000  lgamucov  27004  basellem1  27047  basellem2  27048  basellem3  27049  basellem5  27051  chtdif  27124  ppidif  27129  ppinncl  27140  chtrpcl  27141  ppieq0  27142  ppiltx  27143  ppiublem1  27169  ppiub  27171  chpeq0  27175  chteq0  27176  chtublem  27178  chtub  27179  chpval2  27185  chpub  27187  mersenne  27194  perfectlem1  27196  perfectlem2  27197  dchrptlem1  27231  dchrptlem2  27232  bcmono  27244  bclbnd  27247  bpos1lem  27249  bposlem1  27251  bposlem2  27252  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem7  27257  bposlem8  27258  bposlem9  27259  lgslem1  27264  lgsdirprm  27298  gausslemma2dlem0c  27325  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem3  27335  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisen  27346  lgsquadlem1  27347  lgsquadlem2  27348  m1lgs  27355  2lgslem1a1  27356  2lgslem1a2  27357  2lgslem1c  27360  2lgslem4  27373  2sqlem11  27396  2sq2  27400  2sqreultlem  27414  2sqreunnltlem  27417  chebbnd1lem1  27436  chebbnd1lem2  27437  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  chtppilimlem2  27441  chtppilim  27442  chto1ub  27443  chebbnd2  27444  chto1lb  27445  chpchtlim  27446  chpo1ub  27447  chpo1ubb  27448  rplogsumlem1  27451  rplogsumlem2  27452  dchrisumlem2  27457  dchrisumlem3  27458  dchrvmasumiflem1  27468  dchrisum0fno1  27478  dchrisum0re  27480  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2  27485  rplogsum  27494  mulog2sumlem1  27501  mulog2sumlem2  27502  log2sumbnd  27511  selberglem2  27513  selbergb  27516  selberg2b  27519  chpdifbndlem1  27520  logdivbnd  27523  selberg3lem1  27524  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrmax  27531  pntrsumbnd2  27534  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntpbnd  27555  pntibndlem2  27558  pntibndlem3  27559  pntibnd  27560  pntlemb  27564  pntlemg  27565  pntlemh  27566  pntlemr  27569  pntlemk  27573  pntlemo  27574  pnt2  27580  pnt  27581  ostth2lem1  27585  ostth3  27605  slotsinbpsd  28513  slotslnbpsd  28514  istrkg3ld  28533  tgldimor  28574  trgcgrg  28587  tgcgr4  28603  axlowdimlem6  29020  axlowdimlem16  29030  axlowdimlem17  29031  axlowdim  29034  upgrfi  29164  umgrupgr  29176  umgrislfupgrlem  29195  umgrislfupgr  29196  lfgrnloop  29198  usgruspgr  29253  usgrislfuspgr  29260  lfuhgr1v0e  29327  usgrexmpldifpr  29331  usgrexmplef  29332  nbusgrvtxm1  29452  vdegp1bi  29611  upgrewlkle2  29680  lfgrwlkprop  29759  upgr2pthnlp  29805  usgr2pthlem  29836  pthdlem1  29839  wwlksm1edg  29954  wwlksnextwrd  29970  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextproplem3  29984  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a2  30068  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlk2  30078  clwlkclwwlkf  30083  clwwlkext2edg  30131  konigsbergiedgw  30323  konigsbergssiedgw  30325  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  konigsberg  30332  frgrreggt1  30468  ex-pss  30503  ex-res  30516  ex-fv  30518  ex-fl  30522  ex-mod  30524  ex-abs  30530  nrt2irr  30548  ipidsq  30785  minvecolem2  30950  minvecolem4  30955  normlem7  31191  norm-ii-i  31212  norm3lemt  31227  normpar2i  31231  bcsiALT  31254  pjhthlem1  31466  opsqrlem6  32220  cdj3lem1  32509  addltmulALT  32521  nexple  32925  2exple2exp  32926  threehalves  32996  pfx1s2  33021  wrdt2ind  33035  cyc3conja  33239  drngidlhash  33515  evl1deg3  33659  rtelextdg2lem  33883  fldext2chn  33885  constraddcl  33919  iconstr  33923  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  sqsscirc1  34065  dya2iocucvr  34441  omssubadd  34457  oddpwdc  34511  eulerpartlemgc  34519  fibp1  34558  coinfliplem  34636  coinflipspace  34638  ballotlem2  34646  signstfveq0  34734  prodfzo03  34760  hgt750lemd  34805  logdivsqrle  34807  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  lfuhgr2  35313  usgrcyclgt2v  35325  acycgr2v  35344  subfacp1lem1  35373  subfacp1lem5  35378  subfacval3  35383  problem2  35860  problem5  35863  circum  35868  nn0prpwlem  36516  dnibndlem10  36687  knoppcnlem2  36694  knoppcnlem4  36696  knoppcnlem10  36702  unbdqndv2lem1  36709  knoppndvlem1  36712  knoppndvlem10  36721  knoppndvlem11  36722  knoppndvlem12  36723  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem17  36728  knoppndvlem18  36729  knoppndvlem19  36730  knoppndvlem20  36731  knoppndvlem21  36732  cnndvlem1  36737  taupi  37528  iccioo01  37532  relowlpssretop  37569  sin2h  37811  cos2h  37812  tan2h  37813  poimirlem7  37828  poimirlem9  37830  opnmbllem0  37857  mblfinlem1  37858  mblfinlem2  37859  itg2addnclem  37872  isbnd2  37984  isbnd3  37985  heiborlem7  38018  12gcd5e1  42257  lcm2un  42268  lcmineqlem19  42301  lcmineqlem20  42302  lcmineqlem22  42304  3lexlogpow5ineq2  42309  3lexlogpow5ineq4  42310  3lexlogpow5ineq3  42311  3lexlogpow2ineq1  42312  3lexlogpow2ineq2  42313  3lexlogpow5ineq5  42314  aks4d1lem1  42316  aks4d1p1p3  42323  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p5  42334  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  aks4d1p9  42342  posbezout  42354  aks6d1c3  42377  2np3bcnp1  42398  2ap1caineq  42399  aks6d1c6lem4  42427  aks6d1c7lem1  42434  aks6d1c7lem2  42435  oexpreposd  42577  asin1half  42612  remul02  42660  sn-0ne2  42661  remul01  42662  flt4lem7  42902  rabren3dioph  43057  pellexlem2  43072  pellexlem5  43075  pell14qrgapw  43118  pellfundex  43128  rmspecsqrtnq  43148  jm2.24nn  43201  jm2.17a  43202  jm2.17b  43203  jm2.17c  43204  acongrep  43222  acongeq  43225  jm2.22  43237  jm2.23  43238  jm2.20nn  43239  jm3.1lem2  43260  expdiophlem1  43263  sqrtcval  43882  imo72b2lem0  44406  lhe4.4ex1a  44570  isosctrlem1ALT  45174  sineq0ALT  45177  lt3addmuld  45549  suplesup  45584  infleinflem2  45615  infleinf  45616  sumnnodd  45876  0ellimcdiv  45893  sinaover2ne0  46112  stoweidlem13  46257  stoweidlem14  46258  stoweidlem26  46270  stoweidlem49  46293  stoweidlem52  46296  wallispilem4  46312  wallispilem5  46313  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  wallispi2  46317  stirlinglem1  46318  stirlinglem3  46320  stirlinglem5  46322  stirlinglem6  46323  stirlinglem7  46324  stirlinglem10  46327  stirlinglem11  46328  stirlinglem15  46332  stirlingr  46334  dirker2re  46336  dirkerval2  46338  dirkerre  46339  dirkerper  46340  dirkertrigeqlem1  46342  dirkertrigeqlem3  46344  dirkercncflem1  46347  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem24  46375  fourierdlem43  46394  fourierdlem44  46395  fourierdlem57  46407  fourierdlem58  46408  fourierdlem62  46412  fourierdlem66  46416  fourierdlem68  46418  fourierdlem72  46422  fourierdlem76  46426  fourierdlem78  46428  fourierdlem79  46429  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem113  46463  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  etransclem23  46501  salexct2  46583  salexct3  46586  salgencntex  46587  salgensscntex  46588  sge0ad2en  46675  ovnsubaddlem1  46814  smfmullem4  47038  smf2id  47045  nthrucw  47130  2leaddle2  47544  p1lep2  47546  2ltceilhalf  47574  ceilhalfgt1  47575  2tceilhalfelfzo1  47578  rehalfge1  47581  ceilhalfnn  47582  ceil5half3  47586  difmodm1lt  47605  fmtnoge3  47776  fmtnof1  47781  fmtnoprmfac2lem1  47812  fmtno4prmfac  47818  fmtno4prm  47821  2pwp1prm  47835  31prm  47843  sfprmdvdsmersenne  47849  lighneallem2  47852  lighneallem4a  47854  lighneallem4b  47855  requad01  47867  requad1  47868  requad2  47869  dfodd4  47905  nn0o1gt2ALTV  47940  nnoALTV  47941  nn0oALTV  47942  nn0e  47943  nneven  47944  perfectALTVlem1  47967  perfectALTVlem2  47968  341fppr2  47980  9fppr8  47983  fpprel2  47987  nfermltl2rev  47989  gbowgt5  48008  sbgoldbalt  48027  sgoldbeven3prm  48029  mogoldbb  48031  nnsum3primes4  48034  nnsum3primesgbe  48038  nnsum3primesle9  48040  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  cycl3grtri  48193  usgrexmpl1lem  48267  usgrexmpl2lem  48272  usgrexmpl2nb2  48279  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  usgrexmpl2trifr  48283  gpgprismgrusgra  48304  gpg5nbgrvtx13starlem2  48318  gpg3nbgrvtx0  48322  gpg3kgrtriexlem1  48329  cznnring  48508  ply1mulgsumlem2  48633  zlmodzxznm  48743  zlmodzxzldeplem  48744  nn0eo  48774  flnn0div2ge  48779  rege1logbzge0  48805  fldivexpfllog2  48811  logbpw2m1  48813  fllog2  48814  blenpw2m1  48825  nnpw2blen  48826  nnolog2flm1  48836  blennngt2o2  48838  dig2nn1st  48851  dig2nn0  48857  dig2bits  48860  dignn0flhalflem1  48861  dignn0flhalflem2  48862  dignn0flhalf  48864  nn0sumshdiglemA  48865  ackval42  48942  rrx2xpref1o  48964  itscnhlc0yqe  49005  itsclquadb  49022  2itscp  49027  itscnhlinecirc02p  49031  sepfsepc  49173