Theorem 2re 8109

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 8098	. 2 ⊢ 2 = (1 + 1)
2		1re 7118	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 7132	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2151	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 1433  (class class class)co 5532  ℝcr 6980  1c1 6982   + caddc 6984  2c2 8089

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077  df-2 8098

This theorem is referenced by:  2cn  8110  3re  8113  2ne0  8131  2ap0  8132  3pos  8133  2lt3  8202  1lt3  8203  2lt4  8205  1lt4  8206  2lt5  8209  2lt6  8214  1lt6  8215  2lt7  8220  1lt7  8221  2lt8  8227  1lt8  8228  2lt9  8235  1lt9  8236  1le2  8239  2rene0  8241  halfre  8244  halfgt0  8246  halflt1  8248  rehalfcl  8258  halfpos2  8261  halfnneg2  8263  addltmul  8267  nominpos  8268  avglt1  8269  avglt2  8270  div4p1lem1div2  8284  nn0lele2xi  8339  nn0ge2m1nn  8348  halfnz  8443  3halfnz  8444  2lt10  8614  1lt10  8615  uzuzle23  8659  uz3m2nn  8661  2rp  8739  fztpval  9100  fzo0to42pr  9229  qbtwnrelemcalc  9264  qbtwnre  9265  2tnp1ge0ge0  9303  flhalf  9304  fldiv4p1lem1div2  9307  mulp1mod1  9367  expubnd  9533  nn0opthlem2d  9648  faclbnd2  9669  4bc2eq6  9701  cvg1nlemres  9871  resqrexlemover  9896  resqrexlemga  9909  sqrt4  9933  sqrt2gt1lt2  9935  abstri  9990  amgm2  10004  maxabslemlub  10093  maxltsup  10104  oexpneg  10276  oddge22np1  10281  evennn02n  10282  evennn2n  10283  nn0ehalf  10303  nno  10306  nn0o  10307  nn0oddm1d2  10309  nnoddm1d2  10310  flodddiv4t2lthalf  10337  6gcd4e2  10384  ncoprmgcdne1b  10471  3lcm2e6  10539  sqrt2irrlem  10540  sqrt2re  10542  sqrt2irraplemnn  10557  sqrt2irrap  10558  ex-fl  10563