Theorem 2re 9374

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

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178  1c1 8180   + caddc 8182  2c2 9355

This proof depends on 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 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-2 9363

This theorem is used by:  2cn  9375  3re  9378  2ne0  9396  2ap0  9397  3pos  9398  2lt3  9475  1lt3  9476  2lt4  9478  1lt4  9479  2lt5  9482  2lt6  9487  1lt6  9488  2lt7  9493  1lt7  9494  2lt8  9500  1lt8  9501  2lt9  9508  1lt9  9509  1ap2  9512  1le2  9513  2rene0  9515  halfre  9518  halfgt0  9520  halflt1  9522  rehalfcl  9532  halfpos2  9535  halfnneg2  9537  addltmul  9542  nominpos  9543  avglt1  9544  avglt2  9545  div4p1lem1div2  9559  nn0lele2xi  9614  nn0ge2m1nn  9627  halfnz  9742  3halfnz  9743  2lt10  9914  1lt10  9915  uzuzle23  9962  uzuzle24  9963  eluz4eluz2  9968  uz3m2nn  9973  2rp  10059  xleaddadd  10289  fztpval  10490  fz0to4untppr  10531  fzo0to42pr  10638  qbtwnrelemcalc  10690  qbtwnre  10691  2tnp1ge0ge0  10736  flhalf  10737  fldiv4p1lem1div2  10740  mulp1mod1  10802  expubnd  11033  nn0opthlem2d  11159  faclbnd2  11180  4bc2eq6  11213  hashtpglem  11298  wrdlenge2n0  11340  sq01  11660  cvg1nlemres  11751  resqrexlemover  11776  resqrexlemga  11789  sqrt4  11813  sqrt2gt1lt2  11815  abstri  11870  amgm2  11884  maxabslemlub  11973  maxltsup  11984  bdtrilem  12005  efcllemp  12425  efcllem  12426  ege2le3  12438  ef01bndlem  12523  cos01bnd  12525  cos2bnd  12527  cos01gt0  12530  sin02gt0  12531  sincos2sgn  12533  sin4lt0  12534  cos12dec  12535  eirraplem  12544  egt2lt3  12547  epos  12548  ene1  12552  eap1  12553  oexpneg  12644  oddge22np1  12648  evennn02n  12649  evennn2n  12650  nn0ehalf  12670  nno  12673  nn0o  12674  nn0oddm1d2  12676  nnoddm1d2  12677  flodddiv4t2lthalf  12706  bitsp1o  12720  bitsfzolem  12721  bitsfzo  12722  bitsfi  12724  6gcd4e2  12772  ncoprmgcdne1b  12867  prmdc  12908  3lcm2e6  12938  sqrt2irrlem  12939  sqrt2re  12941  sqrt2irraplemnn  12957  sqrt2irrap  12958  4sqlem11  13180  4sqlem12  13181  2expltfac  13218  ballotfilem2  13228  plusgndxnmulrndx  13487  starvndxnplusgndx  13497  scandxnplusgndx  13509  vscandxnplusgndx  13514  ipndxnplusgndx  13527  tsetndxnplusgndx  13546  plendxnplusgndx  13560  dsndxnplusgndx  13575  slotsdifunifndx  13586  bl2in  15504  hoverb  15749  ivthdichlem  15752  reeff1o  15874  cosz12  15881  sin0pilem1  15882  sin0pilem2  15883  pilem3  15884  pipos  15889  sinhalfpilem  15892  sincosq1lem  15926  sincosq4sgn  15930  sinq12gt0  15931  cosq23lt0  15934  coseq00topi  15936  coseq0negpitopi  15937  tangtx  15939  sincos4thpi  15941  tan4thpi  15942  sincos6thpi  15943  cosordlem  15950  cosq34lt1  15951  cos02pilt1  15952  cos0pilt1  15953  2logb9irr  16073  2logb3irr  16075  2logb9irrALT  16076  sqrt2cxp2logb9e3  16077  2logb9irrap  16079  log2tlbndlog2  16082  log2ublem2  16084  log2ublog2  16086  pellexlem2  16092  mersenne  16111  perfectlem1  16113  perfectlem2  16114  lgslem1  16119  lgsdirprm  16153  gausslemma2dlem0c  16170  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem3  16182  gausslemma2dlem4  16183  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1a1  16205  2lgslem1a2  16206  2lgslem1c  16209  2lgslem4  16222  usgrexmpldifpr  16490  clwwlkext2edg  16663  konigsbergiedgwen  16725  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberg  16734  ex-fl  16739  taupi  17123