Theorem 2re 9306

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 9295	. 2 |- 2 = ( 1 + 1 )
2		1re 8272	. . 3 |- 1 e. RR
3	2, 2	readdcli 8286	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2305	1 |- 2 e. RR

Syntax hints:   e. wcel 2203  (class class class)co 6049   RRcr 8125   1c1 8127   + caddc 8129   2c2 9287

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214  ax-1re 8220  ax-addrcl 8223

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-2 9295

This theorem is referenced by:  2cn  9307  3re  9310  2ne0  9328  2ap0  9329  3pos  9330  2lt3  9407  1lt3  9408  2lt4  9410  1lt4  9411  2lt5  9414  2lt6  9419  1lt6  9420  2lt7  9425  1lt7  9426  2lt8  9432  1lt8  9433  2lt9  9440  1lt9  9441  1ap2  9444  1le2  9445  2rene0  9447  halfre  9450  halfgt0  9452  halflt1  9454  rehalfcl  9464  halfpos2  9467  halfnneg2  9469  addltmul  9474  nominpos  9475  avglt1  9476  avglt2  9477  div4p1lem1div2  9491  nn0lele2xi  9546  nn0ge2m1nn  9559  halfnz  9673  3halfnz  9674  2lt10  9845  1lt10  9846  uzuzle23  9893  uzuzle24  9894  eluz4eluz2  9899  uz3m2nn  9904  2rp  9990  xleaddadd  10219  fztpval  10416  fz0to4untppr  10457  fzo0to42pr  10564  qbtwnrelemcalc  10614  qbtwnre  10615  2tnp1ge0ge0  10660  flhalf  10661  fldiv4p1lem1div2  10664  mulp1mod1  10726  expubnd  10957  nn0opthlem2d  11082  faclbnd2  11103  4bc2eq6  11135  hashtpglem  11214  wrdlenge2n0  11256  cvg1nlemres  11666  resqrexlemover  11691  resqrexlemga  11704  sqrt4  11728  sqrt2gt1lt2  11730  abstri  11785  amgm2  11799  maxabslemlub  11888  maxltsup  11899  bdtrilem  11920  efcllemp  12340  efcllem  12341  ege2le3  12353  ef01bndlem  12438  cos01bnd  12440  cos2bnd  12442  cos01gt0  12445  sin02gt0  12446  sincos2sgn  12448  sin4lt0  12449  cos12dec  12450  eirraplem  12459  egt2lt3  12462  epos  12463  ene1  12467  eap1  12468  oexpneg  12559  oddge22np1  12563  evennn02n  12564  evennn2n  12565  nn0ehalf  12585  nno  12588  nn0o  12589  nn0oddm1d2  12591  nnoddm1d2  12592  flodddiv4t2lthalf  12621  bitsp1o  12635  bitsfzolem  12636  bitsfzo  12637  bitsfi  12639  6gcd4e2  12687  ncoprmgcdne1b  12782  prmdc  12823  3lcm2e6  12853  sqrt2irrlem  12854  sqrt2re  12856  sqrt2irraplemnn  12872  sqrt2irrap  12873  4sqlem11  13095  4sqlem12  13096  2expltfac  13133  plusgndxnmulrndx  13338  starvndxnplusgndx  13348  scandxnplusgndx  13360  vscandxnplusgndx  13365  ipndxnplusgndx  13378  tsetndxnplusgndx  13397  plendxnplusgndx  13411  dsndxnplusgndx  13426  slotsdifunifndx  13437  bl2in  15260  hoverb  15505  ivthdichlem  15508  reeff1o  15630  cosz12  15637  sin0pilem1  15638  sin0pilem2  15639  pilem3  15640  pipos  15645  sinhalfpilem  15648  sincosq1lem  15682  sincosq4sgn  15686  sinq12gt0  15687  cosq23lt0  15690  coseq00topi  15692  coseq0negpitopi  15693  tangtx  15695  sincos4thpi  15697  tan4thpi  15698  sincos6thpi  15699  cosordlem  15706  cosq34lt1  15707  cos02pilt1  15708  cos0pilt1  15709  2logb9irr  15828  2logb3irr  15830  2logb9irrALT  15831  sqrt2cxp2logb9e3  15832  2logb9irrap  15834  pellexlem2  15838  mersenne  15857  perfectlem1  15859  perfectlem2  15860  lgslem1  15865  lgsdirprm  15899  gausslemma2dlem0c  15916  gausslemma2dlem1a  15923  gausslemma2dlem2  15927  gausslemma2dlem3  15928  gausslemma2dlem4  15929  lgseisenlem1  15935  lgseisenlem2  15936  lgseisenlem3  15937  lgseisen  15939  lgsquadlem1  15942  lgsquadlem2  15943  2lgslem1a1  15951  2lgslem1a2  15952  2lgslem1c  15955  2lgslem4  15968  usgrexmpldifpr  16236  clwwlkext2edg  16409  konigsbergiedgwen  16471  konigsberglem1  16475  konigsberglem2  16476  konigsberglem3  16477  konigsberg  16480  ex-fl  16485  taupi  16850