Theorem 2re 8918

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 8907	. 2 ⊢ 2 = (1 + 1)
2		1re 7889	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 7903	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2237	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2135  (class class class)co 5836  ℝcr 7743  1c1 7745   + caddc 7747  2c2 8899

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146  ax-1re 7838  ax-addrcl 7841

This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160  df-2 8907

This theorem is referenced by:  2cn  8919  3re  8922  2ne0  8940  2ap0  8941  3pos  8942  2lt3  9018  1lt3  9019  2lt4  9021  1lt4  9022  2lt5  9025  2lt6  9030  1lt6  9031  2lt7  9036  1lt7  9037  2lt8  9043  1lt8  9044  2lt9  9051  1lt9  9052  1ap2  9055  1le2  9056  2rene0  9058  halfre  9061  halfgt0  9063  halflt1  9065  rehalfcl  9075  halfpos2  9078  halfnneg2  9080  addltmul  9084  nominpos  9085  avglt1  9086  avglt2  9087  div4p1lem1div2  9101  nn0lele2xi  9156  nn0ge2m1nn  9165  halfnz  9278  3halfnz  9279  2lt10  9450  1lt10  9451  eluz4eluz2  9496  uzuzle23  9500  uz3m2nn  9502  2rp  9585  xleaddadd  9814  fztpval  10008  fz0to4untppr  10049  fzo0to42pr  10145  qbtwnrelemcalc  10181  qbtwnre  10182  2tnp1ge0ge0  10226  flhalf  10227  fldiv4p1lem1div2  10230  mulp1mod1  10290  expubnd  10502  nn0opthlem2d  10623  faclbnd2  10644  4bc2eq6  10676  cvg1nlemres  10913  resqrexlemover  10938  resqrexlemga  10951  sqrt4  10975  sqrt2gt1lt2  10977  abstri  11032  amgm2  11046  maxabslemlub  11135  maxltsup  11146  bdtrilem  11166  efcllemp  11585  efcllem  11586  ege2le3  11598  ef01bndlem  11683  cos01bnd  11685  cos2bnd  11687  cos01gt0  11689  sin02gt0  11690  sincos2sgn  11692  sin4lt0  11693  cos12dec  11694  eirraplem  11703  egt2lt3  11706  epos  11707  ene1  11711  eap1  11712  oexpneg  11799  oddge22np1  11803  evennn02n  11804  evennn2n  11805  nn0ehalf  11825  nno  11828  nn0o  11829  nn0oddm1d2  11831  nnoddm1d2  11832  flodddiv4t2lthalf  11859  6gcd4e2  11913  ncoprmgcdne1b  12000  prmdc  12041  3lcm2e6  12069  sqrt2irrlem  12070  sqrt2re  12072  sqrt2irraplemnn  12088  sqrt2irrap  12089  plusgndxnmulrndx  12444  bl2in  12944  reeff1o  13235  cosz12  13242  sin0pilem1  13243  sin0pilem2  13244  pilem3  13245  pipos  13250  sinhalfpilem  13253  sincosq1lem  13287  sincosq4sgn  13291  sinq12gt0  13292  cosq23lt0  13295  coseq00topi  13297  coseq0negpitopi  13298  tangtx  13300  sincos4thpi  13302  tan4thpi  13303  sincos6thpi  13304  cosordlem  13311  cosq34lt1  13312  cos02pilt1  13313  cos0pilt1  13314  2logb9irr  13430  2logb3irr  13432  2logb9irrALT  13433  sqrt2cxp2logb9e3  13434  2logb9irrap  13436  ex-fl  13443  taupi  13783