Theorem 2re 12292

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 12280	. 2 ⊢ 2 = (1 + 1)
2		1re 11181	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11197	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2858	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℝcr 11072  1c1 11074   + caddc 11076  2c2 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280

This theorem is referenced by:  2cnALT  12294  3re  12298  0le2  12320  2lt3  12391  2le3  12392  1lt3  12393  2lt4  12395  1lt4  12396  2lt5  12399  2lt6  12404  1lt6  12405  2lt7  12410  1lt7  12411  2lt8  12417  1lt8  12418  2lt9  12425  1lt9  12426  1le2  12429  2rene0  12431  halfre  12434  halfgt0  12436  halflt1  12438  rehalfcl  12448  halfpos2  12450  halfnneg2  12452  addltmul  12457  nominpos  12458  avglt1  12459  avglt2  12460  div4p1lem1div2  12476  nn0lele2xi  12537  nn0n0n1ge2b  12550  nn0ge2m1nn  12551  nn0le2is012  12637  halfnz  12651  3halfnz  12652  2lt10  12832  1lt10OLD  12834  uzuzle23  12885  uzuzle24  12886  uz3m2nn  12895  2rp  12998  ge2halflem1  13110  xnn0n0n1ge2b  13134  fztpval  13591  fz0to4untppr  13635  fz0to5un2tp  13636  fzo0to42pr  13759  flhalf  13840  fldiv4p1lem1div2  13845  2txmodxeq0  13944  expubnd  14191  expmulnbnd  14248  nn0opthlem2  14282  faclbnd2  14304  faclbnd4lem1  14306  faclbnd5  14311  4bc2eq6  14342  hashgt23el  14437  hashfun  14450  hashge2el2dif  14493  hashge2el2difr  14494  hash3tpde  14506  wrdlenge2n0  14565  f1oun2prg  14930  01sqrexlem7  15275  sqrt4  15299  sqrt2gt1lt2  15301  abstri  15358  sqreulem  15387  amgm2  15397  caucvgrlem  15700  climcndslem1  15879  climcndslem2  15880  climcnds  15881  efcllem  16107  ege2le3  16120  ef01bndlem  16216  cos01bnd  16218  cos2bnd  16220  cos01gt0  16223  sin02gt0  16224  sincos2sgn  16226  sin4lt0  16227  eirrlem  16236  egt2lt3  16238  epos  16239  ene1  16242  sqrt2re  16282  mod2eq1n2dvds  16381  oddge22np1  16383  evennn2n  16385  nn0o1gt2  16415  nno  16416  nn0o  16417  nnoddm1d2  16420  bitsp1o  16467  bitsfzolem  16468  bitsfzo  16469  bitsfi  16471  6gcd4e2  16572  2mulprm  16727  ge2nprmge4  16736  isprm7  16743  3lcm2e6  16767  prmreclem2  16953  prmreclem6  16957  4sqlem11  16991  4sqlem12  16992  prmgaplem7  17093  2expltfac  17128  plusgndxnmulrndx  17326  starvndxnplusgndx  17334  scandxnplusgndx  17346  vscandxnplusgndx  17351  ipndxnplusgndx  17362  tsetndxnplusgndx  17386  plendxnplusgndx  17400  dsndxnplusgndx  17419  slotsdifunifndx  17430  efgredleme  19783  zringndrg  21517  chfacfscmul0  22915  chfacfpmmul0  22919  psmetge0  24369  xmetge0  24401  bl2in  24457  metnrmlem3  24919  iihalf1  24990  iihalf2  24992  pcoass  25083  tcphcphlem1  25294  csbren  25458  trirn  25459  minveclem2  25485  minveclem4  25491  pjthlem1  25496  ovolunlem1a  25555  dyadss  25653  opnmbllem  25660  vitalilem2  25668  vitalilem4  25670  mbfi1fseqlem5  25778  lhop1lem  26072  aaliou3lem2  26404  aaliou3lem8  26406  pilem2  26512  pilem3  26513  2pire  26517  pipos  26520  sinhalfpilem  26525  sincosq1lem  26559  sincosq4sgn  26563  tangtx  26567  sinq12gt0  26569  sincos4thpi  26575  tan4thpi  26576  tan4thpiOLD  26577  sincos6thpi  26578  sineq0  26586  cos02pilt1  26588  cosq34lt1  26589  cosordlem  26592  cos0pilt1  26594  tanord1  26599  efif1olem1  26604  efif1olem2  26605  efif1olem4  26607  efif1o  26608  efifo  26609  2irrexpq  26793  cxpcn3lem  26809  root1id  26816  root1eq1  26817  root1cj  26818  cxpeq  26819  2logb9irr  26857  2logb3irr  26859  ang180lem1  26871  ang180lem2  26872  chordthmlem2  26895  1cubrlem  26903  atancj  26972  atantan  26985  atanbndlem  26987  atans2  26993  leibpi  27004  log2tlbnd  27007  log2ublem2  27009  log2ub  27011  divsqrtsumlem  27041  harmonicbnd3  27069  zetacvg  27076  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem6  27095  lgamucov  27099  basellem1  27142  basellem2  27143  basellem3  27144  basellem5  27146  chtdif  27219  ppidif  27224  ppinncl  27235  chtrpcl  27236  ppieq0  27237  ppiltx  27238  ppiublem1  27263  ppiub  27265  chpeq0  27269  chteq0  27270  chtublem  27272  chtub  27273  chpval2  27279  chpub  27281  mersenne  27288  perfectlem1  27290  perfectlem2  27291  dchrptlem1  27325  dchrptlem2  27326  bcmono  27338  bclbnd  27341  bpos1lem  27343  bposlem1  27345  bposlem2  27346  bposlem3  27347  bposlem4  27348  bposlem5  27349  bposlem6  27350  bposlem7  27351  bposlem8  27352  bposlem9  27353  lgslem1  27358  lgsdirprm  27392  gausslemma2dlem0c  27419  gausslemma2dlem1a  27426  gausslemma2dlem2  27428  gausslemma2dlem3  27429  lgseisenlem1  27436  lgseisenlem2  27437  lgseisenlem3  27438  lgseisen  27440  lgsquadlem1  27441  lgsquadlem2  27442  m1lgs  27449  2lgslem1a1  27450  2lgslem1a2  27451  2lgslem1c  27454  2lgslem4  27467  2sqlem11  27490  2sq2  27494  2sqreultlem  27508  2sqreunnltlem  27511  chebbnd1lem1  27530  chebbnd1lem2  27531  chebbnd1lem3  27532  chebbnd1  27533  chtppilimlem1  27534  chtppilimlem2  27535  chtppilim  27536  chto1ub  27537  chebbnd2  27538  chto1lb  27539  chpchtlim  27540  chpo1ub  27541  chpo1ubb  27542  rplogsumlem1  27545  rplogsumlem2  27546  dchrisumlem2  27551  dchrisumlem3  27552  dchrvmasumiflem1  27562  dchrisum0fno1  27572  dchrisum0re  27574  dchrisum0lem1b  27576  dchrisum0lem1  27577  dchrisum0lem2  27579  rplogsum  27588  mulog2sumlem1  27595  mulog2sumlem2  27596  log2sumbnd  27605  selberglem2  27607  selbergb  27610  selberg2b  27613  chpdifbndlem1  27614  logdivbnd  27617  selberg3lem1  27618  selberg3  27620  selberg4lem1  27621  selberg4  27622  pntrmax  27625  pntrsumbnd2  27628  selberg3r  27630  selberg4r  27631  selberg34r  27632  pntrlog2bndlem2  27639  pntrlog2bndlem3  27640  pntrlog2bndlem4  27641  pntrlog2bndlem5  27642  pntrlog2bndlem6  27644  pntrlog2bnd  27645  pntpbnd1a  27646  pntpbnd1  27647  pntpbnd2  27648  pntpbnd  27649  pntibndlem2  27652  pntibndlem3  27653  pntibnd  27654  pntlemb  27658  pntlemg  27659  pntlemh  27660  pntlemr  27663  pntlemk  27667  pntlemo  27668  pnt2  27674  pnt  27675  ostth2lem1  27679  ostth3  27699  slotsinbpsd  28607  slotslnbpsd  28608  istrkg3ld  28627  tgldimor  28668  trgcgrg  28681  tgcgr4  28697  axlowdimlem6  29145  axlowdimlem16  29155  axlowdimlem17  29156  axlowdim  29159  upgrfi  29289  umgrupgr  29301  umgrislfupgrlem  29320  umgrislfupgr  29321  lfgrnloop  29323  usgruspgr  29378  usgrislfuspgr  29385  lfuhgr1v0e  29452  usgrexmpldifpr  29456  usgrexmplef  29457  nbusgrvtxm1  29577  vdegp1bi  29735  upgrewlkle2  29804  lfgrwlkprop  29883  upgr2pthnlp  29929  usgr2pthlem  29960  pthdlem1  29963  wwlksm1edg  30078  wwlksnextwrd  30094  wwlksnextfun  30095  wwlksnextinj  30096  wwlksnextproplem3  30108  clwlkclwwlklem2a1  30191  clwlkclwwlklem2a2  30192  clwlkclwwlklem2fv1  30194  clwlkclwwlklem2fv2  30195  clwlkclwwlklem2a4  30196  clwlkclwwlklem2a  30197  clwlkclwwlklem2  30199  clwlkclwwlk2  30202  clwlkclwwlkf  30207  clwwlkext2edg  30255  konigsbergiedgw  30447  konigsbergssiedgw  30449  konigsberglem1  30451  konigsberglem2  30452  konigsberglem3  30453  konigsberg  30456  frgrreggt1  30592  ex-pss  30627  ex-res  30640  ex-fv  30642  ex-fl  30646  ex-mod  30648  ex-abs  30654  nrt2irr  30672  ipidsq  30910  minvecolem2  31075  minvecolem4  31080  normlem7  31316  norm-ii-i  31337  norm3lemt  31352  normpar2i  31356  bcsiALT  31379  pjhthlem1  31591  opsqrlem6  32345  cdj3lem1  32634  addltmulALT  32646  nexple  33032  2exple2exp  33033  threehalves  33089  pfx1s2  33114  wrdt2ind  33128  cyc3conja  33334  drngidlhash  33617  evl1deg3  33771  rtelextdg2lem  34020  fldext2chn  34022  constraddcl  34056  iconstr  34060  2sqr3minply  34074  2sqr3nconstr  34075  cos9thpinconstrlem1  34083  cos9thpinconstrlem2  34084  sqsscirc1  34202  dya2iocucvr  34578  omssubadd  34594  oddpwdc  34648  eulerpartlemgc  34656  fibp1  34695  coinfliplem  34773  coinflipspace  34775  ballotlem2  34783  signstfveq0  34868  prodfzo03  34894  hgt750lemd  34939  logdivsqrle  34941  hgt750lem  34942  hgt750lem2  34943  hgt750leme  34949  lfuhgr2  35466  usgrcyclgt2v  35478  acycgr2v  35497  subfacp1lem1  35526  subfacp1lem5  35531  subfacval3  35536  problem2  36013  problem5  36016  circum  36021  nn0prpwlem  36679  dnibndlem10  36922  knoppcnlem2  36929  knoppcnlem4  36931  knoppcnlem10  36937  unbdqndv2lem1  36944  knoppndvlem1  36947  knoppndvlem10  36956  knoppndvlem11  36957  knoppndvlem12  36958  knoppndvlem14  36960  knoppndvlem15  36961  knoppndvlem17  36963  knoppndvlem18  36964  knoppndvlem19  36965  knoppndvlem20  36966  knoppndvlem21  36967  cnndvlem1  36972  taupi  37812  iccioo01  37818  relowlpssretop  37855  sin2h  38106  cos2h  38107  tan2h  38108  poimirlem7  38123  poimirlem9  38125  opnmbllem0  38152  mblfinlem1  38153  mblfinlem2  38154  itg2addnclem  38167  isbnd2  38279  isbnd3  38280  heiborlem7  38313  12gcd5e1  42617  lcm2un  42628  lcmineqlem19  42661  lcmineqlem20  42662  lcmineqlem22  42664  3lexlogpow5ineq2  42669  3lexlogpow5ineq4  42670  3lexlogpow5ineq3  42671  3lexlogpow2ineq1  42672  3lexlogpow2ineq2  42673  3lexlogpow5ineq5  42674  aks4d1lem1  42676  aks4d1p1p3  42683  aks4d1p1p2  42684  aks4d1p1p4  42685  aks4d1p1p6  42687  aks4d1p1p7  42688  aks4d1p1p5  42689  aks4d1p1  42690  aks4d1p2  42691  aks4d1p3  42692  aks4d1p5  42694  aks4d1p6  42695  aks4d1p7d1  42696  aks4d1p7  42697  aks4d1p8  42701  aks4d1p9  42702  posbezout  42714  aks6d1c3  42737  2np3bcnp1  42758  2ap1caineq  42759  aks6d1c6lem4  42787  aks6d1c7lem1  42794  aks6d1c7lem2  42795  oexpreposd  42928  asin1half  42963  remul02  43011  sn-0ne2  43012  remul01  43013  flt4lem7  43238  rabren3dioph  43389  pellexlem2  43404  pellexlem5  43407  pell14qrgapw  43450  pellfundex  43460  rmspecsqrtnq  43480  jm2.24nn  43533  jm2.17a  43534  jm2.17b  43535  jm2.17c  43536  acongrep  43554  acongeq  43557  jm2.22  43569  jm2.23  43570  jm3.1lem2  43592  expdiophlem1  43595  sqrtcval  44214  imo72b2lem0  44738  lhe4.4ex1a  44902  isosctrlem1ALT  45506  sineq0ALT  45509  lt3addmuld  45877  suplesup  45912  infleinflem2  45943  infleinf  45944  sumnnodd  46203  0ellimcdiv  46220  sinaover2ne0  46439  stoweidlem13  46584  stoweidlem14  46585  stoweidlem26  46597  stoweidlem49  46620  stoweidlem52  46623  wallispilem4  46639  wallispilem5  46640  wallispi  46641  wallispi2lem1  46642  wallispi2lem2  46643  wallispi2  46644  stirlinglem1  46645  stirlinglem3  46647  stirlinglem5  46649  stirlinglem6  46650  stirlinglem7  46651  stirlinglem10  46654  stirlinglem11  46655  stirlinglem15  46659  stirlingr  46661  dirker2re  46663  dirkerval2  46665  dirkerre  46666  dirkertrigeqlem1  46669  dirkertrigeqlem3  46671  dirkercncflem1  46674  dirkercncflem4  46677  fourierdlem24  46702  fourierdlem43  46721  fourierdlem44  46722  fourierdlem57  46734  fourierdlem58  46735  fourierdlem62  46739  fourierdlem66  46743  fourierdlem68  46745  fourierdlem72  46749  fourierdlem76  46753  fourierdlem78  46755  fourierdlem79  46756  fourierdlem94  46771  fourierdlem103  46780  fourierdlem104  46781  fourierdlem111  46788  sqwvfoura  46799  sqwvfourb  46800  fourierswlem  46801  fouriersw  46802  etransclem23  46828  salexct2  46910  salexct3  46913  salgencntex  46914  salgensscntex  46915  sge0ad2en  47002  ovnsubaddlem1  47141  smfmullem4  47365  smf2id  47372  nthrucw  47459  goldrarr  47472  goldrapos  47474  2leaddle2  47889  p1lep2  47891  2ltceilhalf  47923  ceilhalfgt1  47924  2tceilhalfelfzo1  47927  rehalfge1  47930  ceilhalfnn  47931  ceil5half3  47937  difmodm1lt  47956  2timesltsq  47969  2timesltsqm1  47970  fmtnoge3  48136  fmtnof1  48141  fmtnoprmfac2lem1  48172  fmtno4prmfac  48178  fmtno4prm  48181  2pwp1prm  48195  31prm  48203  sfprmdvdsmersenne  48209  lighneallem2  48212  lighneallem4a  48214  lighneallem4b  48215  nprmdvdsfacm1lem2  48227  nprmdvdsfacm1lem4  48229  ppivalnnnprmge6  48232  requad01  48240  requad1  48241  requad2  48242  dfodd4  48278  nn0o1gt2ALTV  48313  nnoALTV  48314  nn0oALTV  48315  nn0e  48316  nneven  48317  perfectALTVlem1  48340  perfectALTVlem2  48341  341fppr2  48353  9fppr8  48356  fpprel2  48360  nfermltl2rev  48362  gbowgt5  48381  sbgoldbalt  48400  sgoldbeven3prm  48402  mogoldbb  48404  nnsum3primes4  48407  nnsum3primesgbe  48411  nnsum3primesle9  48413  nnsum4primesodd  48415  nnsum4primesoddALTV  48416  wtgoldbnnsum4prm  48421  bgoldbnnsum3prm  48423  cycl3grtri  48566  usgrexmpl1lem  48640  usgrexmpl2lem  48645  usgrexmpl2nb2  48652  usgrexmpl2nb3  48653  usgrexmpl2nb4  48654  usgrexmpl2nb5  48655  usgrexmpl2trifr  48656  gpgprismgrusgra  48677  gpg5nbgrvtx13starlem2  48691  gpg3nbgrvtx0  48695  gpg3kgrtriexlem1  48702  cznnring  48881  ply1mulgsumlem2  49006  zlmodzxznm  49116  zlmodzxzldeplem  49117  nn0eo  49147  flnn0div2ge  49152  rege1logbzge0  49178  fldivexpfllog2  49184  logbpw2m1  49186  fllog2  49187  blenpw2m1  49198  nnpw2blen  49199  nnolog2flm1  49209  blennngt2o2  49211  dig2nn1st  49224  dig2nn0  49230  dig2bits  49233  dignn0flhalflem1  49234  dignn0flhalflem2  49235  dignn0flhalf  49237  nn0sumshdiglemA  49238  ackval42  49315  rrx2xpref1o  49337  itscnhlc0yqe  49378  itsclquadb  49395  2itscp  49400  itscnhlinecirc02p  49404  sepfsepc  49546