Theorem 2re 9255

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 9244	. 2 ⊢ 2 = (1 + 1)
2		1re 8221	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8235	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2304	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6028  ℝcr 8074  1c1 8076   + caddc 8078  2c2 9236

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 2213  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9244

This theorem is referenced by:  2cn  9256  3re  9259  2ne0  9277  2ap0  9278  3pos  9279  2lt3  9356  1lt3  9357  2lt4  9359  1lt4  9360  2lt5  9363  2lt6  9368  1lt6  9369  2lt7  9374  1lt7  9375  2lt8  9381  1lt8  9382  2lt9  9389  1lt9  9390  1ap2  9393  1le2  9394  2rene0  9396  halfre  9399  halfgt0  9401  halflt1  9403  rehalfcl  9413  halfpos2  9416  halfnneg2  9418  addltmul  9423  nominpos  9424  avglt1  9425  avglt2  9426  div4p1lem1div2  9440  nn0lele2xi  9495  nn0ge2m1nn  9506  halfnz  9620  3halfnz  9621  2lt10  9792  1lt10  9793  uzuzle23  9840  uzuzle24  9841  eluz4eluz2  9846  uz3m2nn  9851  2rp  9937  xleaddadd  10166  fztpval  10363  fz0to4untppr  10404  fzo0to42pr  10511  qbtwnrelemcalc  10561  qbtwnre  10562  2tnp1ge0ge0  10607  flhalf  10608  fldiv4p1lem1div2  10611  mulp1mod1  10673  expubnd  10904  nn0opthlem2d  11029  faclbnd2  11050  4bc2eq6  11082  hashtpglem  11156  wrdlenge2n0  11198  cvg1nlemres  11608  resqrexlemover  11633  resqrexlemga  11646  sqrt4  11670  sqrt2gt1lt2  11672  abstri  11727  amgm2  11741  maxabslemlub  11830  maxltsup  11841  bdtrilem  11862  efcllemp  12282  efcllem  12283  ege2le3  12295  ef01bndlem  12380  cos01bnd  12382  cos2bnd  12384  cos01gt0  12387  sin02gt0  12388  sincos2sgn  12390  sin4lt0  12391  cos12dec  12392  eirraplem  12401  egt2lt3  12404  epos  12405  ene1  12409  eap1  12410  oexpneg  12501  oddge22np1  12505  evennn02n  12506  evennn2n  12507  nn0ehalf  12527  nno  12530  nn0o  12531  nn0oddm1d2  12533  nnoddm1d2  12534  flodddiv4t2lthalf  12563  bitsp1o  12577  bitsfzolem  12578  bitsfzo  12579  bitsfi  12581  6gcd4e2  12629  ncoprmgcdne1b  12724  prmdc  12765  3lcm2e6  12795  sqrt2irrlem  12796  sqrt2re  12798  sqrt2irraplemnn  12814  sqrt2irrap  12815  4sqlem11  13037  4sqlem12  13038  2expltfac  13075  plusgndxnmulrndx  13279  starvndxnplusgndx  13289  scandxnplusgndx  13301  vscandxnplusgndx  13306  ipndxnplusgndx  13319  tsetndxnplusgndx  13338  plendxnplusgndx  13352  dsndxnplusgndx  13367  slotsdifunifndx  13378  bl2in  15197  hoverb  15442  ivthdichlem  15445  reeff1o  15567  cosz12  15574  sin0pilem1  15575  sin0pilem2  15576  pilem3  15577  pipos  15582  sinhalfpilem  15585  sincosq1lem  15619  sincosq4sgn  15623  sinq12gt0  15624  cosq23lt0  15627  coseq00topi  15629  coseq0negpitopi  15630  tangtx  15632  sincos4thpi  15634  tan4thpi  15635  sincos6thpi  15636  cosordlem  15643  cosq34lt1  15644  cos02pilt1  15645  cos0pilt1  15646  2logb9irr  15765  2logb3irr  15767  2logb9irrALT  15768  sqrt2cxp2logb9e3  15769  2logb9irrap  15771  pellexlem2  15775  mersenne  15794  perfectlem1  15796  perfectlem2  15797  lgslem1  15802  lgsdirprm  15836  gausslemma2dlem0c  15853  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem3  15865  gausslemma2dlem4  15866  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisen  15876  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem1a1  15888  2lgslem1a2  15889  2lgslem1c  15892  2lgslem4  15905  usgrexmpldifpr  16173  clwwlkext2edg  16346  konigsbergiedgwen  16408  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberg  16417  ex-fl  16422  taupi  16789