Theorem 2re 8988

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

Syntax hints:   e. wcel 2148  (class class class)co 5874   RRcr 7809   1c1 7811   + caddc 7813   2c2 8969

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 7904  ax-addrcl 7907

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

This theorem is referenced by:  2cn  8989  3re  8992  2ne0  9010  2ap0  9011  3pos  9012  2lt3  9088  1lt3  9089  2lt4  9091  1lt4  9092  2lt5  9095  2lt6  9100  1lt6  9101  2lt7  9106  1lt7  9107  2lt8  9113  1lt8  9114  2lt9  9121  1lt9  9122  1ap2  9125  1le2  9126  2rene0  9128  halfre  9131  halfgt0  9133  halflt1  9135  rehalfcl  9145  halfpos2  9148  halfnneg2  9150  addltmul  9154  nominpos  9155  avglt1  9156  avglt2  9157  div4p1lem1div2  9171  nn0lele2xi  9226  nn0ge2m1nn  9235  halfnz  9348  3halfnz  9349  2lt10  9520  1lt10  9521  eluz4eluz2  9566  uzuzle23  9570  uz3m2nn  9572  2rp  9657  xleaddadd  9886  fztpval  10082  fz0to4untppr  10123  fzo0to42pr  10219  qbtwnrelemcalc  10255  qbtwnre  10256  2tnp1ge0ge0  10300  flhalf  10301  fldiv4p1lem1div2  10304  mulp1mod1  10364  expubnd  10576  nn0opthlem2d  10700  faclbnd2  10721  4bc2eq6  10753  cvg1nlemres  10993  resqrexlemover  11018  resqrexlemga  11031  sqrt4  11055  sqrt2gt1lt2  11057  abstri  11112  amgm2  11126  maxabslemlub  11215  maxltsup  11226  bdtrilem  11246  efcllemp  11665  efcllem  11666  ege2le3  11678  ef01bndlem  11763  cos01bnd  11765  cos2bnd  11767  cos01gt0  11769  sin02gt0  11770  sincos2sgn  11772  sin4lt0  11773  cos12dec  11774  eirraplem  11783  egt2lt3  11786  epos  11787  ene1  11791  eap1  11792  oexpneg  11881  oddge22np1  11885  evennn02n  11886  evennn2n  11887  nn0ehalf  11907  nno  11910  nn0o  11911  nn0oddm1d2  11913  nnoddm1d2  11914  flodddiv4t2lthalf  11941  6gcd4e2  11995  ncoprmgcdne1b  12088  prmdc  12129  3lcm2e6  12159  sqrt2irrlem  12160  sqrt2re  12162  sqrt2irraplemnn  12178  sqrt2irrap  12179  plusgndxnmulrndx  12590  starvndxnplusgndx  12600  scandxnplusgndx  12612  vscandxnplusgndx  12617  ipndxnplusgndx  12630  tsetndxnplusgndx  12646  plendxnplusgndx  12660  dsndxnplusgndx  12671  slotsdifunifndx  12682  bl2in  13873  reeff1o  14164  cosz12  14171  sin0pilem1  14172  sin0pilem2  14173  pilem3  14174  pipos  14179  sinhalfpilem  14182  sincosq1lem  14216  sincosq4sgn  14220  sinq12gt0  14221  cosq23lt0  14224  coseq00topi  14226  coseq0negpitopi  14227  tangtx  14229  sincos4thpi  14231  tan4thpi  14232  sincos6thpi  14233  cosordlem  14240  cosq34lt1  14241  cos02pilt1  14242  cos0pilt1  14243  2logb9irr  14359  2logb3irr  14361  2logb9irrALT  14362  sqrt2cxp2logb9e3  14363  2logb9irrap  14365  lgslem1  14371  lgsdirprm  14405  lgseisenlem1  14420  lgseisenlem2  14421  ex-fl  14447  taupi  14790