Theorem 2re 9206

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 9195	. 2 |- 2 = ( 1 + 1 )
2		1re 8171	. . 3 |- 1 e. RR
3	2, 2	readdcli 8185	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2302	1 |- 2 e. RR

Syntax hints:   e. wcel 2200  (class class class)co 6013   RRcr 8024   1c1 8026   + caddc 8028   2c2 9187

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8119  ax-addrcl 8122

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9195

This theorem is referenced by:  2cn  9207  3re  9210  2ne0  9228  2ap0  9229  3pos  9230  2lt3  9307  1lt3  9308  2lt4  9310  1lt4  9311  2lt5  9314  2lt6  9319  1lt6  9320  2lt7  9325  1lt7  9326  2lt8  9332  1lt8  9333  2lt9  9340  1lt9  9341  1ap2  9344  1le2  9345  2rene0  9347  halfre  9350  halfgt0  9352  halflt1  9354  rehalfcl  9364  halfpos2  9367  halfnneg2  9369  addltmul  9374  nominpos  9375  avglt1  9376  avglt2  9377  div4p1lem1div2  9391  nn0lele2xi  9446  nn0ge2m1nn  9455  halfnz  9569  3halfnz  9570  2lt10  9741  1lt10  9742  uzuzle23  9789  uzuzle24  9790  eluz4eluz2  9795  uz3m2nn  9800  2rp  9886  xleaddadd  10115  fztpval  10311  fz0to4untppr  10352  fzo0to42pr  10458  qbtwnrelemcalc  10508  qbtwnre  10509  2tnp1ge0ge0  10554  flhalf  10555  fldiv4p1lem1div2  10558  mulp1mod1  10620  expubnd  10851  nn0opthlem2d  10976  faclbnd2  10997  4bc2eq6  11029  wrdlenge2n0  11142  cvg1nlemres  11539  resqrexlemover  11564  resqrexlemga  11577  sqrt4  11601  sqrt2gt1lt2  11603  abstri  11658  amgm2  11672  maxabslemlub  11761  maxltsup  11772  bdtrilem  11793  efcllemp  12212  efcllem  12213  ege2le3  12225  ef01bndlem  12310  cos01bnd  12312  cos2bnd  12314  cos01gt0  12317  sin02gt0  12318  sincos2sgn  12320  sin4lt0  12321  cos12dec  12322  eirraplem  12331  egt2lt3  12334  epos  12335  ene1  12339  eap1  12340  oexpneg  12431  oddge22np1  12435  evennn02n  12436  evennn2n  12437  nn0ehalf  12457  nno  12460  nn0o  12461  nn0oddm1d2  12463  nnoddm1d2  12464  flodddiv4t2lthalf  12493  bitsp1o  12507  bitsfzolem  12508  bitsfzo  12509  bitsfi  12511  6gcd4e2  12559  ncoprmgcdne1b  12654  prmdc  12695  3lcm2e6  12725  sqrt2irrlem  12726  sqrt2re  12728  sqrt2irraplemnn  12744  sqrt2irrap  12745  4sqlem11  12967  4sqlem12  12968  2expltfac  13005  plusgndxnmulrndx  13209  starvndxnplusgndx  13219  scandxnplusgndx  13231  vscandxnplusgndx  13236  ipndxnplusgndx  13249  tsetndxnplusgndx  13268  plendxnplusgndx  13282  dsndxnplusgndx  13297  slotsdifunifndx  13308  bl2in  15120  hoverb  15365  ivthdichlem  15368  reeff1o  15490  cosz12  15497  sin0pilem1  15498  sin0pilem2  15499  pilem3  15500  pipos  15505  sinhalfpilem  15508  sincosq1lem  15542  sincosq4sgn  15546  sinq12gt0  15547  cosq23lt0  15550  coseq00topi  15552  coseq0negpitopi  15553  tangtx  15555  sincos4thpi  15557  tan4thpi  15558  sincos6thpi  15559  cosordlem  15566  cosq34lt1  15567  cos02pilt1  15568  cos0pilt1  15569  2logb9irr  15688  2logb3irr  15690  2logb9irrALT  15691  sqrt2cxp2logb9e3  15692  2logb9irrap  15694  mersenne  15714  perfectlem1  15716  perfectlem2  15717  lgslem1  15722  lgsdirprm  15756  gausslemma2dlem0c  15773  gausslemma2dlem1a  15780  gausslemma2dlem2  15784  gausslemma2dlem3  15785  gausslemma2dlem4  15786  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgseisen  15796  lgsquadlem1  15799  lgsquadlem2  15800  2lgslem1a1  15808  2lgslem1a2  15809  2lgslem1c  15812  2lgslem4  15825  usgrexmpldifpr  16093  clwwlkext2edg  16231  ex-fl  16271  taupi  16627