Theorem 2re 9383

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

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6088  ℝcr 8184  1c1 8186   + caddc 8188  2c2 9364

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 8279  ax-addrcl 8282

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

This theorem is used by:  2cn  9384  3re  9387  2ne0  9405  2ap0  9406  3pos  9407  2lt3  9486  1lt3  9487  2lt4  9489  1lt4  9490  2lt5  9493  2lt6  9498  1lt6  9499  2lt7  9504  1lt7  9505  2lt8  9511  1lt8  9512  2lt9  9519  1lt9  9520  1ap2  9523  1le2  9524  2rene0  9526  halfre  9529  halfgt0  9531  halflt1  9533  rehalfcl  9543  halfpos2  9546  halfnneg2  9548  addltmul  9553  nominpos  9554  avglt1  9555  avglt2  9556  div4p1lem1div2  9570  nn0lele2xi  9625  nn0ge2m1nn  9636  halfnz  9752  3halfnz  9753  2lt10  9929  1lt10  9930  uzuzle23  9977  uzuzle24  9978  eluz4eluz2  9983  uz3m2nn  9988  2rp  10075  xleaddadd  10305  fztpval  10506  fz0to4untppr  10547  fzo0to42pr  10654  qbtwnrelemcalc  10706  qbtwnre  10707  2tnp1ge0ge0  10756  flhalf  10757  fldiv4p1lem1div2  10760  mulp1mod1  10822  expubnd  11053  nn0opthlem2d  11180  faclbnd2  11201  4bc2eq6  11234  hashtpglem  11319  wrdlenge2n0  11361  sq01  11681  cvg1nlemres  11772  resqrexlemover  11797  resqrexlemga  11810  sqrt4  11834  sqrt2gt1lt2  11836  abstri  11892  amgm2  11906  maxabslemlub  11995  maxltsup  12006  bdtrilem  12029  efcllemp  12449  efcllem  12450  ege2le3  12462  ef01bndlem  12547  cos01bnd  12549  cos2bnd  12551  cos01gt0  12554  sin02gt0  12555  sincos2sgn  12557  sin4lt0  12558  cos12dec  12559  eirraplem  12568  egt2lt3  12571  epos  12572  ene1  12576  eap1  12577  oexpneg  12668  oddge22np1  12672  evennn02n  12673  evennn2n  12674  nn0ehalf  12694  nno  12697  nn0o  12698  nn0oddm1d2  12700  nnoddm1d2  12701  flodddiv4t2lthalf  12730  bitsp1o  12744  bitsfzolem  12745  bitsfzo  12746  bitsfi  12748  6gcd4e2  12796  ncoprmgcdne1b  12891  prmdc  12932  3lcm2e6  12963  sqrt2irrlem  12964  sqrt2re  12966  sqrt2irraplemnn  12983  sqrt2irrap  12984  4sqlem11  13208  4sqlem12  13209  2expltfac  13247  ballotfilem2  13285  plusgndxnmulrndx  13545  starvndxnplusgndx  13555  scandxnplusgndx  13567  vscandxnplusgndx  13572  ipndxnplusgndx  13585  tsetndxnplusgndx  13604  plendxnplusgndx  13618  dsndxnplusgndx  13633  slotsdifunifndx  13644  bl2in  15646  hoverb  15891  ivthdichlem  15894  reeff1o  16016  cosz12  16024  sin0pilem1  16025  sin0pilem2  16026  pilem3  16027  pipos  16032  sinhalfpilem  16035  sincosq1lem  16069  sincosq4sgn  16073  sinq12gt0  16074  cosq23lt0  16077  coseq00topi  16079  coseq0negpitopi  16080  tangtx  16082  sincos4thpi  16084  tan4thpi  16085  sincos6thpi  16086  sineq0re  16093  cosordlem  16094  cosq34lt1  16095  cos02pilt1  16096  cos0pilt1  16097  logdivlt  16141  2logb9irr  16224  2logb3irr  16226  2logb9irrALT  16227  sqrt2cxp2logb9e3  16228  2logb9irrap  16230  log2tlbndlog2  16237  log2ublem2  16239  log2ublog2  16241  pellexlem2  16247  ppiqfi  16259  chtdif  16281  ppidif  16286  chtqrpcl  16296  ppiqeq0  16297  ppiqub  16310  chtublem  16312  chtqub  16313  mersenne  16314  perfectlem1  16316  perfectlem2  16317  bcmono  16321  bclbnd  16324  bpos1lem  16326  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgslem1  16341  lgsdirprm  16375  gausslemma2dlem0c  16392  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  gausslemma2dlem3  16404  gausslemma2dlem4  16405  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  2lgslem1a1  16427  2lgslem1a2  16428  2lgslem1c  16431  2lgslem4  16444  usgrexmpldifpr  16712  clwwlkext2edg  16885  konigsbergiedgwen  16947  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberg  16956  ex-fl  16961  taupi  17347