Theorem 2re 9060

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

Syntax hints:   ∈ wcel 2167  (class class class)co 5922  ℝcr 7878  1c1 7880   + caddc 7882  2c2 9041

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 7973  ax-addrcl 7976

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

This theorem is referenced by:  2cn  9061  3re  9064  2ne0  9082  2ap0  9083  3pos  9084  2lt3  9161  1lt3  9162  2lt4  9164  1lt4  9165  2lt5  9168  2lt6  9173  1lt6  9174  2lt7  9179  1lt7  9180  2lt8  9186  1lt8  9187  2lt9  9194  1lt9  9195  1ap2  9198  1le2  9199  2rene0  9201  halfre  9204  halfgt0  9206  halflt1  9208  rehalfcl  9218  halfpos2  9221  halfnneg2  9223  addltmul  9228  nominpos  9229  avglt1  9230  avglt2  9231  div4p1lem1div2  9245  nn0lele2xi  9300  nn0ge2m1nn  9309  halfnz  9422  3halfnz  9423  2lt10  9594  1lt10  9595  eluz4eluz2  9641  uzuzle23  9645  uz3m2nn  9647  2rp  9733  xleaddadd  9962  fztpval  10158  fz0to4untppr  10199  fzo0to42pr  10296  qbtwnrelemcalc  10345  qbtwnre  10346  2tnp1ge0ge0  10391  flhalf  10392  fldiv4p1lem1div2  10395  mulp1mod1  10457  expubnd  10688  nn0opthlem2d  10813  faclbnd2  10834  4bc2eq6  10866  wrdlenge2n0  10970  cvg1nlemres  11150  resqrexlemover  11175  resqrexlemga  11188  sqrt4  11212  sqrt2gt1lt2  11214  abstri  11269  amgm2  11283  maxabslemlub  11372  maxltsup  11383  bdtrilem  11404  efcllemp  11823  efcllem  11824  ege2le3  11836  ef01bndlem  11921  cos01bnd  11923  cos2bnd  11925  cos01gt0  11928  sin02gt0  11929  sincos2sgn  11931  sin4lt0  11932  cos12dec  11933  eirraplem  11942  egt2lt3  11945  epos  11946  ene1  11950  eap1  11951  oexpneg  12042  oddge22np1  12046  evennn02n  12047  evennn2n  12048  nn0ehalf  12068  nno  12071  nn0o  12072  nn0oddm1d2  12074  nnoddm1d2  12075  flodddiv4t2lthalf  12104  bitsp1o  12117  bitsfzolem  12118  bitsfzo  12119  6gcd4e2  12162  ncoprmgcdne1b  12257  prmdc  12298  3lcm2e6  12328  sqrt2irrlem  12329  sqrt2re  12331  sqrt2irraplemnn  12347  sqrt2irrap  12348  4sqlem11  12570  4sqlem12  12571  2expltfac  12608  plusgndxnmulrndx  12810  starvndxnplusgndx  12820  scandxnplusgndx  12832  vscandxnplusgndx  12837  ipndxnplusgndx  12850  tsetndxnplusgndx  12869  plendxnplusgndx  12883  dsndxnplusgndx  12894  slotsdifunifndx  12905  bl2in  14639  hoverb  14884  ivthdichlem  14887  reeff1o  15009  cosz12  15016  sin0pilem1  15017  sin0pilem2  15018  pilem3  15019  pipos  15024  sinhalfpilem  15027  sincosq1lem  15061  sincosq4sgn  15065  sinq12gt0  15066  cosq23lt0  15069  coseq00topi  15071  coseq0negpitopi  15072  tangtx  15074  sincos4thpi  15076  tan4thpi  15077  sincos6thpi  15078  cosordlem  15085  cosq34lt1  15086  cos02pilt1  15087  cos0pilt1  15088  2logb9irr  15207  2logb3irr  15209  2logb9irrALT  15210  sqrt2cxp2logb9e3  15211  2logb9irrap  15213  mersenne  15233  perfectlem1  15235  perfectlem2  15236  lgslem1  15241  lgsdirprm  15275  gausslemma2dlem0c  15292  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  gausslemma2dlem3  15304  gausslemma2dlem4  15305  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem1a1  15327  2lgslem1a2  15328  2lgslem1c  15331  2lgslem4  15344  ex-fl  15371  taupi  15717