Theorem 2re 11292

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 11281	. 2 ⊢ 2 = (1 + 1)
2		1re 10241	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 10255	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2846	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2145  (class class class)co 6793  ℝcr 10137  1c1 10139   + caddc 10141  2c2 11272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-i2m1 10206  ax-1ne0 10207  ax-rrecex 10210  ax-cnre 10211

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796  df-2 11281

This theorem is referenced by:  2cn  11293  3re  11296  2ne0  11315  3pos  11316  2lt3  11397  1lt3  11398  2lt4  11400  1lt4  11401  2lt5  11404  2lt6  11409  1lt6  11410  2lt7  11415  1lt7  11416  2lt8  11422  1lt8  11423  2lt9  11430  1lt9  11431  2lt10OLD  11439  1lt10OLD  11440  1le2  11443  2rene0  11445  halfre  11448  halfgt0  11450  halflt1  11452  rehalfcl  11460  halfpos2  11463  halfnneg2  11465  addltmul  11470  nominpos  11471  avglt1  11472  avglt2  11473  div4p1lem1div2  11489  nn0lele2xi  11550  nn0n0n1ge2b  11561  nn0ge2m1nn  11562  nn0le2is012  11643  halfnz  11657  3halfnz  11658  2lt10  11881  1lt10  11882  uzuzle23  11931  uz3m2nn  11933  2rp  12040  xnn0n0n1ge2b  12170  fztpval  12609  fz0to4untppr  12650  fzo0to42pr  12763  flhalf  12839  fldiv4p1lem1div2  12844  2txmodxeq0  12938  expubnd  13128  expmulnbnd  13203  nn0opthlem2  13260  faclbnd2  13282  faclbnd4lem1  13284  faclbnd5  13289  4bc2eq6  13320  hashfun  13426  hashge2el2dif  13464  hashge2el2difr  13465  wrdlenge2n0  13538  f1oun2prg  13871  sqrlem7  14197  sqrt4  14221  sqrt2gt1lt2  14223  abstri  14278  sqreulem  14307  amgm2  14317  caucvgrlem  14611  climcndslem1  14788  climcndslem2  14789  climcnds  14790  efcllem  15014  ege2le3  15026  ef01bndlem  15120  cos01bnd  15122  cos2bnd  15124  cos01gt0  15127  sin02gt0  15128  sincos2sgn  15130  sin4lt0  15131  eirrlem  15138  egt2lt3  15140  epos  15141  ene1  15144  sqrt2re  15186  mod2eq1n2dvds  15279  oddge22np1  15281  evennn2n  15283  nn0o1gt2  15305  nno  15306  nn0o  15307  nnoddm1d2  15310  n2dvds1  15312  bitsp1o  15363  bitsfzolem  15364  bitsfzo  15365  bitsfi  15367  6gcd4e2  15463  isprm7  15627  3lcm2e6  15647  prmreclem2  15828  prmreclem6  15832  4sqlem11  15866  4sqlem12  15867  prmgaplem7  15968  2expltfac  16006  plusgndxnmulrndx  16206  oppgtset  17989  efgredleme  18363  mgpsca  18704  mgptset  18705  mgpds  18707  rmodislmod  19141  cnfldfun  19973  zringndrg  20053  matplusg  20437  chfacfscmul0  20883  chfacfpmmul0  20887  psmetge0  22337  xmetge0  22369  bl2in  22425  metnrmlem3  22884  iihalf1  22950  iihalf2  22952  pcoass  23043  tchcphlem1  23253  csbren  23401  trirn  23402  minveclem2  23416  minveclem4  23422  pjthlem1  23427  ovolunlem1a  23484  dyadss  23582  opnmbllem  23589  vitalilem2  23597  vitalilem4  23599  mbfi1fseqlem5  23706  lhop1lem  23996  aaliou3lem2  24318  aaliou3lem8  24320  pilem2  24426  pilem3  24427  pilem3OLD  24428  pipos  24433  sinhalfpilem  24436  sincosq1lem  24470  sincosq4sgn  24474  tangtx  24478  sinq12gt0  24480  sincos4thpi  24486  tan4thpi  24487  sincos6thpi  24488  sineq0  24494  cosordlem  24498  tanord1  24504  efif1olem1  24509  efif1olem2  24510  efif1olem4  24512  efif1o  24513  efifo  24514  cxpcn3lem  24709  root1id  24716  root1eq1  24717  root1cj  24718  cxpeq  24719  logblog  24751  ang180lem1  24760  ang180lem2  24761  chordthmlem2  24781  1cubrlem  24789  atancj  24858  atantan  24871  atanbndlem  24873  atans2  24879  leibpilem1  24888  leibpi  24890  log2tlbnd  24893  log2ublem2  24895  log2ub  24897  divsqrtsumlem  24927  harmonicbnd3  24955  zetacvg  24962  lgamgulmlem2  24977  lgamgulmlem3  24978  lgamgulmlem4  24979  lgamgulmlem6  24981  lgamucov  24985  basellem1  25028  basellem2  25029  basellem3  25030  basellem5  25032  chtdif  25105  ppidif  25110  ppinncl  25121  chtrpcl  25122  ppieq0  25123  ppiltx  25124  ppiublem1  25148  ppiub  25150  chpeq0  25154  chteq0  25155  chtublem  25157  chtub  25158  chpval2  25164  chpub  25166  mersenne  25173  perfectlem1  25175  perfectlem2  25176  dchrptlem1  25210  dchrptlem2  25211  bcmono  25223  bclbnd  25226  bpos1lem  25228  bposlem1  25230  bposlem2  25231  bposlem3  25232  bposlem4  25233  bposlem5  25234  bposlem6  25235  bposlem7  25236  bposlem8  25237  bposlem9  25238  lgslem1  25243  lgsdirprm  25277  gausslemma2dlem0c  25304  gausslemma2dlem1a  25311  gausslemma2dlem2  25313  gausslemma2dlem3  25314  lgseisenlem1  25321  lgseisenlem2  25322  lgseisenlem3  25323  lgseisen  25325  lgsquadlem1  25326  lgsquadlem2  25327  m1lgs  25334  2lgslem1a1  25335  2lgslem1a2  25336  2lgslem1c  25339  2lgslem4  25352  2sqlem11  25375  chebbnd1lem1  25379  chebbnd1lem2  25380  chebbnd1lem3  25381  chebbnd1  25382  chtppilimlem1  25383  chtppilimlem2  25384  chtppilim  25385  chto1ub  25386  chebbnd2  25387  chto1lb  25388  chpchtlim  25389  chpo1ub  25390  chpo1ubb  25391  rplogsumlem1  25394  rplogsumlem2  25395  dchrisumlem2  25400  dchrisumlem3  25401  dchrvmasumiflem1  25411  dchrisum0fno1  25421  dchrisum0re  25423  dchrisum0lem1b  25425  dchrisum0lem1  25426  dchrisum0lem2  25428  rplogsum  25437  mulog2sumlem1  25444  mulog2sumlem2  25445  log2sumbnd  25454  selberglem2  25456  selbergb  25459  selberg2b  25462  chpdifbndlem1  25463  logdivbnd  25466  selberg3lem1  25467  selberg3  25469  selberg4lem1  25470  selberg4  25471  pntrmax  25474  pntrsumbnd2  25477  selberg3r  25479  selberg4r  25480  selberg34r  25481  pntrlog2bndlem2  25488  pntrlog2bndlem3  25489  pntrlog2bndlem4  25490  pntrlog2bndlem5  25491  pntrlog2bndlem6  25493  pntrlog2bnd  25494  pntpbnd1a  25495  pntpbnd1  25496  pntpbnd2  25497  pntpbnd  25498  pntibndlem2  25501  pntibndlem3  25502  pntibnd  25503  pntlemb  25507  pntlemg  25508  pntlemh  25509  pntlemr  25512  pntlemk  25516  pntlemo  25517  pnt2  25523  pnt  25524  ostth2lem1  25528  ostth3  25548  istrkg3ld  25581  tgldimor  25618  trgcgrg  25631  tgcgr4  25647  axlowdimlem6  26048  axlowdimlem16  26058  axlowdimlem17  26059  axlowdim  26062  upgrfi  26207  umgrupgr  26219  umgrislfupgrlem  26238  umgrislfupgr  26239  lfgrnloop  26241  usgruspgr  26295  usgrislfuspgr  26301  lfuhgr1v0e  26369  usgrexmpldifpr  26373  usgrexmplef  26374  nbusgrvtxm1  26504  vdegp1bi  26668  upgrewlkle2  26737  lfgrwlkprop  26819  upgr2pthnlp  26863  usgr2pthlem  26894  pthdlem1  26897  wwlksm1edg  27015  wwlksnextwrd  27041  wwlksnextfun  27042  wwlksnextinj  27043  wwlksnextproplem3  27056  clwlkclwwlklem2a1  27142  clwlkclwwlklem2a2  27143  clwlkclwwlklem2fv1  27145  clwlkclwwlklem2fv2  27146  clwlkclwwlklem2a4  27147  clwlkclwwlklem2a  27148  clwlkclwwlklem2  27150  clwlkclwwlk2  27153  clwlkclwwlkf  27158  clwwlkext2edg  27213  clwlksfclwwlkOLD  27243  konigsbergiedgw  27428  konigsbergssiedgw  27430  konigsberglem1  27432  konigsberglem2  27433  konigsberglem3  27434  konigsberg  27437  frgrreggt1  27592  ex-pss  27627  ex-res  27640  ex-fv  27642  ex-fl  27646  ex-mod  27648  ex-abs  27654  ipidsq  27905  minvecolem2  28071  minvecolem4  28076  normlem7  28313  norm-ii-i  28334  norm3lemt  28349  normpar2i  28353  bcsiALT  28376  pjhthlem1  28590  opsqrlem6  29344  cdj3lem1  29633  addltmulALT  29645  threehalves  29963  oppgle  29993  resvplusg  30173  sqsscirc1  30294  nexple  30411  dya2iocucvr  30686  omssubadd  30702  oddpwdc  30756  eulerpartlemgc  30764  fibp1  30803  coinfliplem  30880  coinflipspace  30882  ballotlem2  30890  signstfveq0  30994  prodfzo03  31021  hgt750lemd  31066  logdivsqrle  31068  hgt750lem  31069  hgt750lem2  31070  hgt750leme  31076  subfacp1lem1  31499  subfacp1lem5  31504  subfacval3  31509  problem2  31897  problem2OLD  31898  problem5  31901  circum  31906  nn0prpwlem  32654  dnibndlem10  32814  knoppcnlem2  32821  knoppcnlem4  32823  knoppcnlem10  32829  unbdqndv2lem1  32837  knoppndvlem1  32840  knoppndvlem10  32849  knoppndvlem11  32850  knoppndvlem12  32851  knoppndvlem14  32853  knoppndvlem15  32854  knoppndvlem17  32856  knoppndvlem18  32857  knoppndvlem19  32858  knoppndvlem20  32859  knoppndvlem21  32860  cnndvlem1  32865  taupi  33506  relowlpssretop  33549  sin2h  33732  cos2h  33733  tan2h  33734  poimirlem7  33749  poimirlem9  33751  opnmbllem0  33778  mblfinlem1  33779  mblfinlem2  33780  itg2addnclem  33793  isbnd2  33914  isbnd3  33915  heiborlem7  33948  rabren3dioph  37905  pellexlem2  37920  pellexlem5  37923  pell14qrgapw  37966  pellfundex  37976  rmspecsqrtnq  37996  rmspecsqrtnqOLD  37997  jm2.24nn  38052  jm2.17a  38053  jm2.17b  38054  jm2.17c  38055  acongrep  38073  acongeq  38076  jm2.22  38088  jm2.23  38089  jm2.20nn  38090  jm3.1lem2  38111  expdiophlem1  38114  imo72b2lem0  38991  lhe4.4ex1a  39054  isosctrlem1ALT  39692  sineq0ALT  39695  lt3addmuld  40032  suplesup  40071  infleinflem2  40103  infleinf  40104  sumnnodd  40380  0ellimcdiv  40399  sinaover2ne0  40597  stoweidlem13  40747  stoweidlem14  40748  stoweidlem26  40760  stoweidlem49  40783  stoweidlem52  40786  wallispilem4  40802  wallispilem5  40803  wallispi  40804  wallispi2lem1  40805  wallispi2lem2  40806  wallispi2  40807  stirlinglem1  40808  stirlinglem3  40810  stirlinglem5  40812  stirlinglem6  40813  stirlinglem7  40814  stirlinglem10  40817  stirlinglem11  40818  stirlinglem15  40822  stirlingr  40824  dirker2re  40826  dirkerval2  40828  dirkerre  40829  dirkerper  40830  dirkertrigeqlem1  40832  dirkertrigeqlem3  40834  dirkercncflem1  40837  dirkercncflem2  40838  dirkercncflem4  40840  fourierdlem24  40865  fourierdlem43  40884  fourierdlem44  40885  fourierdlem57  40897  fourierdlem58  40898  fourierdlem62  40902  fourierdlem66  40906  fourierdlem68  40908  fourierdlem72  40912  fourierdlem76  40916  fourierdlem78  40918  fourierdlem79  40919  fourierdlem94  40934  fourierdlem103  40943  fourierdlem104  40944  fourierdlem111  40951  fourierdlem113  40953  sqwvfoura  40962  sqwvfourb  40963  fourierswlem  40964  fouriersw  40965  etransclem23  40991  salexct2  41074  salexct3  41077  salgencntex  41078  salgensscntex  41079  sge0ad2en  41165  ovnsubaddlem1  41304  smfmullem4  41521  smf2id  41528  2leaddle2  41840  p1lep2  41842  pfx2  41940  fmtnoge3  41970  fmtnof1  41975  fmtnoprmfac2lem1  42006  fmtno4prmfac  42012  fmtno4prm  42015  2pwp1prm  42031  31prm  42040  sfprmdvdsmersenne  42048  lighneallem2  42051  lighneallem4a  42053  lighneallem4b  42054  dfodd4  42099  nn0o1gt2ALTV  42133  nnoALTV  42134  nn0oALTV  42135  nn0e  42136  perfectALTVlem1  42158  perfectALTVlem2  42159  gbowgt5  42178  sbgoldbalt  42197  sgoldbeven3prm  42199  mogoldbb  42201  nnsum3primes4  42204  nnsum3primesgbe  42208  nnsum3primesle9  42210  nnsum4primesodd  42212  nnsum4primesoddALTV  42213  wtgoldbnnsum4prm  42218  bgoldbnnsum3prm  42220  cznnring  42484  ply1mulgsumlem2  42703  zlmodzxznm  42814  zlmodzxzldeplem  42815  difmodm1lt  42845  nn0eo  42850  flnn0div2ge  42855  rege1logbzge0  42881  fldivexpfllog2  42887  logbpw2m1  42889  fllog2  42890  blenpw2m1  42901  nnpw2blen  42902  nnolog2flm1  42912  blennngt2o2  42914  dig2nn1st  42927  dig2nn0  42933  dig2bits  42936  dignn0flhalflem1  42937  dignn0flhalflem2  42938  dignn0flhalf  42940  nn0sumshdiglemA  42941