Theorem 2re 8989

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 8978	. 2 |- 2 = ( 1 + 1 )
2		1re 7956	. . 3 |- 1 e. RR
3	2, 2	readdcli 7970	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2250	1 |- 2 e. RR

Syntax hints:   e. wcel 2148  (class class class)co 5875   RRcr 7810   1c1 7812   + caddc 7814   2c2 8970

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7905  ax-addrcl 7908

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8978

This theorem is referenced by:  2cn  8990  3re  8993  2ne0  9011  2ap0  9012  3pos  9013  2lt3  9089  1lt3  9090  2lt4  9092  1lt4  9093  2lt5  9096  2lt6  9101  1lt6  9102  2lt7  9107  1lt7  9108  2lt8  9114  1lt8  9115  2lt9  9122  1lt9  9123  1ap2  9126  1le2  9127  2rene0  9129  halfre  9132  halfgt0  9134  halflt1  9136  rehalfcl  9146  halfpos2  9149  halfnneg2  9151  addltmul  9155  nominpos  9156  avglt1  9157  avglt2  9158  div4p1lem1div2  9172  nn0lele2xi  9227  nn0ge2m1nn  9236  halfnz  9349  3halfnz  9350  2lt10  9521  1lt10  9522  eluz4eluz2  9567  uzuzle23  9571  uz3m2nn  9573  2rp  9658  xleaddadd  9887  fztpval  10083  fz0to4untppr  10124  fzo0to42pr  10220  qbtwnrelemcalc  10256  qbtwnre  10257  2tnp1ge0ge0  10301  flhalf  10302  fldiv4p1lem1div2  10305  mulp1mod1  10365  expubnd  10577  nn0opthlem2d  10701  faclbnd2  10722  4bc2eq6  10754  cvg1nlemres  10994  resqrexlemover  11019  resqrexlemga  11032  sqrt4  11056  sqrt2gt1lt2  11058  abstri  11113  amgm2  11127  maxabslemlub  11216  maxltsup  11227  bdtrilem  11247  efcllemp  11666  efcllem  11667  ege2le3  11679  ef01bndlem  11764  cos01bnd  11766  cos2bnd  11768  cos01gt0  11770  sin02gt0  11771  sincos2sgn  11773  sin4lt0  11774  cos12dec  11775  eirraplem  11784  egt2lt3  11787  epos  11788  ene1  11792  eap1  11793  oexpneg  11882  oddge22np1  11886  evennn02n  11887  evennn2n  11888  nn0ehalf  11908  nno  11911  nn0o  11912  nn0oddm1d2  11914  nnoddm1d2  11915  flodddiv4t2lthalf  11942  6gcd4e2  11996  ncoprmgcdne1b  12089  prmdc  12130  3lcm2e6  12160  sqrt2irrlem  12161  sqrt2re  12163  sqrt2irraplemnn  12179  sqrt2irrap  12180  plusgndxnmulrndx  12591  starvndxnplusgndx  12601  scandxnplusgndx  12613  vscandxnplusgndx  12618  ipndxnplusgndx  12631  tsetndxnplusgndx  12647  plendxnplusgndx  12661  dsndxnplusgndx  12672  slotsdifunifndx  12683  bl2in  13906  reeff1o  14197  cosz12  14204  sin0pilem1  14205  sin0pilem2  14206  pilem3  14207  pipos  14212  sinhalfpilem  14215  sincosq1lem  14249  sincosq4sgn  14253  sinq12gt0  14254  cosq23lt0  14257  coseq00topi  14259  coseq0negpitopi  14260  tangtx  14262  sincos4thpi  14264  tan4thpi  14265  sincos6thpi  14266  cosordlem  14273  cosq34lt1  14274  cos02pilt1  14275  cos0pilt1  14276  2logb9irr  14392  2logb3irr  14394  2logb9irrALT  14395  sqrt2cxp2logb9e3  14396  2logb9irrap  14398  lgslem1  14404  lgsdirprm  14438  lgseisenlem1  14453  lgseisenlem2  14454  ex-fl  14480  taupi  14823