Theorem 2re 9377

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

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  ℝcr 8179  1c1 8181   + caddc 8183  2c2 9358

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 8274  ax-addrcl 8277

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

This theorem is used by:  2cn  9378  3re  9381  2ne0  9399  2ap0  9400  3pos  9401  2lt3  9480  1lt3  9481  2lt4  9483  1lt4  9484  2lt5  9487  2lt6  9492  1lt6  9493  2lt7  9498  1lt7  9499  2lt8  9505  1lt8  9506  2lt9  9513  1lt9  9514  1ap2  9517  1le2  9518  2rene0  9520  halfre  9523  halfgt0  9525  halflt1  9527  rehalfcl  9537  halfpos2  9540  halfnneg2  9542  addltmul  9547  nominpos  9548  avglt1  9549  avglt2  9550  div4p1lem1div2  9564  nn0lele2xi  9619  nn0ge2m1nn  9632  halfnz  9747  3halfnz  9748  2lt10  9924  1lt10  9925  uzuzle23  9972  uzuzle24  9973  eluz4eluz2  9978  uz3m2nn  9983  2rp  10070  xleaddadd  10300  fztpval  10501  fz0to4untppr  10542  fzo0to42pr  10649  qbtwnrelemcalc  10701  qbtwnre  10702  2tnp1ge0ge0  10751  flhalf  10752  fldiv4p1lem1div2  10755  mulp1mod1  10817  expubnd  11048  nn0opthlem2d  11175  faclbnd2  11196  4bc2eq6  11229  hashtpglem  11314  wrdlenge2n0  11356  sq01  11676  cvg1nlemres  11767  resqrexlemover  11792  resqrexlemga  11805  sqrt4  11829  sqrt2gt1lt2  11831  abstri  11887  amgm2  11901  maxabslemlub  11990  maxltsup  12001  bdtrilem  12024  efcllemp  12444  efcllem  12445  ege2le3  12457  ef01bndlem  12542  cos01bnd  12544  cos2bnd  12546  cos01gt0  12549  sin02gt0  12550  sincos2sgn  12552  sin4lt0  12553  cos12dec  12554  eirraplem  12563  egt2lt3  12566  epos  12567  ene1  12571  eap1  12572  oexpneg  12663  oddge22np1  12667  evennn02n  12668  evennn2n  12669  nn0ehalf  12689  nno  12692  nn0o  12693  nn0oddm1d2  12695  nnoddm1d2  12696  flodddiv4t2lthalf  12725  bitsp1o  12739  bitsfzolem  12740  bitsfzo  12741  bitsfi  12743  6gcd4e2  12791  ncoprmgcdne1b  12886  prmdc  12927  3lcm2e6  12958  sqrt2irrlem  12959  sqrt2re  12961  sqrt2irraplemnn  12978  sqrt2irrap  12979  4sqlem11  13203  4sqlem12  13204  2expltfac  13242  ballotfilem2  13280  plusgndxnmulrndx  13540  starvndxnplusgndx  13550  scandxnplusgndx  13562  vscandxnplusgndx  13567  ipndxnplusgndx  13580  tsetndxnplusgndx  13599  plendxnplusgndx  13613  dsndxnplusgndx  13628  slotsdifunifndx  13639  bl2in  15595  hoverb  15840  ivthdichlem  15843  reeff1o  15965  cosz12  15973  sin0pilem1  15974  sin0pilem2  15975  pilem3  15976  pipos  15981  sinhalfpilem  15984  sincosq1lem  16018  sincosq4sgn  16022  sinq12gt0  16023  cosq23lt0  16026  coseq00topi  16028  coseq0negpitopi  16029  tangtx  16031  sincos4thpi  16033  tan4thpi  16034  sincos6thpi  16035  cosordlem  16042  cosq34lt1  16043  cos02pilt1  16044  cos0pilt1  16045  logdivlt  16088  2logb9irr  16168  2logb3irr  16170  2logb9irrALT  16171  sqrt2cxp2logb9e3  16172  2logb9irrap  16174  log2tlbndlog2  16181  log2ublem2  16183  log2ublog2  16185  pellexlem2  16191  ppiqfi  16203  chtdif  16225  ppidif  16230  chtqrpcl  16240  ppiqeq0  16241  ppiqub  16254  chtublem  16256  chtqub  16257  mersenne  16258  perfectlem1  16260  perfectlem2  16261  bcmono  16265  bclbnd  16268  bpos1lem  16270  bposlem1  16272  bposlem2  16273  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgslem1  16285  lgsdirprm  16319  gausslemma2dlem0c  16336  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem3  16348  gausslemma2dlem4  16349  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1a1  16371  2lgslem1a2  16372  2lgslem1c  16375  2lgslem4  16388  usgrexmpldifpr  16656  clwwlkext2edg  16829  konigsbergiedgwen  16891  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberg  16900  ex-fl  16905  taupi  17290