Theorem 2re 9079

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

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

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 7992  ax-addrcl 7995

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

This theorem is referenced by:  2cn  9080  3re  9083  2ne0  9101  2ap0  9102  3pos  9103  2lt3  9180  1lt3  9181  2lt4  9183  1lt4  9184  2lt5  9187  2lt6  9192  1lt6  9193  2lt7  9198  1lt7  9199  2lt8  9205  1lt8  9206  2lt9  9213  1lt9  9214  1ap2  9217  1le2  9218  2rene0  9220  halfre  9223  halfgt0  9225  halflt1  9227  rehalfcl  9237  halfpos2  9240  halfnneg2  9242  addltmul  9247  nominpos  9248  avglt1  9249  avglt2  9250  div4p1lem1div2  9264  nn0lele2xi  9319  nn0ge2m1nn  9328  halfnz  9441  3halfnz  9442  2lt10  9613  1lt10  9614  eluz4eluz2  9660  uzuzle23  9664  uz3m2nn  9666  2rp  9752  xleaddadd  9981  fztpval  10177  fz0to4untppr  10218  fzo0to42pr  10315  qbtwnrelemcalc  10364  qbtwnre  10365  2tnp1ge0ge0  10410  flhalf  10411  fldiv4p1lem1div2  10414  mulp1mod1  10476  expubnd  10707  nn0opthlem2d  10832  faclbnd2  10853  4bc2eq6  10885  wrdlenge2n0  10989  cvg1nlemres  11169  resqrexlemover  11194  resqrexlemga  11207  sqrt4  11231  sqrt2gt1lt2  11233  abstri  11288  amgm2  11302  maxabslemlub  11391  maxltsup  11402  bdtrilem  11423  efcllemp  11842  efcllem  11843  ege2le3  11855  ef01bndlem  11940  cos01bnd  11942  cos2bnd  11944  cos01gt0  11947  sin02gt0  11948  sincos2sgn  11950  sin4lt0  11951  cos12dec  11952  eirraplem  11961  egt2lt3  11964  epos  11965  ene1  11969  eap1  11970  oexpneg  12061  oddge22np1  12065  evennn02n  12066  evennn2n  12067  nn0ehalf  12087  nno  12090  nn0o  12091  nn0oddm1d2  12093  nnoddm1d2  12094  flodddiv4t2lthalf  12123  bitsp1o  12137  bitsfzolem  12138  bitsfzo  12139  bitsfi  12141  6gcd4e2  12189  ncoprmgcdne1b  12284  prmdc  12325  3lcm2e6  12355  sqrt2irrlem  12356  sqrt2re  12358  sqrt2irraplemnn  12374  sqrt2irrap  12375  4sqlem11  12597  4sqlem12  12598  2expltfac  12635  plusgndxnmulrndx  12837  starvndxnplusgndx  12847  scandxnplusgndx  12859  vscandxnplusgndx  12864  ipndxnplusgndx  12877  tsetndxnplusgndx  12896  plendxnplusgndx  12910  dsndxnplusgndx  12925  slotsdifunifndx  12936  bl2in  14747  hoverb  14992  ivthdichlem  14995  reeff1o  15117  cosz12  15124  sin0pilem1  15125  sin0pilem2  15126  pilem3  15127  pipos  15132  sinhalfpilem  15135  sincosq1lem  15169  sincosq4sgn  15173  sinq12gt0  15174  cosq23lt0  15177  coseq00topi  15179  coseq0negpitopi  15180  tangtx  15182  sincos4thpi  15184  tan4thpi  15185  sincos6thpi  15186  cosordlem  15193  cosq34lt1  15194  cos02pilt1  15195  cos0pilt1  15196  2logb9irr  15315  2logb3irr  15317  2logb9irrALT  15318  sqrt2cxp2logb9e3  15319  2logb9irrap  15321  mersenne  15341  perfectlem1  15343  perfectlem2  15344  lgslem1  15349  lgsdirprm  15383  gausslemma2dlem0c  15400  gausslemma2dlem1a  15407  gausslemma2dlem2  15411  gausslemma2dlem3  15412  gausslemma2dlem4  15413  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  2lgslem1a1  15435  2lgslem1a2  15436  2lgslem1c  15439  2lgslem4  15452  ex-fl  15479  taupi  15830