Theorem 2re 8985

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	⊢ 2 ∈ ℝ

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 8974	. 2 ⊢ 2 = (1 + 1)
2		1re 7953	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 7967	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2250	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2148  (class class class)co 5872  ℝcr 7807  1c1 7809   + caddc 7811  2c2 8966

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 7902  ax-addrcl 7905

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

This theorem is referenced by:  2cn  8986  3re  8989  2ne0  9007  2ap0  9008  3pos  9009  2lt3  9085  1lt3  9086  2lt4  9088  1lt4  9089  2lt5  9092  2lt6  9097  1lt6  9098  2lt7  9103  1lt7  9104  2lt8  9110  1lt8  9111  2lt9  9118  1lt9  9119  1ap2  9122  1le2  9123  2rene0  9125  halfre  9128  halfgt0  9130  halflt1  9132  rehalfcl  9142  halfpos2  9145  halfnneg2  9147  addltmul  9151  nominpos  9152  avglt1  9153  avglt2  9154  div4p1lem1div2  9168  nn0lele2xi  9223  nn0ge2m1nn  9232  halfnz  9345  3halfnz  9346  2lt10  9517  1lt10  9518  eluz4eluz2  9563  uzuzle23  9567  uz3m2nn  9569  2rp  9654  xleaddadd  9883  fztpval  10078  fz0to4untppr  10119  fzo0to42pr  10215  qbtwnrelemcalc  10251  qbtwnre  10252  2tnp1ge0ge0  10296  flhalf  10297  fldiv4p1lem1div2  10300  mulp1mod1  10360  expubnd  10572  nn0opthlem2d  10694  faclbnd2  10715  4bc2eq6  10747  cvg1nlemres  10987  resqrexlemover  11012  resqrexlemga  11025  sqrt4  11049  sqrt2gt1lt2  11051  abstri  11106  amgm2  11120  maxabslemlub  11209  maxltsup  11220  bdtrilem  11240  efcllemp  11659  efcllem  11660  ege2le3  11672  ef01bndlem  11757  cos01bnd  11759  cos2bnd  11761  cos01gt0  11763  sin02gt0  11764  sincos2sgn  11766  sin4lt0  11767  cos12dec  11768  eirraplem  11777  egt2lt3  11780  epos  11781  ene1  11785  eap1  11786  oexpneg  11874  oddge22np1  11878  evennn02n  11879  evennn2n  11880  nn0ehalf  11900  nno  11903  nn0o  11904  nn0oddm1d2  11906  nnoddm1d2  11907  flodddiv4t2lthalf  11934  6gcd4e2  11988  ncoprmgcdne1b  12081  prmdc  12122  3lcm2e6  12152  sqrt2irrlem  12153  sqrt2re  12155  sqrt2irraplemnn  12171  sqrt2irrap  12172  plusgndxnmulrndx  12583  starvndxnplusgndx  12593  scandxnplusgndx  12605  vscandxnplusgndx  12610  ipndxnplusgndx  12623  tsetndxnplusgndx  12639  plendxnplusgndx  12653  dsndxnplusgndx  12664  slotsdifunifndx  12675  bl2in  13774  reeff1o  14065  cosz12  14072  sin0pilem1  14073  sin0pilem2  14074  pilem3  14075  pipos  14080  sinhalfpilem  14083  sincosq1lem  14117  sincosq4sgn  14121  sinq12gt0  14122  cosq23lt0  14125  coseq00topi  14127  coseq0negpitopi  14128  tangtx  14130  sincos4thpi  14132  tan4thpi  14133  sincos6thpi  14134  cosordlem  14141  cosq34lt1  14142  cos02pilt1  14143  cos0pilt1  14144  2logb9irr  14260  2logb3irr  14262  2logb9irrALT  14263  sqrt2cxp2logb9e3  14264  2logb9irrap  14266  lgslem1  14272  lgsdirprm  14306  ex-fl  14337  taupi  14680