Theorem 2re 9303

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 9292	. 2 |- 2 = ( 1 + 1 )
2		1re 8269	. . 3 |- 1 e. RR
3	2, 2	readdcli 8283	. 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 8122   1c1 8124   + caddc 8126   2c2 9284

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 8217  ax-addrcl 8220

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

This theorem is referenced by:  2cn  9304  3re  9307  2ne0  9325  2ap0  9326  3pos  9327  2lt3  9404  1lt3  9405  2lt4  9407  1lt4  9408  2lt5  9411  2lt6  9416  1lt6  9417  2lt7  9422  1lt7  9423  2lt8  9429  1lt8  9430  2lt9  9437  1lt9  9438  1ap2  9441  1le2  9442  2rene0  9444  halfre  9447  halfgt0  9449  halflt1  9451  rehalfcl  9461  halfpos2  9464  halfnneg2  9466  addltmul  9471  nominpos  9472  avglt1  9473  avglt2  9474  div4p1lem1div2  9488  nn0lele2xi  9543  nn0ge2m1nn  9556  halfnz  9670  3halfnz  9671  2lt10  9842  1lt10  9843  uzuzle23  9890  uzuzle24  9891  eluz4eluz2  9896  uz3m2nn  9901  2rp  9987  xleaddadd  10216  fztpval  10413  fz0to4untppr  10454  fzo0to42pr  10561  qbtwnrelemcalc  10611  qbtwnre  10612  2tnp1ge0ge0  10657  flhalf  10658  fldiv4p1lem1div2  10661  mulp1mod1  10723  expubnd  10954  nn0opthlem2d  11079  faclbnd2  11100  4bc2eq6  11132  hashtpglem  11211  wrdlenge2n0  11253  cvg1nlemres  11663  resqrexlemover  11688  resqrexlemga  11701  sqrt4  11725  sqrt2gt1lt2  11727  abstri  11782  amgm2  11796  maxabslemlub  11885  maxltsup  11896  bdtrilem  11917  efcllemp  12337  efcllem  12338  ege2le3  12350  ef01bndlem  12435  cos01bnd  12437  cos2bnd  12439  cos01gt0  12442  sin02gt0  12443  sincos2sgn  12445  sin4lt0  12446  cos12dec  12447  eirraplem  12456  egt2lt3  12459  epos  12460  ene1  12464  eap1  12465  oexpneg  12556  oddge22np1  12560  evennn02n  12561  evennn2n  12562  nn0ehalf  12582  nno  12585  nn0o  12586  nn0oddm1d2  12588  nnoddm1d2  12589  flodddiv4t2lthalf  12618  bitsp1o  12632  bitsfzolem  12633  bitsfzo  12634  bitsfi  12636  6gcd4e2  12684  ncoprmgcdne1b  12779  prmdc  12820  3lcm2e6  12850  sqrt2irrlem  12851  sqrt2re  12853  sqrt2irraplemnn  12869  sqrt2irrap  12870  4sqlem11  13092  4sqlem12  13093  2expltfac  13130  plusgndxnmulrndx  13335  starvndxnplusgndx  13345  scandxnplusgndx  13357  vscandxnplusgndx  13362  ipndxnplusgndx  13375  tsetndxnplusgndx  13394  plendxnplusgndx  13408  dsndxnplusgndx  13423  slotsdifunifndx  13434  bl2in  15255  hoverb  15500  ivthdichlem  15503  reeff1o  15625  cosz12  15632  sin0pilem1  15633  sin0pilem2  15634  pilem3  15635  pipos  15640  sinhalfpilem  15643  sincosq1lem  15677  sincosq4sgn  15681  sinq12gt0  15682  cosq23lt0  15685  coseq00topi  15687  coseq0negpitopi  15688  tangtx  15690  sincos4thpi  15692  tan4thpi  15693  sincos6thpi  15694  cosordlem  15701  cosq34lt1  15702  cos02pilt1  15703  cos0pilt1  15704  2logb9irr  15823  2logb3irr  15825  2logb9irrALT  15826  sqrt2cxp2logb9e3  15827  2logb9irrap  15829  pellexlem2  15833  mersenne  15852  perfectlem1  15854  perfectlem2  15855  lgslem1  15860  lgsdirprm  15894  gausslemma2dlem0c  15911  gausslemma2dlem1a  15918  gausslemma2dlem2  15922  gausslemma2dlem3  15923  gausslemma2dlem4  15924  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem3  15932  lgseisen  15934  lgsquadlem1  15937  lgsquadlem2  15938  2lgslem1a1  15946  2lgslem1a2  15947  2lgslem1c  15950  2lgslem4  15963  usgrexmpldifpr  16231  clwwlkext2edg  16404  konigsbergiedgwen  16466  konigsberglem1  16470  konigsberglem2  16471  konigsberglem3  16472  konigsberg  16475  ex-fl  16480  taupi  16845