Theorem 2re 9176

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

Syntax hints:   ∈ wcel 2200  (class class class)co 6000  ℝcr 7994  1c1 7996   + caddc 7998  2c2 9157

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 8089  ax-addrcl 8092

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

This theorem is referenced by:  2cn  9177  3re  9180  2ne0  9198  2ap0  9199  3pos  9200  2lt3  9277  1lt3  9278  2lt4  9280  1lt4  9281  2lt5  9284  2lt6  9289  1lt6  9290  2lt7  9295  1lt7  9296  2lt8  9302  1lt8  9303  2lt9  9310  1lt9  9311  1ap2  9314  1le2  9315  2rene0  9317  halfre  9320  halfgt0  9322  halflt1  9324  rehalfcl  9334  halfpos2  9337  halfnneg2  9339  addltmul  9344  nominpos  9345  avglt1  9346  avglt2  9347  div4p1lem1div2  9361  nn0lele2xi  9416  nn0ge2m1nn  9425  halfnz  9539  3halfnz  9540  2lt10  9711  1lt10  9712  eluz4eluz2  9758  uzuzle23  9762  uz3m2nn  9764  2rp  9850  xleaddadd  10079  fztpval  10275  fz0to4untppr  10316  fzo0to42pr  10421  qbtwnrelemcalc  10470  qbtwnre  10471  2tnp1ge0ge0  10516  flhalf  10517  fldiv4p1lem1div2  10520  mulp1mod1  10582  expubnd  10813  nn0opthlem2d  10938  faclbnd2  10959  4bc2eq6  10991  wrdlenge2n0  11102  cvg1nlemres  11491  resqrexlemover  11516  resqrexlemga  11529  sqrt4  11553  sqrt2gt1lt2  11555  abstri  11610  amgm2  11624  maxabslemlub  11713  maxltsup  11724  bdtrilem  11745  efcllemp  12164  efcllem  12165  ege2le3  12177  ef01bndlem  12262  cos01bnd  12264  cos2bnd  12266  cos01gt0  12269  sin02gt0  12270  sincos2sgn  12272  sin4lt0  12273  cos12dec  12274  eirraplem  12283  egt2lt3  12286  epos  12287  ene1  12291  eap1  12292  oexpneg  12383  oddge22np1  12387  evennn02n  12388  evennn2n  12389  nn0ehalf  12409  nno  12412  nn0o  12413  nn0oddm1d2  12415  nnoddm1d2  12416  flodddiv4t2lthalf  12445  bitsp1o  12459  bitsfzolem  12460  bitsfzo  12461  bitsfi  12463  6gcd4e2  12511  ncoprmgcdne1b  12606  prmdc  12647  3lcm2e6  12677  sqrt2irrlem  12678  sqrt2re  12680  sqrt2irraplemnn  12696  sqrt2irrap  12697  4sqlem11  12919  4sqlem12  12920  2expltfac  12957  plusgndxnmulrndx  13161  starvndxnplusgndx  13171  scandxnplusgndx  13183  vscandxnplusgndx  13188  ipndxnplusgndx  13201  tsetndxnplusgndx  13220  plendxnplusgndx  13234  dsndxnplusgndx  13249  slotsdifunifndx  13260  bl2in  15071  hoverb  15316  ivthdichlem  15319  reeff1o  15441  cosz12  15448  sin0pilem1  15449  sin0pilem2  15450  pilem3  15451  pipos  15456  sinhalfpilem  15459  sincosq1lem  15493  sincosq4sgn  15497  sinq12gt0  15498  cosq23lt0  15501  coseq00topi  15503  coseq0negpitopi  15504  tangtx  15506  sincos4thpi  15508  tan4thpi  15509  sincos6thpi  15510  cosordlem  15517  cosq34lt1  15518  cos02pilt1  15519  cos0pilt1  15520  2logb9irr  15639  2logb3irr  15641  2logb9irrALT  15642  sqrt2cxp2logb9e3  15643  2logb9irrap  15645  mersenne  15665  perfectlem1  15667  perfectlem2  15668  lgslem1  15673  lgsdirprm  15707  gausslemma2dlem0c  15724  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  gausslemma2dlem3  15736  gausslemma2dlem4  15737  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem1a1  15759  2lgslem1a2  15760  2lgslem1c  15763  2lgslem4  15776  ex-fl  16047  taupi  16400