Theorem 2re 9106

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 9095	. 2 |- 2 = ( 1 + 1 )
2		1re 8071	. . 3 |- 1 e. RR
3	2, 2	readdcli 8085	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2278	1 |- 2 e. RR

Syntax hints:   e. wcel 2176  (class class class)co 5944   RRcr 7924   1c1 7926   + caddc 7928   2c2 9087

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1re 8019  ax-addrcl 8022

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201  df-2 9095

This theorem is referenced by:  2cn  9107  3re  9110  2ne0  9128  2ap0  9129  3pos  9130  2lt3  9207  1lt3  9208  2lt4  9210  1lt4  9211  2lt5  9214  2lt6  9219  1lt6  9220  2lt7  9225  1lt7  9226  2lt8  9232  1lt8  9233  2lt9  9240  1lt9  9241  1ap2  9244  1le2  9245  2rene0  9247  halfre  9250  halfgt0  9252  halflt1  9254  rehalfcl  9264  halfpos2  9267  halfnneg2  9269  addltmul  9274  nominpos  9275  avglt1  9276  avglt2  9277  div4p1lem1div2  9291  nn0lele2xi  9346  nn0ge2m1nn  9355  halfnz  9469  3halfnz  9470  2lt10  9641  1lt10  9642  eluz4eluz2  9688  uzuzle23  9692  uz3m2nn  9694  2rp  9780  xleaddadd  10009  fztpval  10205  fz0to4untppr  10246  fzo0to42pr  10349  qbtwnrelemcalc  10398  qbtwnre  10399  2tnp1ge0ge0  10444  flhalf  10445  fldiv4p1lem1div2  10448  mulp1mod1  10510  expubnd  10741  nn0opthlem2d  10866  faclbnd2  10887  4bc2eq6  10919  wrdlenge2n0  11029  cvg1nlemres  11296  resqrexlemover  11321  resqrexlemga  11334  sqrt4  11358  sqrt2gt1lt2  11360  abstri  11415  amgm2  11429  maxabslemlub  11518  maxltsup  11529  bdtrilem  11550  efcllemp  11969  efcllem  11970  ege2le3  11982  ef01bndlem  12067  cos01bnd  12069  cos2bnd  12071  cos01gt0  12074  sin02gt0  12075  sincos2sgn  12077  sin4lt0  12078  cos12dec  12079  eirraplem  12088  egt2lt3  12091  epos  12092  ene1  12096  eap1  12097  oexpneg  12188  oddge22np1  12192  evennn02n  12193  evennn2n  12194  nn0ehalf  12214  nno  12217  nn0o  12218  nn0oddm1d2  12220  nnoddm1d2  12221  flodddiv4t2lthalf  12250  bitsp1o  12264  bitsfzolem  12265  bitsfzo  12266  bitsfi  12268  6gcd4e2  12316  ncoprmgcdne1b  12411  prmdc  12452  3lcm2e6  12482  sqrt2irrlem  12483  sqrt2re  12485  sqrt2irraplemnn  12501  sqrt2irrap  12502  4sqlem11  12724  4sqlem12  12725  2expltfac  12762  plusgndxnmulrndx  12965  starvndxnplusgndx  12975  scandxnplusgndx  12987  vscandxnplusgndx  12992  ipndxnplusgndx  13005  tsetndxnplusgndx  13024  plendxnplusgndx  13038  dsndxnplusgndx  13053  slotsdifunifndx  13064  bl2in  14875  hoverb  15120  ivthdichlem  15123  reeff1o  15245  cosz12  15252  sin0pilem1  15253  sin0pilem2  15254  pilem3  15255  pipos  15260  sinhalfpilem  15263  sincosq1lem  15297  sincosq4sgn  15301  sinq12gt0  15302  cosq23lt0  15305  coseq00topi  15307  coseq0negpitopi  15308  tangtx  15310  sincos4thpi  15312  tan4thpi  15313  sincos6thpi  15314  cosordlem  15321  cosq34lt1  15322  cos02pilt1  15323  cos0pilt1  15324  2logb9irr  15443  2logb3irr  15445  2logb9irrALT  15446  sqrt2cxp2logb9e3  15447  2logb9irrap  15449  mersenne  15469  perfectlem1  15471  perfectlem2  15472  lgslem1  15477  lgsdirprm  15511  gausslemma2dlem0c  15528  gausslemma2dlem1a  15535  gausslemma2dlem2  15539  gausslemma2dlem3  15540  gausslemma2dlem4  15541  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  2lgslem1a1  15563  2lgslem1a2  15564  2lgslem1c  15567  2lgslem4  15580  ex-fl  15665  taupi  16016