Theorem 2re 8790

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 8779	. 2 ⊢ 2 = (1 + 1)
2		1re 7765	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 7779	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2212	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 1480  (class class class)co 5774  ℝcr 7619  1c1 7621   + caddc 7623  2c2 8771

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1re 7714  ax-addrcl 7717

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-2 8779

This theorem is referenced by:  2cn  8791  3re  8794  2ne0  8812  2ap0  8813  3pos  8814  2lt3  8890  1lt3  8891  2lt4  8893  1lt4  8894  2lt5  8897  2lt6  8902  1lt6  8903  2lt7  8908  1lt7  8909  2lt8  8915  1lt8  8916  2lt9  8923  1lt9  8924  1ap2  8927  1le2  8928  2rene0  8930  halfre  8933  halfgt0  8935  halflt1  8937  rehalfcl  8947  halfpos2  8950  halfnneg2  8952  addltmul  8956  nominpos  8957  avglt1  8958  avglt2  8959  div4p1lem1div2  8973  nn0lele2xi  9028  nn0ge2m1nn  9037  halfnz  9147  3halfnz  9148  2lt10  9319  1lt10  9320  uzuzle23  9366  uz3m2nn  9368  2rp  9446  xleaddadd  9670  fztpval  9863  fzo0to42pr  9997  qbtwnrelemcalc  10033  qbtwnre  10034  2tnp1ge0ge0  10074  flhalf  10075  fldiv4p1lem1div2  10078  mulp1mod1  10138  expubnd  10350  nn0opthlem2d  10467  faclbnd2  10488  4bc2eq6  10520  cvg1nlemres  10757  resqrexlemover  10782  resqrexlemga  10795  sqrt4  10819  sqrt2gt1lt2  10821  abstri  10876  amgm2  10890  maxabslemlub  10979  maxltsup  10990  bdtrilem  11010  efcllemp  11364  efcllem  11365  ege2le3  11377  ef01bndlem  11463  cos01bnd  11465  cos2bnd  11467  cos01gt0  11469  sin02gt0  11470  sincos2sgn  11472  sin4lt0  11473  cos12dec  11474  eirraplem  11483  egt2lt3  11486  epos  11487  ene1  11491  eap1  11492  oexpneg  11574  oddge22np1  11578  evennn02n  11579  evennn2n  11580  nn0ehalf  11600  nno  11603  nn0o  11604  nn0oddm1d2  11606  nnoddm1d2  11607  flodddiv4t2lthalf  11634  6gcd4e2  11683  ncoprmgcdne1b  11770  3lcm2e6  11838  sqrt2irrlem  11839  sqrt2re  11841  sqrt2irraplemnn  11857  sqrt2irrap  11858  plusgndxnmulrndx  12072  bl2in  12572  cosz12  12861  sin0pilem1  12862  sin0pilem2  12863  pilem3  12864  pipos  12869  sinhalfpilem  12872  sincosq1lem  12906  sincosq4sgn  12910  sinq12gt0  12911  cosq23lt0  12914  coseq00topi  12916  coseq0negpitopi  12917  tangtx  12919  sincos4thpi  12921  tan4thpi  12922  sincos6thpi  12923  cosordlem  12930  cosq34lt1  12931  cos02pilt1  12932  ex-fl  12937  taupi  13239