Theorem 2re 8694

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 8683	. 2 ⊢ 2 = (1 + 1)
2		1re 7683	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 7697	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2185	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 1461  (class class class)co 5726  ℝcr 7540  1c1 7542   + caddc 7544  2c2 8675

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095  ax-1re 7633  ax-addrcl 7636

This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-clel 2109  df-2 8683

This theorem is referenced by:  2cn  8695  3re  8698  2ne0  8716  2ap0  8717  3pos  8718  2lt3  8788  1lt3  8789  2lt4  8791  1lt4  8792  2lt5  8795  2lt6  8800  1lt6  8801  2lt7  8806  1lt7  8807  2lt8  8813  1lt8  8814  2lt9  8821  1lt9  8822  1ap2  8825  1le2  8826  2rene0  8828  halfre  8831  halfgt0  8833  halflt1  8835  rehalfcl  8845  halfpos2  8848  halfnneg2  8850  addltmul  8854  nominpos  8855  avglt1  8856  avglt2  8857  div4p1lem1div2  8871  nn0lele2xi  8926  nn0ge2m1nn  8935  halfnz  9045  3halfnz  9046  2lt10  9217  1lt10  9218  uzuzle23  9262  uz3m2nn  9264  2rp  9342  xleaddadd  9557  fztpval  9750  fzo0to42pr  9884  qbtwnrelemcalc  9920  qbtwnre  9921  2tnp1ge0ge0  9961  flhalf  9962  fldiv4p1lem1div2  9965  mulp1mod1  10025  expubnd  10237  nn0opthlem2d  10354  faclbnd2  10375  4bc2eq6  10407  cvg1nlemres  10643  resqrexlemover  10668  resqrexlemga  10681  sqrt4  10705  sqrt2gt1lt2  10707  abstri  10762  amgm2  10776  maxabslemlub  10865  maxltsup  10876  bdtrilem  10896  efcllemp  11209  efcllem  11210  ege2le3  11222  ef01bndlem  11308  cos01bnd  11310  cos2bnd  11312  cos01gt0  11314  sin02gt0  11315  sincos2sgn  11317  sin4lt0  11318  eirraplem  11325  egt2lt3  11328  epos  11329  ene1  11333  eap1  11334  oexpneg  11416  oddge22np1  11420  evennn02n  11421  evennn2n  11422  nn0ehalf  11442  nno  11445  nn0o  11446  nn0oddm1d2  11448  nnoddm1d2  11449  flodddiv4t2lthalf  11476  6gcd4e2  11523  ncoprmgcdne1b  11610  3lcm2e6  11678  sqrt2irrlem  11679  sqrt2re  11681  sqrt2irraplemnn  11696  sqrt2irrap  11697  plusgndxnmulrndx  11909  bl2in  12386  ex-fl  12621