Theorem 2re 9136

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 9125	. 2 ⊢ 2 = (1 + 1)
2		1re 8101	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8115	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2279	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2177  (class class class)co 5962  ℝcr 7954  1c1 7956   + caddc 7958  2c2 9117

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188  ax-1re 8049  ax-addrcl 8052

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202  df-2 9125

This theorem is referenced by:  2cn  9137  3re  9140  2ne0  9158  2ap0  9159  3pos  9160  2lt3  9237  1lt3  9238  2lt4  9240  1lt4  9241  2lt5  9244  2lt6  9249  1lt6  9250  2lt7  9255  1lt7  9256  2lt8  9262  1lt8  9263  2lt9  9270  1lt9  9271  1ap2  9274  1le2  9275  2rene0  9277  halfre  9280  halfgt0  9282  halflt1  9284  rehalfcl  9294  halfpos2  9297  halfnneg2  9299  addltmul  9304  nominpos  9305  avglt1  9306  avglt2  9307  div4p1lem1div2  9321  nn0lele2xi  9376  nn0ge2m1nn  9385  halfnz  9499  3halfnz  9500  2lt10  9671  1lt10  9672  eluz4eluz2  9718  uzuzle23  9722  uz3m2nn  9724  2rp  9810  xleaddadd  10039  fztpval  10235  fz0to4untppr  10276  fzo0to42pr  10381  qbtwnrelemcalc  10430  qbtwnre  10431  2tnp1ge0ge0  10476  flhalf  10477  fldiv4p1lem1div2  10480  mulp1mod1  10542  expubnd  10773  nn0opthlem2d  10898  faclbnd2  10919  4bc2eq6  10951  wrdlenge2n0  11061  cvg1nlemres  11381  resqrexlemover  11406  resqrexlemga  11419  sqrt4  11443  sqrt2gt1lt2  11445  abstri  11500  amgm2  11514  maxabslemlub  11603  maxltsup  11614  bdtrilem  11635  efcllemp  12054  efcllem  12055  ege2le3  12067  ef01bndlem  12152  cos01bnd  12154  cos2bnd  12156  cos01gt0  12159  sin02gt0  12160  sincos2sgn  12162  sin4lt0  12163  cos12dec  12164  eirraplem  12173  egt2lt3  12176  epos  12177  ene1  12181  eap1  12182  oexpneg  12273  oddge22np1  12277  evennn02n  12278  evennn2n  12279  nn0ehalf  12299  nno  12302  nn0o  12303  nn0oddm1d2  12305  nnoddm1d2  12306  flodddiv4t2lthalf  12335  bitsp1o  12349  bitsfzolem  12350  bitsfzo  12351  bitsfi  12353  6gcd4e2  12401  ncoprmgcdne1b  12496  prmdc  12537  3lcm2e6  12567  sqrt2irrlem  12568  sqrt2re  12570  sqrt2irraplemnn  12586  sqrt2irrap  12587  4sqlem11  12809  4sqlem12  12810  2expltfac  12847  plusgndxnmulrndx  13050  starvndxnplusgndx  13060  scandxnplusgndx  13072  vscandxnplusgndx  13077  ipndxnplusgndx  13090  tsetndxnplusgndx  13109  plendxnplusgndx  13123  dsndxnplusgndx  13138  slotsdifunifndx  13149  bl2in  14960  hoverb  15205  ivthdichlem  15208  reeff1o  15330  cosz12  15337  sin0pilem1  15338  sin0pilem2  15339  pilem3  15340  pipos  15345  sinhalfpilem  15348  sincosq1lem  15382  sincosq4sgn  15386  sinq12gt0  15387  cosq23lt0  15390  coseq00topi  15392  coseq0negpitopi  15393  tangtx  15395  sincos4thpi  15397  tan4thpi  15398  sincos6thpi  15399  cosordlem  15406  cosq34lt1  15407  cos02pilt1  15408  cos0pilt1  15409  2logb9irr  15528  2logb3irr  15530  2logb9irrALT  15531  sqrt2cxp2logb9e3  15532  2logb9irrap  15534  mersenne  15554  perfectlem1  15556  perfectlem2  15557  lgslem1  15562  lgsdirprm  15596  gausslemma2dlem0c  15613  gausslemma2dlem1a  15620  gausslemma2dlem2  15624  gausslemma2dlem3  15625  gausslemma2dlem4  15626  lgseisenlem1  15632  lgseisenlem2  15633  lgseisenlem3  15634  lgseisen  15636  lgsquadlem1  15639  lgsquadlem2  15640  2lgslem1a1  15648  2lgslem1a2  15649  2lgslem1c  15652  2lgslem4  15665  ex-fl  15831  taupi  16184