Theorem 2re 9191

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 9180	. 2 ⊢ 2 = (1 + 1)
2		1re 8156	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8170	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2302	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6007  ℝcr 8009  1c1 8011   + caddc 8013  2c2 9172

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8104  ax-addrcl 8107

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9180

This theorem is referenced by:  2cn  9192  3re  9195  2ne0  9213  2ap0  9214  3pos  9215  2lt3  9292  1lt3  9293  2lt4  9295  1lt4  9296  2lt5  9299  2lt6  9304  1lt6  9305  2lt7  9310  1lt7  9311  2lt8  9317  1lt8  9318  2lt9  9325  1lt9  9326  1ap2  9329  1le2  9330  2rene0  9332  halfre  9335  halfgt0  9337  halflt1  9339  rehalfcl  9349  halfpos2  9352  halfnneg2  9354  addltmul  9359  nominpos  9360  avglt1  9361  avglt2  9362  div4p1lem1div2  9376  nn0lele2xi  9431  nn0ge2m1nn  9440  halfnz  9554  3halfnz  9555  2lt10  9726  1lt10  9727  eluz4eluz2  9774  uzuzle23  9778  uz3m2nn  9780  2rp  9866  xleaddadd  10095  fztpval  10291  fz0to4untppr  10332  fzo0to42pr  10438  qbtwnrelemcalc  10487  qbtwnre  10488  2tnp1ge0ge0  10533  flhalf  10534  fldiv4p1lem1div2  10537  mulp1mod1  10599  expubnd  10830  nn0opthlem2d  10955  faclbnd2  10976  4bc2eq6  11008  wrdlenge2n0  11120  cvg1nlemres  11511  resqrexlemover  11536  resqrexlemga  11549  sqrt4  11573  sqrt2gt1lt2  11575  abstri  11630  amgm2  11644  maxabslemlub  11733  maxltsup  11744  bdtrilem  11765  efcllemp  12184  efcllem  12185  ege2le3  12197  ef01bndlem  12282  cos01bnd  12284  cos2bnd  12286  cos01gt0  12289  sin02gt0  12290  sincos2sgn  12292  sin4lt0  12293  cos12dec  12294  eirraplem  12303  egt2lt3  12306  epos  12307  ene1  12311  eap1  12312  oexpneg  12403  oddge22np1  12407  evennn02n  12408  evennn2n  12409  nn0ehalf  12429  nno  12432  nn0o  12433  nn0oddm1d2  12435  nnoddm1d2  12436  flodddiv4t2lthalf  12465  bitsp1o  12479  bitsfzolem  12480  bitsfzo  12481  bitsfi  12483  6gcd4e2  12531  ncoprmgcdne1b  12626  prmdc  12667  3lcm2e6  12697  sqrt2irrlem  12698  sqrt2re  12700  sqrt2irraplemnn  12716  sqrt2irrap  12717  4sqlem11  12939  4sqlem12  12940  2expltfac  12977  plusgndxnmulrndx  13181  starvndxnplusgndx  13191  scandxnplusgndx  13203  vscandxnplusgndx  13208  ipndxnplusgndx  13221  tsetndxnplusgndx  13240  plendxnplusgndx  13254  dsndxnplusgndx  13269  slotsdifunifndx  13280  bl2in  15092  hoverb  15337  ivthdichlem  15340  reeff1o  15462  cosz12  15469  sin0pilem1  15470  sin0pilem2  15471  pilem3  15472  pipos  15477  sinhalfpilem  15480  sincosq1lem  15514  sincosq4sgn  15518  sinq12gt0  15519  cosq23lt0  15522  coseq00topi  15524  coseq0negpitopi  15525  tangtx  15527  sincos4thpi  15529  tan4thpi  15530  sincos6thpi  15531  cosordlem  15538  cosq34lt1  15539  cos02pilt1  15540  cos0pilt1  15541  2logb9irr  15660  2logb3irr  15662  2logb9irrALT  15663  sqrt2cxp2logb9e3  15664  2logb9irrap  15666  mersenne  15686  perfectlem1  15688  perfectlem2  15689  lgslem1  15694  lgsdirprm  15728  gausslemma2dlem0c  15745  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  gausslemma2dlem3  15757  gausslemma2dlem4  15758  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  2lgslem1a1  15780  2lgslem1a2  15781  2lgslem1c  15784  2lgslem4  15797  ex-fl  16144  taupi  16501