Theorem 2re 9353

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 9342	. 2 ⊢ 2 = (1 + 1)
2		1re 8315	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8329	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2311	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2209  (class class class)co 6075  ℝcr 8168  1c1 8170   + caddc 8172  2c2 9334

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1re 8263  ax-addrcl 8266

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-2 9342

This theorem is referenced by:  2cn  9354  3re  9357  2ne0  9375  2ap0  9376  3pos  9377  2lt3  9454  1lt3  9455  2lt4  9457  1lt4  9458  2lt5  9461  2lt6  9466  1lt6  9467  2lt7  9472  1lt7  9473  2lt8  9479  1lt8  9480  2lt9  9487  1lt9  9488  1ap2  9491  1le2  9492  2rene0  9494  halfre  9497  halfgt0  9499  halflt1  9501  rehalfcl  9511  halfpos2  9514  halfnneg2  9516  addltmul  9521  nominpos  9522  avglt1  9523  avglt2  9524  div4p1lem1div2  9538  nn0lele2xi  9593  nn0ge2m1nn  9606  halfnz  9721  3halfnz  9722  2lt10  9893  1lt10  9894  uzuzle23  9941  uzuzle24  9942  eluz4eluz2  9947  uz3m2nn  9952  2rp  10038  xleaddadd  10268  fztpval  10468  fz0to4untppr  10509  fzo0to42pr  10616  qbtwnrelemcalc  10668  qbtwnre  10669  2tnp1ge0ge0  10714  flhalf  10715  fldiv4p1lem1div2  10718  mulp1mod1  10780  expubnd  11011  nn0opthlem2d  11137  faclbnd2  11158  4bc2eq6  11191  hashtpglem  11276  wrdlenge2n0  11318  sq01  11638  cvg1nlemres  11729  resqrexlemover  11754  resqrexlemga  11767  sqrt4  11791  sqrt2gt1lt2  11793  abstri  11848  amgm2  11862  maxabslemlub  11951  maxltsup  11962  bdtrilem  11983  efcllemp  12403  efcllem  12404  ege2le3  12416  ef01bndlem  12501  cos01bnd  12503  cos2bnd  12505  cos01gt0  12508  sin02gt0  12509  sincos2sgn  12511  sin4lt0  12512  cos12dec  12513  eirraplem  12522  egt2lt3  12525  epos  12526  ene1  12530  eap1  12531  oexpneg  12622  oddge22np1  12626  evennn02n  12627  evennn2n  12628  nn0ehalf  12648  nno  12651  nn0o  12652  nn0oddm1d2  12654  nnoddm1d2  12655  flodddiv4t2lthalf  12684  bitsp1o  12698  bitsfzolem  12699  bitsfzo  12700  bitsfi  12702  6gcd4e2  12750  ncoprmgcdne1b  12845  prmdc  12886  3lcm2e6  12916  sqrt2irrlem  12917  sqrt2re  12919  sqrt2irraplemnn  12935  sqrt2irrap  12936  4sqlem11  13158  4sqlem12  13159  2expltfac  13196  ballotfilem2  13206  plusgndxnmulrndx  13464  starvndxnplusgndx  13474  scandxnplusgndx  13486  vscandxnplusgndx  13491  ipndxnplusgndx  13504  tsetndxnplusgndx  13523  plendxnplusgndx  13537  dsndxnplusgndx  13552  slotsdifunifndx  13563  bl2in  15427  hoverb  15672  ivthdichlem  15675  reeff1o  15797  cosz12  15804  sin0pilem1  15805  sin0pilem2  15806  pilem3  15807  pipos  15812  sinhalfpilem  15815  sincosq1lem  15849  sincosq4sgn  15853  sinq12gt0  15854  cosq23lt0  15857  coseq00topi  15859  coseq0negpitopi  15860  tangtx  15862  sincos4thpi  15864  tan4thpi  15865  sincos6thpi  15866  cosordlem  15873  cosq34lt1  15874  cos02pilt1  15875  cos0pilt1  15876  2logb9irr  15996  2logb3irr  15998  2logb9irrALT  15999  sqrt2cxp2logb9e3  16000  2logb9irrap  16002  pellexlem2  16006  mersenne  16025  perfectlem1  16027  perfectlem2  16028  lgslem1  16033  lgsdirprm  16067  gausslemma2dlem0c  16084  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  gausslemma2dlem3  16096  gausslemma2dlem4  16097  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem1a1  16119  2lgslem1a2  16120  2lgslem1c  16123  2lgslem4  16136  usgrexmpldifpr  16404  clwwlkext2edg  16577  konigsbergiedgwen  16639  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberg  16648  ex-fl  16653  taupi  17028