Theorem 2re 9324

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 9313	. 2 ⊢ 2 = (1 + 1)
2		1re 8289	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8303	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2307	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2205  (class class class)co 6058  ℝcr 8142  1c1 8144   + caddc 8146  2c2 9305

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230  df-2 9313

This theorem is referenced by:  2cn  9325  3re  9328  2ne0  9346  2ap0  9347  3pos  9348  2lt3  9425  1lt3  9426  2lt4  9428  1lt4  9429  2lt5  9432  2lt6  9437  1lt6  9438  2lt7  9443  1lt7  9444  2lt8  9450  1lt8  9451  2lt9  9458  1lt9  9459  1ap2  9462  1le2  9463  2rene0  9465  halfre  9468  halfgt0  9470  halflt1  9472  rehalfcl  9482  halfpos2  9485  halfnneg2  9487  addltmul  9492  nominpos  9493  avglt1  9494  avglt2  9495  div4p1lem1div2  9509  nn0lele2xi  9564  nn0ge2m1nn  9577  halfnz  9692  3halfnz  9693  2lt10  9864  1lt10  9865  uzuzle23  9912  uzuzle24  9913  eluz4eluz2  9918  uz3m2nn  9923  2rp  10009  xleaddadd  10239  fztpval  10439  fz0to4untppr  10480  fzo0to42pr  10587  qbtwnrelemcalc  10639  qbtwnre  10640  2tnp1ge0ge0  10685  flhalf  10686  fldiv4p1lem1div2  10689  mulp1mod1  10751  expubnd  10982  nn0opthlem2d  11108  faclbnd2  11129  4bc2eq6  11162  hashtpglem  11243  wrdlenge2n0  11285  cvg1nlemres  11695  resqrexlemover  11720  resqrexlemga  11733  sqrt4  11757  sqrt2gt1lt2  11759  abstri  11814  amgm2  11828  maxabslemlub  11917  maxltsup  11928  bdtrilem  11949  efcllemp  12369  efcllem  12370  ege2le3  12382  ef01bndlem  12467  cos01bnd  12469  cos2bnd  12471  cos01gt0  12474  sin02gt0  12475  sincos2sgn  12477  sin4lt0  12478  cos12dec  12479  eirraplem  12488  egt2lt3  12491  epos  12492  ene1  12496  eap1  12497  oexpneg  12588  oddge22np1  12592  evennn02n  12593  evennn2n  12594  nn0ehalf  12614  nno  12617  nn0o  12618  nn0oddm1d2  12620  nnoddm1d2  12621  flodddiv4t2lthalf  12650  bitsp1o  12664  bitsfzolem  12665  bitsfzo  12666  bitsfi  12668  6gcd4e2  12716  ncoprmgcdne1b  12811  prmdc  12852  3lcm2e6  12882  sqrt2irrlem  12883  sqrt2re  12885  sqrt2irraplemnn  12901  sqrt2irrap  12902  4sqlem11  13124  4sqlem12  13125  2expltfac  13162  ballotfilem2  13172  plusgndxnmulrndx  13430  starvndxnplusgndx  13440  scandxnplusgndx  13452  vscandxnplusgndx  13457  ipndxnplusgndx  13470  tsetndxnplusgndx  13489  plendxnplusgndx  13503  dsndxnplusgndx  13518  slotsdifunifndx  13529  bl2in  15394  hoverb  15639  ivthdichlem  15642  reeff1o  15764  cosz12  15771  sin0pilem1  15772  sin0pilem2  15773  pilem3  15774  pipos  15779  sinhalfpilem  15782  sincosq1lem  15816  sincosq4sgn  15820  sinq12gt0  15821  cosq23lt0  15824  coseq00topi  15826  coseq0negpitopi  15827  tangtx  15829  sincos4thpi  15831  tan4thpi  15832  sincos6thpi  15833  cosordlem  15840  cosq34lt1  15841  cos02pilt1  15842  cos0pilt1  15843  2logb9irr  15962  2logb3irr  15964  2logb9irrALT  15965  sqrt2cxp2logb9e3  15966  2logb9irrap  15968  pellexlem2  15972  mersenne  15991  perfectlem1  15993  perfectlem2  15994  lgslem1  15999  lgsdirprm  16033  gausslemma2dlem0c  16050  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  gausslemma2dlem3  16062  gausslemma2dlem4  16063  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1a1  16085  2lgslem1a2  16086  2lgslem1c  16089  2lgslem4  16102  usgrexmpldifpr  16370  clwwlkext2edg  16543  konigsbergiedgwen  16605  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberg  16614  ex-fl  16619  taupi  16985