Theorem 2re 11449

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 11438	. 2 ⊢ 2 = (1 + 1)
2		1re 10376	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 10392	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2855	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 6922  ℝcr 10271  1c1 10273   + caddc 10275  2c2 11430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-i2m1 10340  ax-1ne0 10341  ax-rrecex 10344  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-2 11438

This theorem is referenced by:  2cnALT  11451  3re  11455  2ne0  11486  3pos  11487  2lt3  11554  1lt3  11555  2lt4  11557  1lt4  11558  2lt5  11561  2lt6  11566  1lt6  11567  2lt7  11572  1lt7  11573  2lt8  11579  1lt8  11580  2lt9  11587  1lt9  11588  1le2  11591  2rene0  11593  halfre  11596  halfgt0  11598  halflt1  11600  rehalfcl  11608  halfpos2  11611  halfnneg2  11613  addltmul  11618  nominpos  11619  avglt1  11620  avglt2  11621  div4p1lem1div2  11637  nn0lele2xi  11699  nn0n0n1ge2b  11710  nn0ge2m1nn  11711  nn0le2is012  11793  halfnz  11807  3halfnz  11808  2lt10  11985  1lt10  11986  uzuzle23  12035  uz3m2nn  12037  2rp  12142  xnn0n0n1ge2b  12276  fztpval  12720  fz0to4untppr  12761  fzo0to42pr  12874  flhalf  12950  fldiv4p1lem1div2  12955  2txmodxeq0  13049  expubnd  13239  expmulnbnd  13315  nn0opthlem2  13374  faclbnd2  13396  faclbnd4lem1  13398  faclbnd5  13403  4bc2eq6  13434  hashfun  13538  hashge2el2dif  13576  hashge2el2difr  13577  wrdlenge2n0  13642  f1oun2prg  14068  pfx2  14098  sqrlem7  14396  sqrt4  14420  sqrt2gt1lt2  14422  abstri  14477  sqreulem  14506  amgm2  14516  caucvgrlem  14811  climcndslem1  14985  climcndslem2  14986  climcnds  14987  efcllem  15210  ege2le3  15222  ef01bndlem  15316  cos01bnd  15318  cos2bnd  15320  cos01gt0  15323  sin02gt0  15324  sincos2sgn  15326  sin4lt0  15327  eirrlem  15336  egt2lt3  15338  epos  15339  ene1  15342  sqrt2re  15383  mod2eq1n2dvds  15475  oddge22np1  15477  evennn2n  15479  n2dvds1OLD  15497  nn0o1gt2  15511  nno  15512  nn0o  15513  nnoddm1d2  15516  bitsp1o  15561  bitsfzolem  15562  bitsfzo  15563  bitsfi  15565  6gcd4e2  15661  isprm7  15824  3lcm2e6  15844  prmreclem2  16025  prmreclem6  16029  4sqlem11  16063  4sqlem12  16064  prmgaplem7  16165  2expltfac  16198  plusgndxnmulrndx  16390  oppgtset  18165  efgredleme  18541  mgpsca  18883  mgptset  18884  mgpds  18886  rmodislmod  19323  cnfldfun  20154  zringndrg  20234  matplusg  20624  chfacfscmul0  21070  chfacfpmmul0  21074  psmetge0  22525  xmetge0  22557  bl2in  22613  metnrmlem3  23072  iihalf1  23138  iihalf2  23140  pcoass  23231  tcphcphlem1  23441  csbren  23605  trirn  23606  minveclem2  23632  minveclem4  23638  pjthlem1  23643  ovolunlem1a  23700  dyadss  23798  opnmbllem  23805  vitalilem2  23813  vitalilem4  23815  mbfi1fseqlem5  23923  lhop1lem  24213  aaliou3lem2  24535  aaliou3lem8  24537  pilem2  24643  pilem3  24644  pilem3OLD  24645  pipos  24650  sinhalfpilem  24653  sincosq1lem  24687  sincosq4sgn  24691  tangtx  24695  sinq12gt0  24697  sincos4thpi  24703  tan4thpi  24704  sincos6thpi  24705  sineq0  24711  cosordlem  24715  tanord1  24721  efif1olem1  24726  efif1olem2  24727  efif1olem4  24729  efif1o  24730  efifo  24731  2irrexpq  24913  cxpcn3lem  24928  root1id  24935  root1eq1  24936  root1cj  24937  cxpeq  24938  logblog  24970  2logb9irr  24973  2logb3irr  24975  ang180lem1  24987  ang180lem2  24988  chordthmlem2  25011  1cubrlem  25019  atancj  25088  atantan  25101  atanbndlem  25103  atans2  25109  leibpilem1OLD  25119  leibpi  25121  log2tlbnd  25124  log2ublem2  25126  log2ub  25128  divsqrtsumlem  25158  harmonicbnd3  25186  zetacvg  25193  lgamgulmlem2  25208  lgamgulmlem3  25209  lgamgulmlem4  25210  lgamgulmlem6  25212  lgamucov  25216  basellem1  25259  basellem2  25260  basellem3  25261  basellem5  25263  chtdif  25336  ppidif  25341  ppinncl  25352  chtrpcl  25353  ppieq0  25354  ppiltx  25355  ppiublem1  25379  ppiub  25381  chpeq0  25385  chteq0  25386  chtublem  25388  chtub  25389  chpval2  25395  chpub  25397  mersenne  25404  perfectlem1  25406  perfectlem2  25407  dchrptlem1  25441  dchrptlem2  25442  bcmono  25454  bclbnd  25457  bpos1lem  25459  bposlem1  25461  bposlem2  25462  bposlem3  25463  bposlem4  25464  bposlem5  25465  bposlem6  25466  bposlem7  25467  bposlem8  25468  bposlem9  25469  lgslem1  25474  lgsdirprm  25508  gausslemma2dlem0c  25535  gausslemma2dlem1a  25542  gausslemma2dlem2  25544  gausslemma2dlem3  25545  lgseisenlem1  25552  lgseisenlem2  25553  lgseisenlem3  25554  lgseisen  25556  lgsquadlem1  25557  lgsquadlem2  25558  m1lgs  25565  2lgslem1a1  25566  2lgslem1a2  25567  2lgslem1c  25570  2lgslem4  25583  2sqlem11  25606  chebbnd1lem1  25610  chebbnd1lem2  25611  chebbnd1lem3  25612  chebbnd1  25613  chtppilimlem1  25614  chtppilimlem2  25615  chtppilim  25616  chto1ub  25617  chebbnd2  25618  chto1lb  25619  chpchtlim  25620  chpo1ub  25621  chpo1ubb  25622  rplogsumlem1  25625  rplogsumlem2  25626  dchrisumlem2  25631  dchrisumlem3  25632  dchrvmasumiflem1  25642  dchrisum0fno1  25652  dchrisum0re  25654  dchrisum0lem1b  25656  dchrisum0lem1  25657  dchrisum0lem2  25659  rplogsum  25668  mulog2sumlem1  25675  mulog2sumlem2  25676  log2sumbnd  25685  selberglem2  25687  selbergb  25690  selberg2b  25693  chpdifbndlem1  25694  logdivbnd  25697  selberg3lem1  25698  selberg3  25700  selberg4lem1  25701  selberg4  25702  pntrmax  25705  pntrsumbnd2  25708  selberg3r  25710  selberg4r  25711  selberg34r  25712  pntrlog2bndlem2  25719  pntrlog2bndlem3  25720  pntrlog2bndlem4  25721  pntrlog2bndlem5  25722  pntrlog2bndlem6  25724  pntrlog2bnd  25725  pntpbnd1a  25726  pntpbnd1  25727  pntpbnd2  25728  pntpbnd  25729  pntibndlem2  25732  pntibndlem3  25733  pntibnd  25734  pntlemb  25738  pntlemg  25739  pntlemh  25740  pntlemr  25743  pntlemk  25747  pntlemo  25748  pnt2  25754  pnt  25755  ostth2lem1  25759  ostth3  25779  istrkg3ld  25812  tgldimor  25853  trgcgrg  25866  tgcgr4  25882  axlowdimlem6  26296  axlowdimlem16  26306  axlowdimlem17  26307  axlowdim  26310  upgrfi  26439  umgrupgr  26451  umgrislfupgrlem  26470  umgrislfupgr  26471  lfgrnloop  26473  usgruspgr  26527  usgrislfuspgr  26533  lfuhgr1v0e  26601  usgrexmpldifpr  26605  usgrexmplef  26606  nbusgrvtxm1  26727  vdegp1bi  26885  upgrewlkle2  26954  lfgrwlkprop  27038  upgr2pthnlp  27084  usgr2pthlem  27115  pthdlem1  27118  wwlksm1edg  27230  wwlksm1edgOLD  27231  wwlksnextwrd  27261  wwlksnextfun  27262  wwlksnextinj  27263  wwlksnextwrdOLD  27266  wwlksnextfunOLD  27267  wwlksnextinjOLD  27268  wwlksnextproplem3  27287  wwlksnextproplem3OLD  27288  clwlkclwwlklem2a1  27372  clwlkclwwlklem2a2  27373  clwlkclwwlklem2fv1  27375  clwlkclwwlklem2fv2  27376  clwlkclwwlklem2a4  27377  clwlkclwwlklem2a  27378  clwlkclwwlklem2  27380  clwlkclwwlk2  27384  clwlkclwwlk2OLD  27385  clwlkclwwlkfOLD  27392  clwlkclwwlkf  27396  clwwlkext2edg  27453  konigsbergiedgw  27654  konigsbergssiedgw  27656  konigsberglem1  27658  konigsberglem2  27659  konigsberglem3  27660  konigsberg  27663  frgrreggt1  27825  ex-pss  27860  ex-res  27873  ex-fv  27875  ex-fl  27879  ex-mod  27881  ex-abs  27887  ipidsq  28137  minvecolem2  28303  minvecolem4  28308  normlem7  28545  norm-ii-i  28566  norm3lemt  28581  normpar2i  28585  bcsiALT  28608  pjhthlem1  28822  opsqrlem6  29576  cdj3lem1  29865  addltmulALT  29877  threehalves  30185  oppgle  30215  resvplusg  30395  sqsscirc1  30552  nexple  30669  dya2iocucvr  30944  omssubadd  30960  oddpwdc  31014  eulerpartlemgc  31022  fibp1  31062  coinfliplem  31139  coinflipspace  31141  ballotlem2  31149  signstfveq0  31255  signstfveq0OLD  31256  prodfzo03  31283  hgt750lemd  31328  logdivsqrle  31330  hgt750lem  31331  hgt750lem2  31332  hgt750leme  31338  subfacp1lem1  31760  subfacp1lem5  31765  subfacval3  31770  problem2  32157  problem5  32160  circum  32165  nn0prpwlem  32905  dnibndlem10  33060  knoppcnlem2  33067  knoppcnlem4  33069  knoppcnlem10  33075  unbdqndv2lem1  33082  knoppndvlem1  33085  knoppndvlem10  33094  knoppndvlem11  33095  knoppndvlem12  33096  knoppndvlem14  33098  knoppndvlem15  33099  knoppndvlem17  33101  knoppndvlem18  33102  knoppndvlem19  33103  knoppndvlem20  33104  knoppndvlem21  33105  cnndvlem1  33110  taupi  33765  relowlpssretop  33807  sin2h  34026  cos2h  34027  tan2h  34028  poimirlem7  34044  poimirlem9  34046  opnmbllem0  34073  mblfinlem1  34074  mblfinlem2  34075  itg2addnclem  34088  isbnd2  34208  isbnd3  34209  heiborlem7  34242  oexpreposd  38161  rabren3dioph  38343  pellexlem2  38358  pellexlem5  38361  pell14qrgapw  38404  pellfundex  38414  rmspecsqrtnq  38434  jm2.24nn  38489  jm2.17a  38490  jm2.17b  38491  jm2.17c  38492  acongrep  38510  acongeq  38513  jm2.22  38525  jm2.23  38526  jm2.20nn  38527  jm3.1lem2  38548  expdiophlem1  38551  imo72b2lem0  39425  lhe4.4ex1a  39488  isosctrlem1ALT  40107  sineq0ALT  40110  lt3addmuld  40428  suplesup  40467  infleinflem2  40499  infleinf  40500  sumnnodd  40774  0ellimcdiv  40793  sinaover2ne0  41011  stoweidlem13  41161  stoweidlem14  41162  stoweidlem26  41174  stoweidlem49  41197  stoweidlem52  41200  wallispilem4  41216  wallispilem5  41217  wallispi  41218  wallispi2lem1  41219  wallispi2lem2  41220  wallispi2  41221  stirlinglem1  41222  stirlinglem3  41224  stirlinglem5  41226  stirlinglem6  41227  stirlinglem7  41228  stirlinglem10  41231  stirlinglem11  41232  stirlinglem15  41236  stirlingr  41238  dirker2re  41240  dirkerval2  41242  dirkerre  41243  dirkerper  41244  dirkertrigeqlem1  41246  dirkertrigeqlem3  41248  dirkercncflem1  41251  dirkercncflem2  41252  dirkercncflem4  41254  fourierdlem24  41279  fourierdlem43  41298  fourierdlem44  41299  fourierdlem57  41311  fourierdlem58  41312  fourierdlem62  41316  fourierdlem66  41320  fourierdlem68  41322  fourierdlem72  41326  fourierdlem76  41330  fourierdlem78  41332  fourierdlem79  41333  fourierdlem94  41348  fourierdlem103  41357  fourierdlem104  41358  fourierdlem111  41365  fourierdlem113  41367  sqwvfoura  41376  sqwvfourb  41377  fourierswlem  41378  fouriersw  41379  etransclem23  41405  salexct2  41485  salexct3  41488  salgencntex  41489  salgensscntex  41490  sge0ad2en  41576  ovnsubaddlem1  41715  smfmullem4  41932  smf2id  41939  2leaddle2  42344  p1lep2  42346  fmtnoge3  42467  fmtnof1  42472  fmtnoprmfac2lem1  42503  fmtno4prmfac  42509  fmtno4prm  42512  2pwp1prm  42528  31prm  42537  sfprmdvdsmersenne  42545  lighneallem2  42548  lighneallem4a  42550  lighneallem4b  42551  requad01  42563  requad1  42564  requad2  42565  dfodd4  42600  nn0o1gt2ALTV  42634  nnoALTV  42635  nn0oALTV  42636  nn0e  42637  perfectALTVlem1  42659  perfectALTVlem2  42660  gbowgt5  42679  sbgoldbalt  42698  sgoldbeven3prm  42700  mogoldbb  42702  nnsum3primes4  42705  nnsum3primesgbe  42709  nnsum3primesle9  42711  nnsum4primesodd  42713  nnsum4primesoddALTV  42714  wtgoldbnnsum4prm  42719  bgoldbnnsum3prm  42721  cznnring  42975  ply1mulgsumlem2  43194  zlmodzxznm  43305  zlmodzxzldeplem  43306  difmodm1lt  43336  nn0eo  43341  flnn0div2ge  43346  rege1logbzge0  43372  fldivexpfllog2  43378  logbpw2m1  43380  fllog2  43381  blenpw2m1  43392  nnpw2blen  43393  nnolog2flm1  43403  blennngt2o2  43405  dig2nn1st  43418  dig2nn0  43424  dig2bits  43427  dignn0flhalflem1  43428  dignn0flhalflem2  43429  dignn0flhalf  43431  nn0sumshdiglemA  43432  rrx2xpref1o  43458  itscnhlc0yqe  43499  itsclquadb  43516  2itscp  43521  itscnhlinecirc02p  43525