Theorem 2re 9141

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 9130	. 2 |- 2 = ( 1 + 1 )
2		1re 8106	. . 3 |- 1 e. RR
3	2, 2	readdcli 8120	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2280	1 |- 2 e. RR

Syntax hints:   e. wcel 2178  (class class class)co 5967   RRcr 7959   1c1 7961   + caddc 7963   2c2 9122

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203  df-2 9130

This theorem is referenced by:  2cn  9142  3re  9145  2ne0  9163  2ap0  9164  3pos  9165  2lt3  9242  1lt3  9243  2lt4  9245  1lt4  9246  2lt5  9249  2lt6  9254  1lt6  9255  2lt7  9260  1lt7  9261  2lt8  9267  1lt8  9268  2lt9  9275  1lt9  9276  1ap2  9279  1le2  9280  2rene0  9282  halfre  9285  halfgt0  9287  halflt1  9289  rehalfcl  9299  halfpos2  9302  halfnneg2  9304  addltmul  9309  nominpos  9310  avglt1  9311  avglt2  9312  div4p1lem1div2  9326  nn0lele2xi  9381  nn0ge2m1nn  9390  halfnz  9504  3halfnz  9505  2lt10  9676  1lt10  9677  eluz4eluz2  9723  uzuzle23  9727  uz3m2nn  9729  2rp  9815  xleaddadd  10044  fztpval  10240  fz0to4untppr  10281  fzo0to42pr  10386  qbtwnrelemcalc  10435  qbtwnre  10436  2tnp1ge0ge0  10481  flhalf  10482  fldiv4p1lem1div2  10485  mulp1mod1  10547  expubnd  10778  nn0opthlem2d  10903  faclbnd2  10924  4bc2eq6  10956  wrdlenge2n0  11066  cvg1nlemres  11411  resqrexlemover  11436  resqrexlemga  11449  sqrt4  11473  sqrt2gt1lt2  11475  abstri  11530  amgm2  11544  maxabslemlub  11633  maxltsup  11644  bdtrilem  11665  efcllemp  12084  efcllem  12085  ege2le3  12097  ef01bndlem  12182  cos01bnd  12184  cos2bnd  12186  cos01gt0  12189  sin02gt0  12190  sincos2sgn  12192  sin4lt0  12193  cos12dec  12194  eirraplem  12203  egt2lt3  12206  epos  12207  ene1  12211  eap1  12212  oexpneg  12303  oddge22np1  12307  evennn02n  12308  evennn2n  12309  nn0ehalf  12329  nno  12332  nn0o  12333  nn0oddm1d2  12335  nnoddm1d2  12336  flodddiv4t2lthalf  12365  bitsp1o  12379  bitsfzolem  12380  bitsfzo  12381  bitsfi  12383  6gcd4e2  12431  ncoprmgcdne1b  12526  prmdc  12567  3lcm2e6  12597  sqrt2irrlem  12598  sqrt2re  12600  sqrt2irraplemnn  12616  sqrt2irrap  12617  4sqlem11  12839  4sqlem12  12840  2expltfac  12877  plusgndxnmulrndx  13080  starvndxnplusgndx  13090  scandxnplusgndx  13102  vscandxnplusgndx  13107  ipndxnplusgndx  13120  tsetndxnplusgndx  13139  plendxnplusgndx  13153  dsndxnplusgndx  13168  slotsdifunifndx  13179  bl2in  14990  hoverb  15235  ivthdichlem  15238  reeff1o  15360  cosz12  15367  sin0pilem1  15368  sin0pilem2  15369  pilem3  15370  pipos  15375  sinhalfpilem  15378  sincosq1lem  15412  sincosq4sgn  15416  sinq12gt0  15417  cosq23lt0  15420  coseq00topi  15422  coseq0negpitopi  15423  tangtx  15425  sincos4thpi  15427  tan4thpi  15428  sincos6thpi  15429  cosordlem  15436  cosq34lt1  15437  cos02pilt1  15438  cos0pilt1  15439  2logb9irr  15558  2logb3irr  15560  2logb9irrALT  15561  sqrt2cxp2logb9e3  15562  2logb9irrap  15564  mersenne  15584  perfectlem1  15586  perfectlem2  15587  lgslem1  15592  lgsdirprm  15626  gausslemma2dlem0c  15643  gausslemma2dlem1a  15650  gausslemma2dlem2  15654  gausslemma2dlem3  15655  gausslemma2dlem4  15656  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  2lgslem1a1  15678  2lgslem1a2  15679  2lgslem1c  15682  2lgslem4  15695  ex-fl  15861  taupi  16214