Theorem 2re 8783

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 8772	. 2 ⊢ 2 = (1 + 1)
2		1re 7758	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 7772	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2210	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 1480  (class class class)co 5767  ℝcr 7612  1c1 7614   + caddc 7616  2c2 8764

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 2119  ax-1re 7707  ax-addrcl 7710

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133  df-2 8772

This theorem is referenced by:  2cn  8784  3re  8787  2ne0  8805  2ap0  8806  3pos  8807  2lt3  8883  1lt3  8884  2lt4  8886  1lt4  8887  2lt5  8890  2lt6  8895  1lt6  8896  2lt7  8901  1lt7  8902  2lt8  8908  1lt8  8909  2lt9  8916  1lt9  8917  1ap2  8920  1le2  8921  2rene0  8923  halfre  8926  halfgt0  8928  halflt1  8930  rehalfcl  8940  halfpos2  8943  halfnneg2  8945  addltmul  8949  nominpos  8950  avglt1  8951  avglt2  8952  div4p1lem1div2  8966  nn0lele2xi  9021  nn0ge2m1nn  9030  halfnz  9140  3halfnz  9141  2lt10  9312  1lt10  9313  uzuzle23  9359  uz3m2nn  9361  2rp  9439  xleaddadd  9663  fztpval  9856  fzo0to42pr  9990  qbtwnrelemcalc  10026  qbtwnre  10027  2tnp1ge0ge0  10067  flhalf  10068  fldiv4p1lem1div2  10071  mulp1mod1  10131  expubnd  10343  nn0opthlem2d  10460  faclbnd2  10481  4bc2eq6  10513  cvg1nlemres  10750  resqrexlemover  10775  resqrexlemga  10788  sqrt4  10812  sqrt2gt1lt2  10814  abstri  10869  amgm2  10883  maxabslemlub  10972  maxltsup  10983  bdtrilem  11003  efcllemp  11353  efcllem  11354  ege2le3  11366  ef01bndlem  11452  cos01bnd  11454  cos2bnd  11456  cos01gt0  11458  sin02gt0  11459  sincos2sgn  11461  sin4lt0  11462  cos12dec  11463  eirraplem  11472  egt2lt3  11475  epos  11476  ene1  11480  eap1  11481  oexpneg  11563  oddge22np1  11567  evennn02n  11568  evennn2n  11569  nn0ehalf  11589  nno  11592  nn0o  11593  nn0oddm1d2  11595  nnoddm1d2  11596  flodddiv4t2lthalf  11623  6gcd4e2  11672  ncoprmgcdne1b  11759  3lcm2e6  11827  sqrt2irrlem  11828  sqrt2re  11830  sqrt2irraplemnn  11846  sqrt2irrap  11847  plusgndxnmulrndx  12061  bl2in  12561  cosz12  12850  sin0pilem1  12851  sin0pilem2  12852  pilem3  12853  pipos  12858  sinhalfpilem  12861  sincosq1lem  12895  sincosq4sgn  12899  sinq12gt0  12900  cosq23lt0  12903  coseq00topi  12905  coseq0negpitopi  12906  tangtx  12908  sincos4thpi  12910  tan4thpi  12911  sincos6thpi  12912  cosordlem  12919  cosq34lt1  12920  cos02pilt1  12921  ex-fl  12926  taupi  13228