Theorem 2re 8927

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 8916	. 2 ⊢ 2 = (1 + 1)
2		1re 7898	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 7912	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2239	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2136  (class class class)co 5842  ℝcr 7752  1c1 7754   + caddc 7756  2c2 8908

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 7847  ax-addrcl 7850

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

This theorem is referenced by:  2cn  8928  3re  8931  2ne0  8949  2ap0  8950  3pos  8951  2lt3  9027  1lt3  9028  2lt4  9030  1lt4  9031  2lt5  9034  2lt6  9039  1lt6  9040  2lt7  9045  1lt7  9046  2lt8  9052  1lt8  9053  2lt9  9060  1lt9  9061  1ap2  9064  1le2  9065  2rene0  9067  halfre  9070  halfgt0  9072  halflt1  9074  rehalfcl  9084  halfpos2  9087  halfnneg2  9089  addltmul  9093  nominpos  9094  avglt1  9095  avglt2  9096  div4p1lem1div2  9110  nn0lele2xi  9165  nn0ge2m1nn  9174  halfnz  9287  3halfnz  9288  2lt10  9459  1lt10  9460  eluz4eluz2  9505  uzuzle23  9509  uz3m2nn  9511  2rp  9594  xleaddadd  9823  fztpval  10018  fz0to4untppr  10059  fzo0to42pr  10155  qbtwnrelemcalc  10191  qbtwnre  10192  2tnp1ge0ge0  10236  flhalf  10237  fldiv4p1lem1div2  10240  mulp1mod1  10300  expubnd  10512  nn0opthlem2d  10634  faclbnd2  10655  4bc2eq6  10687  cvg1nlemres  10927  resqrexlemover  10952  resqrexlemga  10965  sqrt4  10989  sqrt2gt1lt2  10991  abstri  11046  amgm2  11060  maxabslemlub  11149  maxltsup  11160  bdtrilem  11180  efcllemp  11599  efcllem  11600  ege2le3  11612  ef01bndlem  11697  cos01bnd  11699  cos2bnd  11701  cos01gt0  11703  sin02gt0  11704  sincos2sgn  11706  sin4lt0  11707  cos12dec  11708  eirraplem  11717  egt2lt3  11720  epos  11721  ene1  11725  eap1  11726  oexpneg  11814  oddge22np1  11818  evennn02n  11819  evennn2n  11820  nn0ehalf  11840  nno  11843  nn0o  11844  nn0oddm1d2  11846  nnoddm1d2  11847  flodddiv4t2lthalf  11874  6gcd4e2  11928  ncoprmgcdne1b  12021  prmdc  12062  3lcm2e6  12092  sqrt2irrlem  12093  sqrt2re  12095  sqrt2irraplemnn  12111  sqrt2irrap  12112  plusgndxnmulrndx  12508  bl2in  13043  reeff1o  13334  cosz12  13341  sin0pilem1  13342  sin0pilem2  13343  pilem3  13344  pipos  13349  sinhalfpilem  13352  sincosq1lem  13386  sincosq4sgn  13390  sinq12gt0  13391  cosq23lt0  13394  coseq00topi  13396  coseq0negpitopi  13397  tangtx  13399  sincos4thpi  13401  tan4thpi  13402  sincos6thpi  13403  cosordlem  13410  cosq34lt1  13411  cos02pilt1  13412  cos0pilt1  13413  2logb9irr  13529  2logb3irr  13531  2logb9irrALT  13532  sqrt2cxp2logb9e3  13533  2logb9irrap  13535  lgslem1  13541  lgsdirprm  13575  ex-fl  13606  taupi  13949