Theorem 2re 9312

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 9301	. 2 |- 2 = ( 1 + 1 )
2		1re 8278	. . 3 |- 1 e. RR
3	2, 2	readdcli 8292	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2307	1 |- 2 e. RR

Syntax hints:   e. wcel 2205  (class class class)co 6052   RRcr 8131   1c1 8133   + caddc 8135   2c2 9293

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 2216  ax-1re 8226  ax-addrcl 8229

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230  df-2 9301

This theorem is referenced by:  2cn  9313  3re  9316  2ne0  9334  2ap0  9335  3pos  9336  2lt3  9413  1lt3  9414  2lt4  9416  1lt4  9417  2lt5  9420  2lt6  9425  1lt6  9426  2lt7  9431  1lt7  9432  2lt8  9438  1lt8  9439  2lt9  9446  1lt9  9447  1ap2  9450  1le2  9451  2rene0  9453  halfre  9456  halfgt0  9458  halflt1  9460  rehalfcl  9470  halfpos2  9473  halfnneg2  9475  addltmul  9480  nominpos  9481  avglt1  9482  avglt2  9483  div4p1lem1div2  9497  nn0lele2xi  9552  nn0ge2m1nn  9565  halfnz  9680  3halfnz  9681  2lt10  9852  1lt10  9853  uzuzle23  9900  uzuzle24  9901  eluz4eluz2  9906  uz3m2nn  9911  2rp  9997  xleaddadd  10226  fztpval  10424  fz0to4untppr  10465  fzo0to42pr  10572  qbtwnrelemcalc  10622  qbtwnre  10623  2tnp1ge0ge0  10668  flhalf  10669  fldiv4p1lem1div2  10672  mulp1mod1  10734  expubnd  10965  nn0opthlem2d  11091  faclbnd2  11112  4bc2eq6  11145  hashtpglem  11226  wrdlenge2n0  11268  cvg1nlemres  11678  resqrexlemover  11703  resqrexlemga  11716  sqrt4  11740  sqrt2gt1lt2  11742  abstri  11797  amgm2  11811  maxabslemlub  11900  maxltsup  11911  bdtrilem  11932  efcllemp  12352  efcllem  12353  ege2le3  12365  ef01bndlem  12450  cos01bnd  12452  cos2bnd  12454  cos01gt0  12457  sin02gt0  12458  sincos2sgn  12460  sin4lt0  12461  cos12dec  12462  eirraplem  12471  egt2lt3  12474  epos  12475  ene1  12479  eap1  12480  oexpneg  12571  oddge22np1  12575  evennn02n  12576  evennn2n  12577  nn0ehalf  12597  nno  12600  nn0o  12601  nn0oddm1d2  12603  nnoddm1d2  12604  flodddiv4t2lthalf  12633  bitsp1o  12647  bitsfzolem  12648  bitsfzo  12649  bitsfi  12651  6gcd4e2  12699  ncoprmgcdne1b  12794  prmdc  12835  3lcm2e6  12865  sqrt2irrlem  12866  sqrt2re  12868  sqrt2irraplemnn  12884  sqrt2irrap  12885  4sqlem11  13107  4sqlem12  13108  2expltfac  13145  ballotfilem2  13153  plusgndxnmulrndx  13367  starvndxnplusgndx  13377  scandxnplusgndx  13389  vscandxnplusgndx  13394  ipndxnplusgndx  13407  tsetndxnplusgndx  13426  plendxnplusgndx  13440  dsndxnplusgndx  13455  slotsdifunifndx  13466  bl2in  15317  hoverb  15562  ivthdichlem  15565  reeff1o  15687  cosz12  15694  sin0pilem1  15695  sin0pilem2  15696  pilem3  15697  pipos  15702  sinhalfpilem  15705  sincosq1lem  15739  sincosq4sgn  15743  sinq12gt0  15744  cosq23lt0  15747  coseq00topi  15749  coseq0negpitopi  15750  tangtx  15752  sincos4thpi  15754  tan4thpi  15755  sincos6thpi  15756  cosordlem  15763  cosq34lt1  15764  cos02pilt1  15765  cos0pilt1  15766  2logb9irr  15885  2logb3irr  15887  2logb9irrALT  15888  sqrt2cxp2logb9e3  15889  2logb9irrap  15891  pellexlem2  15895  mersenne  15914  perfectlem1  15916  perfectlem2  15917  lgslem1  15922  lgsdirprm  15956  gausslemma2dlem0c  15973  gausslemma2dlem1a  15980  gausslemma2dlem2  15984  gausslemma2dlem3  15985  gausslemma2dlem4  15986  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem3  15994  lgseisen  15996  lgsquadlem1  15999  lgsquadlem2  16000  2lgslem1a1  16008  2lgslem1a2  16009  2lgslem1c  16012  2lgslem4  16025  usgrexmpldifpr  16293  clwwlkext2edg  16466  konigsbergiedgwen  16528  konigsberglem1  16532  konigsberglem2  16533  konigsberglem3  16534  konigsberg  16537  ex-fl  16542  taupi  16908