Theorem 2re 9191

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

Syntax hints:   e. wcel 2200  (class class class)co 6007   RRcr 8009   1c1 8011   + caddc 8013   2c2 9172

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 8104  ax-addrcl 8107

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

This theorem is referenced by:  2cn  9192  3re  9195  2ne0  9213  2ap0  9214  3pos  9215  2lt3  9292  1lt3  9293  2lt4  9295  1lt4  9296  2lt5  9299  2lt6  9304  1lt6  9305  2lt7  9310  1lt7  9311  2lt8  9317  1lt8  9318  2lt9  9325  1lt9  9326  1ap2  9329  1le2  9330  2rene0  9332  halfre  9335  halfgt0  9337  halflt1  9339  rehalfcl  9349  halfpos2  9352  halfnneg2  9354  addltmul  9359  nominpos  9360  avglt1  9361  avglt2  9362  div4p1lem1div2  9376  nn0lele2xi  9431  nn0ge2m1nn  9440  halfnz  9554  3halfnz  9555  2lt10  9726  1lt10  9727  eluz4eluz2  9774  uzuzle23  9778  uz3m2nn  9780  2rp  9866  xleaddadd  10095  fztpval  10291  fz0to4untppr  10332  fzo0to42pr  10438  qbtwnrelemcalc  10487  qbtwnre  10488  2tnp1ge0ge0  10533  flhalf  10534  fldiv4p1lem1div2  10537  mulp1mod1  10599  expubnd  10830  nn0opthlem2d  10955  faclbnd2  10976  4bc2eq6  11008  wrdlenge2n0  11120  cvg1nlemres  11512  resqrexlemover  11537  resqrexlemga  11550  sqrt4  11574  sqrt2gt1lt2  11576  abstri  11631  amgm2  11645  maxabslemlub  11734  maxltsup  11745  bdtrilem  11766  efcllemp  12185  efcllem  12186  ege2le3  12198  ef01bndlem  12283  cos01bnd  12285  cos2bnd  12287  cos01gt0  12290  sin02gt0  12291  sincos2sgn  12293  sin4lt0  12294  cos12dec  12295  eirraplem  12304  egt2lt3  12307  epos  12308  ene1  12312  eap1  12313  oexpneg  12404  oddge22np1  12408  evennn02n  12409  evennn2n  12410  nn0ehalf  12430  nno  12433  nn0o  12434  nn0oddm1d2  12436  nnoddm1d2  12437  flodddiv4t2lthalf  12466  bitsp1o  12480  bitsfzolem  12481  bitsfzo  12482  bitsfi  12484  6gcd4e2  12532  ncoprmgcdne1b  12627  prmdc  12668  3lcm2e6  12698  sqrt2irrlem  12699  sqrt2re  12701  sqrt2irraplemnn  12717  sqrt2irrap  12718  4sqlem11  12940  4sqlem12  12941  2expltfac  12978  plusgndxnmulrndx  13182  starvndxnplusgndx  13192  scandxnplusgndx  13204  vscandxnplusgndx  13209  ipndxnplusgndx  13222  tsetndxnplusgndx  13241  plendxnplusgndx  13255  dsndxnplusgndx  13270  slotsdifunifndx  13281  bl2in  15093  hoverb  15338  ivthdichlem  15341  reeff1o  15463  cosz12  15470  sin0pilem1  15471  sin0pilem2  15472  pilem3  15473  pipos  15478  sinhalfpilem  15481  sincosq1lem  15515  sincosq4sgn  15519  sinq12gt0  15520  cosq23lt0  15523  coseq00topi  15525  coseq0negpitopi  15526  tangtx  15528  sincos4thpi  15530  tan4thpi  15531  sincos6thpi  15532  cosordlem  15539  cosq34lt1  15540  cos02pilt1  15541  cos0pilt1  15542  2logb9irr  15661  2logb3irr  15663  2logb9irrALT  15664  sqrt2cxp2logb9e3  15665  2logb9irrap  15667  mersenne  15687  perfectlem1  15689  perfectlem2  15690  lgslem1  15695  lgsdirprm  15729  gausslemma2dlem0c  15746  gausslemma2dlem1a  15753  gausslemma2dlem2  15757  gausslemma2dlem3  15758  gausslemma2dlem4  15759  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  2lgslem1a1  15781  2lgslem1a2  15782  2lgslem1c  15785  2lgslem4  15798  clwwlkext2edg  16164  ex-fl  16172  taupi  16529