Theorem 2re 10025

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 10014	. 2 |- 2 = ( 1 + 1 )
2		1re 9046	. . 3 |- 1 e. RR
3	2, 2	readdcli 9059	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2474	1 |- 2 e. RR

Syntax hints:   e. wcel 1721  (class class class)co 6040   RRcr 8945   1c1 8947   + caddc 8949   2c2 10005

This theorem is referenced by:  2cn  10026  3re  10027  2ne0  10039  3pos  10040  2lt3  10099  1lt3  10100  2lt4  10102  1lt4  10103  2lt5  10106  2lt6  10111  1lt6  10112  2lt7  10117  1lt7  10118  2lt8  10124  1lt8  10125  2lt9  10132  1lt9  10133  2lt10  10141  1lt10  10142  halfgt0  10144  halflt1  10145  halfpm6th  10148  rehalfcl  10150  halfpos2  10153  halfnneg2  10155  addltmul  10159  nominpos  10160  avglt1  10161  avglt2  10162  nn0lele2xi  10228  nn0n0n1ge2b  10237  halfnz  10304  2rp  10573  fzprval  11062  fztpval  11063  4fvwrd4  11076  fzo0to42pr  11141  flhalf  11186  expubnd  11395  expmulnbnd  11466  nn0opthlem2  11517  faclbnd2  11537  faclbnd4lem1  11539  faclbnd5  11544  hashfun  11655  f1oun2prg  11819  sqrlem7  12009  sqr4  12033  sqr2gt1lt2  12035  abstri  12089  rddif  12099  absrdbnd  12100  sqreulem  12118  amgm2  12128  caucvgrlem  12421  iseralt  12433  climcndslem1  12584  climcndslem2  12585  climcnds  12586  geoihalfsum  12614  efcllem  12635  ege2le3  12647  ef01bndlem  12740  cos01bnd  12742  cos2bnd  12744  cos01gt0  12747  sin02gt0  12748  sincos2sgn  12750  sin4lt0  12751  eirrlem  12758  egt2lt3  12760  epos  12761  sqr2re  12804  oexpneg  12866  bitsp1o  12900  bitsfzolem  12901  bitsfzo  12902  bitsmod  12903  bitsfi  12904  bitsinv1lem  12908  isprm3  13043  oddprm  13144  iserodd  13164  prmreclem2  13240  prmreclem6  13244  4sqlem11  13278  4sqlem12  13279  2expltfac  13381  oppgtset  15103  efgredleme  15330  mgpsca  15610  mgptset  15611  mgpds  15613  abvtrivd  15883  psmetge0  18296  xmetge0  18327  bl2in  18383  metnrmlem3  18844  iihalf1  18909  iihalf2  18911  pcoass  19002  tchcphlem1  19145  minveclem2  19280  minveclem4  19286  pjthlem1  19291  ovolunlem1a  19345  dyadss  19439  opnmbllem  19446  vitalilem2  19454  vitalilem4  19456  mbfi1fseqlem5  19564  lhop1lem  19850  aaliou3lem1  20212  aaliou3lem2  20213  aaliou3lem3  20214  aaliou3lem8  20215  pilem2  20321  pilem3  20322  pipos  20326  sinhalfpilem  20327  sincosq1lem  20358  sincosq4sgn  20362  tangtx  20366  sinq12gt0  20368  sincos4thpi  20374  tan4thpi  20375  sincos6thpi  20376  sineq0  20382  cosordlem  20386  tanord1  20392  efif1olem1  20397  efif1olem2  20398  efif1olem4  20400  efif1o  20401  efifo  20402  logsqr  20548  cxpcn3lem  20584  root1id  20591  root1eq1  20592  root1cj  20593  cxpeq  20594  ang180lem1  20604  ang180lem2  20605  chordthmlem2  20627  1cubrlem  20634  atancj  20703  atantan  20716  atanbndlem  20718  atans2  20724  leibpilem1  20733  leibpi  20735  log2tlbnd  20738  log2ublem2  20740  log2ub  20742  divsqrsumlem  20771  harmonicbnd3  20799  basellem1  20816  basellem2  20817  basellem3  20818  basellem5  20820  ppisval  20839  chtdif  20894  ppidif  20899  ppinncl  20910  chtrpcl  20911  ppieq0  20912  ppiltx  20913  ppiublem1  20939  ppiub  20941  chpeq0  20945  chteq0  20946  chtublem  20948  chtub  20949  chpval2  20955  chpub  20957  mersenne  20964  perfectlem1  20966  perfectlem2  20967  dchrptlem1  21001  dchrptlem2  21002  bcmono  21014  bclbnd  21017  bpos1lem  21019  bposlem1  21021  bposlem2  21022  bposlem3  21023  bposlem4  21024  bposlem5  21025  bposlem6  21026  bposlem7  21027  bposlem8  21028  bposlem9  21029  lgslem1  21033  lgsdirprm  21066  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisen  21090  lgsquadlem1  21091  lgsquadlem2  21092  m1lgs  21099  2sqlem11  21112  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  chebbnd1  21119  chtppilimlem1  21120  chtppilimlem2  21121  chtppilim  21122  chto1ub  21123  chebbnd2  21124  chto1lb  21125  chpchtlim  21126  chpo1ub  21127  chpo1ubb  21128  rplogsumlem1  21131  rplogsumlem2  21132  dchrisumlem2  21137  dchrisumlem3  21138  dchrvmasumiflem1  21148  dchrisum0fno1  21158  dchrisum0re  21160  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2  21165  rplogsum  21174  mulog2sumlem1  21181  mulog2sumlem2  21182  log2sumbnd  21191  selberglem2  21193  selbergb  21196  selberg2b  21199  chpdifbndlem1  21200  logdivbnd  21203  selberg3lem1  21204  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrmax  21211  pntrsumbnd2  21214  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntpbnd  21235  pntibndlem2  21238  pntibndlem3  21239  pntibnd  21240  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemr  21249  pntlemk  21253  pntlemo  21254  pnt2  21260  pnt  21261  ostth2lem1  21265  ostth3  21285  umgrafi  21310  usisuslgra  21340  usgraexvlem  21367  usgraex2elv  21370  usgraexmpldifpr  21372  wlkntrllem2  21513  constr3lem4  21587  constr3trllem3  21592  constr3pthlem1  21595  constr3pthlem3  21597  konigsberg  21662  ex-pss  21689  ex-res  21702  ex-fv  21704  ex-fl  21708  nvge0  22116  ipidsq  22162  minvecolem2  22330  minvecolem4  22335  normlem7  22571  norm-ii-i  22592  norm3lemt  22607  normpar2i  22611  bcsiALT  22634  pjhthlem1  22846  opsqrlem6  23601  cdj3lem1  23890  addltmulALT  23902  sqsscirc1  24259  rnlogblem  24352  dya2iocucvr  24587  coinfliplem  24689  coinflipspace  24691  ballotlem2  24699  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem6  24771  lgamucov  24775  subfacp1lem1  24818  subfacp1lem5  24823  subfacval3  24828  circum  25064  4bc2eq6  25157  axlowdimlem3  25787  axlowdimlem4  25788  axlowdimlem6  25790  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  mblfinlem  26143  itg2addnclem  26155  nn0prpwlem  26215  csbrn  26346  trirn  26347  isbnd2  26382  isbnd3  26383  heiborlem7  26416  rabren3dioph  26766  pellexlem2  26783  pellexlem5  26786  pell14qrgapw  26829  pellfundex  26839  rmspecsqrnq  26859  jm2.24nn  26914  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  acongrep  26935  acongeq  26938  jm2.22  26956  jm2.23  26957  jm2.20nn  26958  jm3.1lem2  26979  expdiophlem1  26982  matplusg  27337  lhe4.4ex1a  27414  stoweidlem13  27629  stoweidlem14  27630  stoweidlem26  27642  stoweidlem49  27665  stoweidlem52  27668  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem10  27699  stirlinglem11  27700  stirlinglem15  27704  stirlingr  27706  usgra2pthlem1  28040  vdgfrgragt2  28132  ene1  28245

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rrecex 9018  ax-cnre 9019

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-2 10014