Theorem 2re 9357

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 9346	. 2 |- 2 = ( 1 + 1 )
2		1re 8319	. . 3 |- 1 e. RR
3	2, 2	readdcli 8333	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2311	1 |- 2 e. RR

Syntax hints:   e. wcel 2209  (class class class)co 6079   RRcr 8172   1c1 8174   + caddc 8176   2c2 9338

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1re 8267  ax-addrcl 8270

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-2 9346

This theorem is referenced by:  2cn  9358  3re  9361  2ne0  9379  2ap0  9380  3pos  9381  2lt3  9458  1lt3  9459  2lt4  9461  1lt4  9462  2lt5  9465  2lt6  9470  1lt6  9471  2lt7  9476  1lt7  9477  2lt8  9483  1lt8  9484  2lt9  9491  1lt9  9492  1ap2  9495  1le2  9496  2rene0  9498  halfre  9501  halfgt0  9503  halflt1  9505  rehalfcl  9515  halfpos2  9518  halfnneg2  9520  addltmul  9525  nominpos  9526  avglt1  9527  avglt2  9528  div4p1lem1div2  9542  nn0lele2xi  9597  nn0ge2m1nn  9610  halfnz  9725  3halfnz  9726  2lt10  9897  1lt10  9898  uzuzle23  9945  uzuzle24  9946  eluz4eluz2  9951  uz3m2nn  9956  2rp  10042  xleaddadd  10272  fztpval  10473  fz0to4untppr  10514  fzo0to42pr  10621  qbtwnrelemcalc  10673  qbtwnre  10674  2tnp1ge0ge0  10719  flhalf  10720  fldiv4p1lem1div2  10723  mulp1mod1  10785  expubnd  11016  nn0opthlem2d  11142  faclbnd2  11163  4bc2eq6  11196  hashtpglem  11281  wrdlenge2n0  11323  sq01  11643  cvg1nlemres  11734  resqrexlemover  11759  resqrexlemga  11772  sqrt4  11796  sqrt2gt1lt2  11798  abstri  11853  amgm2  11867  maxabslemlub  11956  maxltsup  11967  bdtrilem  11988  efcllemp  12408  efcllem  12409  ege2le3  12421  ef01bndlem  12506  cos01bnd  12508  cos2bnd  12510  cos01gt0  12513  sin02gt0  12514  sincos2sgn  12516  sin4lt0  12517  cos12dec  12518  eirraplem  12527  egt2lt3  12530  epos  12531  ene1  12535  eap1  12536  oexpneg  12627  oddge22np1  12631  evennn02n  12632  evennn2n  12633  nn0ehalf  12653  nno  12656  nn0o  12657  nn0oddm1d2  12659  nnoddm1d2  12660  flodddiv4t2lthalf  12689  bitsp1o  12703  bitsfzolem  12704  bitsfzo  12705  bitsfi  12707  6gcd4e2  12755  ncoprmgcdne1b  12850  prmdc  12891  3lcm2e6  12921  sqrt2irrlem  12922  sqrt2re  12924  sqrt2irraplemnn  12940  sqrt2irrap  12941  4sqlem11  13163  4sqlem12  13164  2expltfac  13201  ballotfilem2  13211  plusgndxnmulrndx  13470  starvndxnplusgndx  13480  scandxnplusgndx  13492  vscandxnplusgndx  13497  ipndxnplusgndx  13510  tsetndxnplusgndx  13529  plendxnplusgndx  13543  dsndxnplusgndx  13558  slotsdifunifndx  13569  bl2in  15487  hoverb  15732  ivthdichlem  15735  reeff1o  15857  cosz12  15864  sin0pilem1  15865  sin0pilem2  15866  pilem3  15867  pipos  15872  sinhalfpilem  15875  sincosq1lem  15909  sincosq4sgn  15913  sinq12gt0  15914  cosq23lt0  15917  coseq00topi  15919  coseq0negpitopi  15920  tangtx  15922  sincos4thpi  15924  tan4thpi  15925  sincos6thpi  15926  cosordlem  15933  cosq34lt1  15934  cos02pilt1  15935  cos0pilt1  15936  2logb9irr  16056  2logb3irr  16058  2logb9irrALT  16059  sqrt2cxp2logb9e3  16060  2logb9irrap  16062  log2tlbndlog2  16065  log2ublem2  16067  log2ublog2  16069  pellexlem2  16075  mersenne  16094  perfectlem1  16096  perfectlem2  16097  lgslem1  16102  lgsdirprm  16136  gausslemma2dlem0c  16153  gausslemma2dlem1a  16160  gausslemma2dlem2  16164  gausslemma2dlem3  16165  gausslemma2dlem4  16166  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgseisen  16176  lgsquadlem1  16179  lgsquadlem2  16180  2lgslem1a1  16188  2lgslem1a2  16189  2lgslem1c  16192  2lgslem4  16205  usgrexmpldifpr  16473  clwwlkext2edg  16646  konigsbergiedgwen  16708  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  konigsberg  16717  ex-fl  16722  taupi  17097