Theorem 2re 9052

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 9041	. 2 |- 2 = ( 1 + 1 )
2		1re 8018	. . 3 |- 1 e. RR
3	2, 2	readdcli 8032	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2266	1 |- 2 e. RR

Syntax hints:   e. wcel 2164  (class class class)co 5918   RRcr 7871   1c1 7873   + caddc 7875   2c2 9033

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 7966  ax-addrcl 7969

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

This theorem is referenced by:  2cn  9053  3re  9056  2ne0  9074  2ap0  9075  3pos  9076  2lt3  9152  1lt3  9153  2lt4  9155  1lt4  9156  2lt5  9159  2lt6  9164  1lt6  9165  2lt7  9170  1lt7  9171  2lt8  9177  1lt8  9178  2lt9  9185  1lt9  9186  1ap2  9189  1le2  9190  2rene0  9192  halfre  9195  halfgt0  9197  halflt1  9199  rehalfcl  9209  halfpos2  9212  halfnneg2  9214  addltmul  9219  nominpos  9220  avglt1  9221  avglt2  9222  div4p1lem1div2  9236  nn0lele2xi  9291  nn0ge2m1nn  9300  halfnz  9413  3halfnz  9414  2lt10  9585  1lt10  9586  eluz4eluz2  9632  uzuzle23  9636  uz3m2nn  9638  2rp  9724  xleaddadd  9953  fztpval  10149  fz0to4untppr  10190  fzo0to42pr  10287  qbtwnrelemcalc  10324  qbtwnre  10325  2tnp1ge0ge0  10370  flhalf  10371  fldiv4p1lem1div2  10374  mulp1mod1  10436  expubnd  10667  nn0opthlem2d  10792  faclbnd2  10813  4bc2eq6  10845  wrdlenge2n0  10949  cvg1nlemres  11129  resqrexlemover  11154  resqrexlemga  11167  sqrt4  11191  sqrt2gt1lt2  11193  abstri  11248  amgm2  11262  maxabslemlub  11351  maxltsup  11362  bdtrilem  11382  efcllemp  11801  efcllem  11802  ege2le3  11814  ef01bndlem  11899  cos01bnd  11901  cos2bnd  11903  cos01gt0  11906  sin02gt0  11907  sincos2sgn  11909  sin4lt0  11910  cos12dec  11911  eirraplem  11920  egt2lt3  11923  epos  11924  ene1  11928  eap1  11929  oexpneg  12018  oddge22np1  12022  evennn02n  12023  evennn2n  12024  nn0ehalf  12044  nno  12047  nn0o  12048  nn0oddm1d2  12050  nnoddm1d2  12051  flodddiv4t2lthalf  12078  6gcd4e2  12132  ncoprmgcdne1b  12227  prmdc  12268  3lcm2e6  12298  sqrt2irrlem  12299  sqrt2re  12301  sqrt2irraplemnn  12317  sqrt2irrap  12318  4sqlem11  12539  4sqlem12  12540  plusgndxnmulrndx  12750  starvndxnplusgndx  12760  scandxnplusgndx  12772  vscandxnplusgndx  12777  ipndxnplusgndx  12790  tsetndxnplusgndx  12809  plendxnplusgndx  12823  dsndxnplusgndx  12834  slotsdifunifndx  12845  bl2in  14571  hoverb  14802  ivthdichlem  14805  reeff1o  14908  cosz12  14915  sin0pilem1  14916  sin0pilem2  14917  pilem3  14918  pipos  14923  sinhalfpilem  14926  sincosq1lem  14960  sincosq4sgn  14964  sinq12gt0  14965  cosq23lt0  14968  coseq00topi  14970  coseq0negpitopi  14971  tangtx  14973  sincos4thpi  14975  tan4thpi  14976  sincos6thpi  14977  cosordlem  14984  cosq34lt1  14985  cos02pilt1  14986  cos0pilt1  14987  2logb9irr  15103  2logb3irr  15105  2logb9irrALT  15106  sqrt2cxp2logb9e3  15107  2logb9irrap  15109  lgslem1  15116  lgsdirprm  15150  gausslemma2dlem0c  15167  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem3  15179  gausslemma2dlem4  15180  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisen  15190  lgsquadlem1  15191  ex-fl  15217  taupi  15563