Theorem 2re 8948

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 8937	. 2 |- 2 = ( 1 + 1 )
2		1re 7919	. . 3 |- 1 e. RR
3	2, 2	readdcli 7933	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2243	1 |- 2 e. RR

Syntax hints:   e. wcel 2141  (class class class)co 5853   RRcr 7773   1c1 7775   + caddc 7777   2c2 8929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-2 8937

This theorem is referenced by:  2cn  8949  3re  8952  2ne0  8970  2ap0  8971  3pos  8972  2lt3  9048  1lt3  9049  2lt4  9051  1lt4  9052  2lt5  9055  2lt6  9060  1lt6  9061  2lt7  9066  1lt7  9067  2lt8  9073  1lt8  9074  2lt9  9081  1lt9  9082  1ap2  9085  1le2  9086  2rene0  9088  halfre  9091  halfgt0  9093  halflt1  9095  rehalfcl  9105  halfpos2  9108  halfnneg2  9110  addltmul  9114  nominpos  9115  avglt1  9116  avglt2  9117  div4p1lem1div2  9131  nn0lele2xi  9186  nn0ge2m1nn  9195  halfnz  9308  3halfnz  9309  2lt10  9480  1lt10  9481  eluz4eluz2  9526  uzuzle23  9530  uz3m2nn  9532  2rp  9615  xleaddadd  9844  fztpval  10039  fz0to4untppr  10080  fzo0to42pr  10176  qbtwnrelemcalc  10212  qbtwnre  10213  2tnp1ge0ge0  10257  flhalf  10258  fldiv4p1lem1div2  10261  mulp1mod1  10321  expubnd  10533  nn0opthlem2d  10655  faclbnd2  10676  4bc2eq6  10708  cvg1nlemres  10949  resqrexlemover  10974  resqrexlemga  10987  sqrt4  11011  sqrt2gt1lt2  11013  abstri  11068  amgm2  11082  maxabslemlub  11171  maxltsup  11182  bdtrilem  11202  efcllemp  11621  efcllem  11622  ege2le3  11634  ef01bndlem  11719  cos01bnd  11721  cos2bnd  11723  cos01gt0  11725  sin02gt0  11726  sincos2sgn  11728  sin4lt0  11729  cos12dec  11730  eirraplem  11739  egt2lt3  11742  epos  11743  ene1  11747  eap1  11748  oexpneg  11836  oddge22np1  11840  evennn02n  11841  evennn2n  11842  nn0ehalf  11862  nno  11865  nn0o  11866  nn0oddm1d2  11868  nnoddm1d2  11869  flodddiv4t2lthalf  11896  6gcd4e2  11950  ncoprmgcdne1b  12043  prmdc  12084  3lcm2e6  12114  sqrt2irrlem  12115  sqrt2re  12117  sqrt2irraplemnn  12133  sqrt2irrap  12134  plusgndxnmulrndx  12531  bl2in  13197  reeff1o  13488  cosz12  13495  sin0pilem1  13496  sin0pilem2  13497  pilem3  13498  pipos  13503  sinhalfpilem  13506  sincosq1lem  13540  sincosq4sgn  13544  sinq12gt0  13545  cosq23lt0  13548  coseq00topi  13550  coseq0negpitopi  13551  tangtx  13553  sincos4thpi  13555  tan4thpi  13556  sincos6thpi  13557  cosordlem  13564  cosq34lt1  13565  cos02pilt1  13566  cos0pilt1  13567  2logb9irr  13683  2logb3irr  13685  2logb9irrALT  13686  sqrt2cxp2logb9e3  13687  2logb9irrap  13689  lgslem1  13695  lgsdirprm  13729  ex-fl  13760  taupi  14102