Theorem 2re 9327

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

Syntax hints:   e. wcel 2205  (class class class)co 6058   RRcr 8142   1c1 8144   + caddc 8146   2c2 9308

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 8237  ax-addrcl 8240

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

This theorem is referenced by:  2cn  9328  3re  9331  2ne0  9349  2ap0  9350  3pos  9351  2lt3  9428  1lt3  9429  2lt4  9431  1lt4  9432  2lt5  9435  2lt6  9440  1lt6  9441  2lt7  9446  1lt7  9447  2lt8  9453  1lt8  9454  2lt9  9461  1lt9  9462  1ap2  9465  1le2  9466  2rene0  9468  halfre  9471  halfgt0  9473  halflt1  9475  rehalfcl  9485  halfpos2  9488  halfnneg2  9490  addltmul  9495  nominpos  9496  avglt1  9497  avglt2  9498  div4p1lem1div2  9512  nn0lele2xi  9567  nn0ge2m1nn  9580  halfnz  9695  3halfnz  9696  2lt10  9867  1lt10  9868  uzuzle23  9915  uzuzle24  9916  eluz4eluz2  9921  uz3m2nn  9926  2rp  10012  xleaddadd  10242  fztpval  10442  fz0to4untppr  10483  fzo0to42pr  10590  qbtwnrelemcalc  10642  qbtwnre  10643  2tnp1ge0ge0  10688  flhalf  10689  fldiv4p1lem1div2  10692  mulp1mod1  10754  expubnd  10985  nn0opthlem2d  11111  faclbnd2  11132  4bc2eq6  11165  hashtpglem  11246  wrdlenge2n0  11288  cvg1nlemres  11698  resqrexlemover  11723  resqrexlemga  11736  sqrt4  11760  sqrt2gt1lt2  11762  abstri  11817  amgm2  11831  maxabslemlub  11920  maxltsup  11931  bdtrilem  11952  efcllemp  12372  efcllem  12373  ege2le3  12385  ef01bndlem  12470  cos01bnd  12472  cos2bnd  12474  cos01gt0  12477  sin02gt0  12478  sincos2sgn  12480  sin4lt0  12481  cos12dec  12482  eirraplem  12491  egt2lt3  12494  epos  12495  ene1  12499  eap1  12500  oexpneg  12591  oddge22np1  12595  evennn02n  12596  evennn2n  12597  nn0ehalf  12617  nno  12620  nn0o  12621  nn0oddm1d2  12623  nnoddm1d2  12624  flodddiv4t2lthalf  12653  bitsp1o  12667  bitsfzolem  12668  bitsfzo  12669  bitsfi  12671  6gcd4e2  12719  ncoprmgcdne1b  12814  prmdc  12855  3lcm2e6  12885  sqrt2irrlem  12886  sqrt2re  12888  sqrt2irraplemnn  12904  sqrt2irrap  12905  4sqlem11  13127  4sqlem12  13128  2expltfac  13165  ballotfilem2  13175  plusgndxnmulrndx  13433  starvndxnplusgndx  13443  scandxnplusgndx  13455  vscandxnplusgndx  13460  ipndxnplusgndx  13473  tsetndxnplusgndx  13492  plendxnplusgndx  13506  dsndxnplusgndx  13521  slotsdifunifndx  13532  bl2in  15397  hoverb  15642  ivthdichlem  15645  reeff1o  15767  cosz12  15774  sin0pilem1  15775  sin0pilem2  15776  pilem3  15777  pipos  15782  sinhalfpilem  15785  sincosq1lem  15819  sincosq4sgn  15823  sinq12gt0  15824  cosq23lt0  15827  coseq00topi  15829  coseq0negpitopi  15830  tangtx  15832  sincos4thpi  15834  tan4thpi  15835  sincos6thpi  15836  cosordlem  15843  cosq34lt1  15844  cos02pilt1  15845  cos0pilt1  15846  2logb9irr  15965  2logb3irr  15967  2logb9irrALT  15968  sqrt2cxp2logb9e3  15969  2logb9irrap  15971  pellexlem2  15975  mersenne  15994  perfectlem1  15996  perfectlem2  15997  lgslem1  16002  lgsdirprm  16036  gausslemma2dlem0c  16053  gausslemma2dlem1a  16060  gausslemma2dlem2  16064  gausslemma2dlem3  16065  gausslemma2dlem4  16066  lgseisenlem1  16072  lgseisenlem2  16073  lgseisenlem3  16074  lgseisen  16076  lgsquadlem1  16079  lgsquadlem2  16080  2lgslem1a1  16088  2lgslem1a2  16089  2lgslem1c  16092  2lgslem4  16105  usgrexmpldifpr  16373  clwwlkext2edg  16546  konigsbergiedgwen  16608  konigsberglem1  16612  konigsberglem2  16613  konigsberglem3  16614  konigsberg  16617  ex-fl  16622  taupi  16998