Theorem 2re 9180

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

Syntax hints:   e. wcel 2200  (class class class)co 6001   RRcr 7998   1c1 8000   + caddc 8002   2c2 9161

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 8093  ax-addrcl 8096

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

This theorem is referenced by:  2cn  9181  3re  9184  2ne0  9202  2ap0  9203  3pos  9204  2lt3  9281  1lt3  9282  2lt4  9284  1lt4  9285  2lt5  9288  2lt6  9293  1lt6  9294  2lt7  9299  1lt7  9300  2lt8  9306  1lt8  9307  2lt9  9314  1lt9  9315  1ap2  9318  1le2  9319  2rene0  9321  halfre  9324  halfgt0  9326  halflt1  9328  rehalfcl  9338  halfpos2  9341  halfnneg2  9343  addltmul  9348  nominpos  9349  avglt1  9350  avglt2  9351  div4p1lem1div2  9365  nn0lele2xi  9420  nn0ge2m1nn  9429  halfnz  9543  3halfnz  9544  2lt10  9715  1lt10  9716  eluz4eluz2  9762  uzuzle23  9766  uz3m2nn  9768  2rp  9854  xleaddadd  10083  fztpval  10279  fz0to4untppr  10320  fzo0to42pr  10426  qbtwnrelemcalc  10475  qbtwnre  10476  2tnp1ge0ge0  10521  flhalf  10522  fldiv4p1lem1div2  10525  mulp1mod1  10587  expubnd  10818  nn0opthlem2d  10943  faclbnd2  10964  4bc2eq6  10996  wrdlenge2n0  11107  cvg1nlemres  11496  resqrexlemover  11521  resqrexlemga  11534  sqrt4  11558  sqrt2gt1lt2  11560  abstri  11615  amgm2  11629  maxabslemlub  11718  maxltsup  11729  bdtrilem  11750  efcllemp  12169  efcllem  12170  ege2le3  12182  ef01bndlem  12267  cos01bnd  12269  cos2bnd  12271  cos01gt0  12274  sin02gt0  12275  sincos2sgn  12277  sin4lt0  12278  cos12dec  12279  eirraplem  12288  egt2lt3  12291  epos  12292  ene1  12296  eap1  12297  oexpneg  12388  oddge22np1  12392  evennn02n  12393  evennn2n  12394  nn0ehalf  12414  nno  12417  nn0o  12418  nn0oddm1d2  12420  nnoddm1d2  12421  flodddiv4t2lthalf  12450  bitsp1o  12464  bitsfzolem  12465  bitsfzo  12466  bitsfi  12468  6gcd4e2  12516  ncoprmgcdne1b  12611  prmdc  12652  3lcm2e6  12682  sqrt2irrlem  12683  sqrt2re  12685  sqrt2irraplemnn  12701  sqrt2irrap  12702  4sqlem11  12924  4sqlem12  12925  2expltfac  12962  plusgndxnmulrndx  13166  starvndxnplusgndx  13176  scandxnplusgndx  13188  vscandxnplusgndx  13193  ipndxnplusgndx  13206  tsetndxnplusgndx  13225  plendxnplusgndx  13239  dsndxnplusgndx  13254  slotsdifunifndx  13265  bl2in  15077  hoverb  15322  ivthdichlem  15325  reeff1o  15447  cosz12  15454  sin0pilem1  15455  sin0pilem2  15456  pilem3  15457  pipos  15462  sinhalfpilem  15465  sincosq1lem  15499  sincosq4sgn  15503  sinq12gt0  15504  cosq23lt0  15507  coseq00topi  15509  coseq0negpitopi  15510  tangtx  15512  sincos4thpi  15514  tan4thpi  15515  sincos6thpi  15516  cosordlem  15523  cosq34lt1  15524  cos02pilt1  15525  cos0pilt1  15526  2logb9irr  15645  2logb3irr  15647  2logb9irrALT  15648  sqrt2cxp2logb9e3  15649  2logb9irrap  15651  mersenne  15671  perfectlem1  15673  perfectlem2  15674  lgslem1  15679  lgsdirprm  15713  gausslemma2dlem0c  15730  gausslemma2dlem1a  15737  gausslemma2dlem2  15741  gausslemma2dlem3  15742  gausslemma2dlem4  15743  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  2lgslem1a1  15765  2lgslem1a2  15766  2lgslem1c  15769  2lgslem4  15782  ex-fl  16089  taupi  16441