Theorem 2re 9054

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 9043	. 2 ⊢ 2 = (1 + 1)
2		1re 8020	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8034	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2266	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2164  (class class class)co 5919  ℝcr 7873  1c1 7875   + caddc 7877  2c2 9035

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189  df-2 9043

This theorem is referenced by:  2cn  9055  3re  9058  2ne0  9076  2ap0  9077  3pos  9078  2lt3  9155  1lt3  9156  2lt4  9158  1lt4  9159  2lt5  9162  2lt6  9167  1lt6  9168  2lt7  9173  1lt7  9174  2lt8  9180  1lt8  9181  2lt9  9188  1lt9  9189  1ap2  9192  1le2  9193  2rene0  9195  halfre  9198  halfgt0  9200  halflt1  9202  rehalfcl  9212  halfpos2  9215  halfnneg2  9217  addltmul  9222  nominpos  9223  avglt1  9224  avglt2  9225  div4p1lem1div2  9239  nn0lele2xi  9294  nn0ge2m1nn  9303  halfnz  9416  3halfnz  9417  2lt10  9588  1lt10  9589  eluz4eluz2  9635  uzuzle23  9639  uz3m2nn  9641  2rp  9727  xleaddadd  9956  fztpval  10152  fz0to4untppr  10193  fzo0to42pr  10290  qbtwnrelemcalc  10327  qbtwnre  10328  2tnp1ge0ge0  10373  flhalf  10374  fldiv4p1lem1div2  10377  mulp1mod1  10439  expubnd  10670  nn0opthlem2d  10795  faclbnd2  10816  4bc2eq6  10848  wrdlenge2n0  10952  cvg1nlemres  11132  resqrexlemover  11157  resqrexlemga  11170  sqrt4  11194  sqrt2gt1lt2  11196  abstri  11251  amgm2  11265  maxabslemlub  11354  maxltsup  11365  bdtrilem  11385  efcllemp  11804  efcllem  11805  ege2le3  11817  ef01bndlem  11902  cos01bnd  11904  cos2bnd  11906  cos01gt0  11909  sin02gt0  11910  sincos2sgn  11912  sin4lt0  11913  cos12dec  11914  eirraplem  11923  egt2lt3  11926  epos  11927  ene1  11931  eap1  11932  oexpneg  12021  oddge22np1  12025  evennn02n  12026  evennn2n  12027  nn0ehalf  12047  nno  12050  nn0o  12051  nn0oddm1d2  12053  nnoddm1d2  12054  flodddiv4t2lthalf  12081  6gcd4e2  12135  ncoprmgcdne1b  12230  prmdc  12271  3lcm2e6  12301  sqrt2irrlem  12302  sqrt2re  12304  sqrt2irraplemnn  12320  sqrt2irrap  12321  4sqlem11  12542  4sqlem12  12543  plusgndxnmulrndx  12753  starvndxnplusgndx  12763  scandxnplusgndx  12775  vscandxnplusgndx  12780  ipndxnplusgndx  12793  tsetndxnplusgndx  12812  plendxnplusgndx  12826  dsndxnplusgndx  12837  slotsdifunifndx  12848  bl2in  14582  hoverb  14827  ivthdichlem  14830  reeff1o  14949  cosz12  14956  sin0pilem1  14957  sin0pilem2  14958  pilem3  14959  pipos  14964  sinhalfpilem  14967  sincosq1lem  15001  sincosq4sgn  15005  sinq12gt0  15006  cosq23lt0  15009  coseq00topi  15011  coseq0negpitopi  15012  tangtx  15014  sincos4thpi  15016  tan4thpi  15017  sincos6thpi  15018  cosordlem  15025  cosq34lt1  15026  cos02pilt1  15027  cos0pilt1  15028  2logb9irr  15144  2logb3irr  15146  2logb9irrALT  15147  sqrt2cxp2logb9e3  15148  2logb9irrap  15150  lgslem1  15157  lgsdirprm  15191  gausslemma2dlem0c  15208  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem3  15220  gausslemma2dlem4  15221  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1a1  15243  2lgslem1a2  15244  2lgslem1c  15247  2lgslem4  15260  ex-fl  15287  taupi  15633