Theorem 2re 8923

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 8912	. 2 |- 2 = ( 1 + 1 )
2		1re 7894	. . 3 |- 1 e. RR
3	2, 2	readdcli 7908	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2238	1 |- 2 e. RR

Syntax hints:   e. wcel 2136  (class class class)co 5841   RRcr 7748   1c1 7750   + caddc 7752   2c2 8904

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1re 7843  ax-addrcl 7846

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-2 8912

This theorem is referenced by:  2cn  8924  3re  8927  2ne0  8945  2ap0  8946  3pos  8947  2lt3  9023  1lt3  9024  2lt4  9026  1lt4  9027  2lt5  9030  2lt6  9035  1lt6  9036  2lt7  9041  1lt7  9042  2lt8  9048  1lt8  9049  2lt9  9056  1lt9  9057  1ap2  9060  1le2  9061  2rene0  9063  halfre  9066  halfgt0  9068  halflt1  9070  rehalfcl  9080  halfpos2  9083  halfnneg2  9085  addltmul  9089  nominpos  9090  avglt1  9091  avglt2  9092  div4p1lem1div2  9106  nn0lele2xi  9161  nn0ge2m1nn  9170  halfnz  9283  3halfnz  9284  2lt10  9455  1lt10  9456  eluz4eluz2  9501  uzuzle23  9505  uz3m2nn  9507  2rp  9590  xleaddadd  9819  fztpval  10014  fz0to4untppr  10055  fzo0to42pr  10151  qbtwnrelemcalc  10187  qbtwnre  10188  2tnp1ge0ge0  10232  flhalf  10233  fldiv4p1lem1div2  10236  mulp1mod1  10296  expubnd  10508  nn0opthlem2d  10630  faclbnd2  10651  4bc2eq6  10683  cvg1nlemres  10923  resqrexlemover  10948  resqrexlemga  10961  sqrt4  10985  sqrt2gt1lt2  10987  abstri  11042  amgm2  11056  maxabslemlub  11145  maxltsup  11156  bdtrilem  11176  efcllemp  11595  efcllem  11596  ege2le3  11608  ef01bndlem  11693  cos01bnd  11695  cos2bnd  11697  cos01gt0  11699  sin02gt0  11700  sincos2sgn  11702  sin4lt0  11703  cos12dec  11704  eirraplem  11713  egt2lt3  11716  epos  11717  ene1  11721  eap1  11722  oexpneg  11810  oddge22np1  11814  evennn02n  11815  evennn2n  11816  nn0ehalf  11836  nno  11839  nn0o  11840  nn0oddm1d2  11842  nnoddm1d2  11843  flodddiv4t2lthalf  11870  6gcd4e2  11924  ncoprmgcdne1b  12017  prmdc  12058  3lcm2e6  12088  sqrt2irrlem  12089  sqrt2re  12091  sqrt2irraplemnn  12107  sqrt2irrap  12108  plusgndxnmulrndx  12503  bl2in  13003  reeff1o  13294  cosz12  13301  sin0pilem1  13302  sin0pilem2  13303  pilem3  13304  pipos  13309  sinhalfpilem  13312  sincosq1lem  13346  sincosq4sgn  13350  sinq12gt0  13351  cosq23lt0  13354  coseq00topi  13356  coseq0negpitopi  13357  tangtx  13359  sincos4thpi  13361  tan4thpi  13362  sincos6thpi  13363  cosordlem  13370  cosq34lt1  13371  cos02pilt1  13372  cos0pilt1  13373  2logb9irr  13489  2logb3irr  13491  2logb9irrALT  13492  sqrt2cxp2logb9e3  13493  2logb9irrap  13495  lgslem1  13501  lgsdirprm  13535  ex-fl  13566  taupi  13909