Theorem 2re 9077

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 9066	. 2 ⊢ 2 = (1 + 1)
2		1re 8042	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8056	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2269	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  ℝcr 7895  1c1 7897   + caddc 7899  2c2 9058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1re 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9066

This theorem is referenced by:  2cn  9078  3re  9081  2ne0  9099  2ap0  9100  3pos  9101  2lt3  9178  1lt3  9179  2lt4  9181  1lt4  9182  2lt5  9185  2lt6  9190  1lt6  9191  2lt7  9196  1lt7  9197  2lt8  9203  1lt8  9204  2lt9  9211  1lt9  9212  1ap2  9215  1le2  9216  2rene0  9218  halfre  9221  halfgt0  9223  halflt1  9225  rehalfcl  9235  halfpos2  9238  halfnneg2  9240  addltmul  9245  nominpos  9246  avglt1  9247  avglt2  9248  div4p1lem1div2  9262  nn0lele2xi  9317  nn0ge2m1nn  9326  halfnz  9439  3halfnz  9440  2lt10  9611  1lt10  9612  eluz4eluz2  9658  uzuzle23  9662  uz3m2nn  9664  2rp  9750  xleaddadd  9979  fztpval  10175  fz0to4untppr  10216  fzo0to42pr  10313  qbtwnrelemcalc  10362  qbtwnre  10363  2tnp1ge0ge0  10408  flhalf  10409  fldiv4p1lem1div2  10412  mulp1mod1  10474  expubnd  10705  nn0opthlem2d  10830  faclbnd2  10851  4bc2eq6  10883  wrdlenge2n0  10987  cvg1nlemres  11167  resqrexlemover  11192  resqrexlemga  11205  sqrt4  11229  sqrt2gt1lt2  11231  abstri  11286  amgm2  11300  maxabslemlub  11389  maxltsup  11400  bdtrilem  11421  efcllemp  11840  efcllem  11841  ege2le3  11853  ef01bndlem  11938  cos01bnd  11940  cos2bnd  11942  cos01gt0  11945  sin02gt0  11946  sincos2sgn  11948  sin4lt0  11949  cos12dec  11950  eirraplem  11959  egt2lt3  11962  epos  11963  ene1  11967  eap1  11968  oexpneg  12059  oddge22np1  12063  evennn02n  12064  evennn2n  12065  nn0ehalf  12085  nno  12088  nn0o  12089  nn0oddm1d2  12091  nnoddm1d2  12092  flodddiv4t2lthalf  12121  bitsp1o  12135  bitsfzolem  12136  bitsfzo  12137  bitsfi  12139  6gcd4e2  12187  ncoprmgcdne1b  12282  prmdc  12323  3lcm2e6  12353  sqrt2irrlem  12354  sqrt2re  12356  sqrt2irraplemnn  12372  sqrt2irrap  12373  4sqlem11  12595  4sqlem12  12596  2expltfac  12633  plusgndxnmulrndx  12835  starvndxnplusgndx  12845  scandxnplusgndx  12857  vscandxnplusgndx  12862  ipndxnplusgndx  12875  tsetndxnplusgndx  12894  plendxnplusgndx  12908  dsndxnplusgndx  12923  slotsdifunifndx  12934  bl2in  14723  hoverb  14968  ivthdichlem  14971  reeff1o  15093  cosz12  15100  sin0pilem1  15101  sin0pilem2  15102  pilem3  15103  pipos  15108  sinhalfpilem  15111  sincosq1lem  15145  sincosq4sgn  15149  sinq12gt0  15150  cosq23lt0  15153  coseq00topi  15155  coseq0negpitopi  15156  tangtx  15158  sincos4thpi  15160  tan4thpi  15161  sincos6thpi  15162  cosordlem  15169  cosq34lt1  15170  cos02pilt1  15171  cos0pilt1  15172  2logb9irr  15291  2logb3irr  15293  2logb9irrALT  15294  sqrt2cxp2logb9e3  15295  2logb9irrap  15297  mersenne  15317  perfectlem1  15319  perfectlem2  15320  lgslem1  15325  lgsdirprm  15359  gausslemma2dlem0c  15376  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  gausslemma2dlem3  15388  gausslemma2dlem4  15389  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem1a1  15411  2lgslem1a2  15412  2lgslem1c  15415  2lgslem4  15428  ex-fl  15455  taupi  15804