Theorem 2re 9108

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 9097	. 2 |- 2 = ( 1 + 1 )
2		1re 8073	. . 3 |- 1 e. RR
3	2, 2	readdcli 8087	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2278	1 |- 2 e. RR

Syntax hints:   e. wcel 2176  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930   2c2 9089

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201  df-2 9097

This theorem is referenced by:  2cn  9109  3re  9112  2ne0  9130  2ap0  9131  3pos  9132  2lt3  9209  1lt3  9210  2lt4  9212  1lt4  9213  2lt5  9216  2lt6  9221  1lt6  9222  2lt7  9227  1lt7  9228  2lt8  9234  1lt8  9235  2lt9  9242  1lt9  9243  1ap2  9246  1le2  9247  2rene0  9249  halfre  9252  halfgt0  9254  halflt1  9256  rehalfcl  9266  halfpos2  9269  halfnneg2  9271  addltmul  9276  nominpos  9277  avglt1  9278  avglt2  9279  div4p1lem1div2  9293  nn0lele2xi  9348  nn0ge2m1nn  9357  halfnz  9471  3halfnz  9472  2lt10  9643  1lt10  9644  eluz4eluz2  9690  uzuzle23  9694  uz3m2nn  9696  2rp  9782  xleaddadd  10011  fztpval  10207  fz0to4untppr  10248  fzo0to42pr  10351  qbtwnrelemcalc  10400  qbtwnre  10401  2tnp1ge0ge0  10446  flhalf  10447  fldiv4p1lem1div2  10450  mulp1mod1  10512  expubnd  10743  nn0opthlem2d  10868  faclbnd2  10889  4bc2eq6  10921  wrdlenge2n0  11031  cvg1nlemres  11329  resqrexlemover  11354  resqrexlemga  11367  sqrt4  11391  sqrt2gt1lt2  11393  abstri  11448  amgm2  11462  maxabslemlub  11551  maxltsup  11562  bdtrilem  11583  efcllemp  12002  efcllem  12003  ege2le3  12015  ef01bndlem  12100  cos01bnd  12102  cos2bnd  12104  cos01gt0  12107  sin02gt0  12108  sincos2sgn  12110  sin4lt0  12111  cos12dec  12112  eirraplem  12121  egt2lt3  12124  epos  12125  ene1  12129  eap1  12130  oexpneg  12221  oddge22np1  12225  evennn02n  12226  evennn2n  12227  nn0ehalf  12247  nno  12250  nn0o  12251  nn0oddm1d2  12253  nnoddm1d2  12254  flodddiv4t2lthalf  12283  bitsp1o  12297  bitsfzolem  12298  bitsfzo  12299  bitsfi  12301  6gcd4e2  12349  ncoprmgcdne1b  12444  prmdc  12485  3lcm2e6  12515  sqrt2irrlem  12516  sqrt2re  12518  sqrt2irraplemnn  12534  sqrt2irrap  12535  4sqlem11  12757  4sqlem12  12758  2expltfac  12795  plusgndxnmulrndx  12998  starvndxnplusgndx  13008  scandxnplusgndx  13020  vscandxnplusgndx  13025  ipndxnplusgndx  13038  tsetndxnplusgndx  13057  plendxnplusgndx  13071  dsndxnplusgndx  13086  slotsdifunifndx  13097  bl2in  14908  hoverb  15153  ivthdichlem  15156  reeff1o  15278  cosz12  15285  sin0pilem1  15286  sin0pilem2  15287  pilem3  15288  pipos  15293  sinhalfpilem  15296  sincosq1lem  15330  sincosq4sgn  15334  sinq12gt0  15335  cosq23lt0  15338  coseq00topi  15340  coseq0negpitopi  15341  tangtx  15343  sincos4thpi  15345  tan4thpi  15346  sincos6thpi  15347  cosordlem  15354  cosq34lt1  15355  cos02pilt1  15356  cos0pilt1  15357  2logb9irr  15476  2logb3irr  15478  2logb9irrALT  15479  sqrt2cxp2logb9e3  15480  2logb9irrap  15482  mersenne  15502  perfectlem1  15504  perfectlem2  15505  lgslem1  15510  lgsdirprm  15544  gausslemma2dlem0c  15561  gausslemma2dlem1a  15568  gausslemma2dlem2  15572  gausslemma2dlem3  15573  gausslemma2dlem4  15574  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisen  15584  lgsquadlem1  15587  lgsquadlem2  15588  2lgslem1a1  15596  2lgslem1a2  15597  2lgslem1c  15600  2lgslem4  15613  ex-fl  15698  taupi  16049