Theorem 2re 8991

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 8980	. 2 |- 2 = ( 1 + 1 )
2		1re 7958	. . 3 |- 1 e. RR
3	2, 2	readdcli 7972	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2250	1 |- 2 e. RR

Syntax hints:   e. wcel 2148  (class class class)co 5877   RRcr 7812   1c1 7814   + caddc 7816   2c2 8972

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7907  ax-addrcl 7910

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8980

This theorem is referenced by:  2cn  8992  3re  8995  2ne0  9013  2ap0  9014  3pos  9015  2lt3  9091  1lt3  9092  2lt4  9094  1lt4  9095  2lt5  9098  2lt6  9103  1lt6  9104  2lt7  9109  1lt7  9110  2lt8  9116  1lt8  9117  2lt9  9124  1lt9  9125  1ap2  9128  1le2  9129  2rene0  9131  halfre  9134  halfgt0  9136  halflt1  9138  rehalfcl  9148  halfpos2  9151  halfnneg2  9153  addltmul  9157  nominpos  9158  avglt1  9159  avglt2  9160  div4p1lem1div2  9174  nn0lele2xi  9229  nn0ge2m1nn  9238  halfnz  9351  3halfnz  9352  2lt10  9523  1lt10  9524  eluz4eluz2  9569  uzuzle23  9573  uz3m2nn  9575  2rp  9660  xleaddadd  9889  fztpval  10085  fz0to4untppr  10126  fzo0to42pr  10222  qbtwnrelemcalc  10258  qbtwnre  10259  2tnp1ge0ge0  10303  flhalf  10304  fldiv4p1lem1div2  10307  mulp1mod1  10367  expubnd  10579  nn0opthlem2d  10703  faclbnd2  10724  4bc2eq6  10756  cvg1nlemres  10996  resqrexlemover  11021  resqrexlemga  11034  sqrt4  11058  sqrt2gt1lt2  11060  abstri  11115  amgm2  11129  maxabslemlub  11218  maxltsup  11229  bdtrilem  11249  efcllemp  11668  efcllem  11669  ege2le3  11681  ef01bndlem  11766  cos01bnd  11768  cos2bnd  11770  cos01gt0  11772  sin02gt0  11773  sincos2sgn  11775  sin4lt0  11776  cos12dec  11777  eirraplem  11786  egt2lt3  11789  epos  11790  ene1  11794  eap1  11795  oexpneg  11884  oddge22np1  11888  evennn02n  11889  evennn2n  11890  nn0ehalf  11910  nno  11913  nn0o  11914  nn0oddm1d2  11916  nnoddm1d2  11917  flodddiv4t2lthalf  11944  6gcd4e2  11998  ncoprmgcdne1b  12091  prmdc  12132  3lcm2e6  12162  sqrt2irrlem  12163  sqrt2re  12165  sqrt2irraplemnn  12181  sqrt2irrap  12182  plusgndxnmulrndx  12593  starvndxnplusgndx  12603  scandxnplusgndx  12615  vscandxnplusgndx  12620  ipndxnplusgndx  12633  tsetndxnplusgndx  12652  plendxnplusgndx  12666  dsndxnplusgndx  12677  slotsdifunifndx  12688  bl2in  13988  reeff1o  14279  cosz12  14286  sin0pilem1  14287  sin0pilem2  14288  pilem3  14289  pipos  14294  sinhalfpilem  14297  sincosq1lem  14331  sincosq4sgn  14335  sinq12gt0  14336  cosq23lt0  14339  coseq00topi  14341  coseq0negpitopi  14342  tangtx  14344  sincos4thpi  14346  tan4thpi  14347  sincos6thpi  14348  cosordlem  14355  cosq34lt1  14356  cos02pilt1  14357  cos0pilt1  14358  2logb9irr  14474  2logb3irr  14476  2logb9irrALT  14477  sqrt2cxp2logb9e3  14478  2logb9irrap  14480  lgslem1  14486  lgsdirprm  14520  lgseisenlem1  14535  lgseisenlem2  14536  ex-fl  14562  taupi  14906