Theorem 2re 9307

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 9296	. 2 ⊢ 2 = (1 + 1)
2		1re 8273	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8287	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2305	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2203  (class class class)co 6050  ℝcr 8126  1c1 8128   + caddc 8130  2c2 9288

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 2214  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-2 9296

This theorem is referenced by:  2cn  9308  3re  9311  2ne0  9329  2ap0  9330  3pos  9331  2lt3  9408  1lt3  9409  2lt4  9411  1lt4  9412  2lt5  9415  2lt6  9420  1lt6  9421  2lt7  9426  1lt7  9427  2lt8  9433  1lt8  9434  2lt9  9441  1lt9  9442  1ap2  9445  1le2  9446  2rene0  9448  halfre  9451  halfgt0  9453  halflt1  9455  rehalfcl  9465  halfpos2  9468  halfnneg2  9470  addltmul  9475  nominpos  9476  avglt1  9477  avglt2  9478  div4p1lem1div2  9492  nn0lele2xi  9547  nn0ge2m1nn  9560  halfnz  9674  3halfnz  9675  2lt10  9846  1lt10  9847  uzuzle23  9894  uzuzle24  9895  eluz4eluz2  9900  uz3m2nn  9905  2rp  9991  xleaddadd  10220  fztpval  10417  fz0to4untppr  10458  fzo0to42pr  10565  qbtwnrelemcalc  10615  qbtwnre  10616  2tnp1ge0ge0  10661  flhalf  10662  fldiv4p1lem1div2  10665  mulp1mod1  10727  expubnd  10958  nn0opthlem2d  11083  faclbnd2  11104  4bc2eq6  11137  hashtpglem  11218  wrdlenge2n0  11260  cvg1nlemres  11670  resqrexlemover  11695  resqrexlemga  11708  sqrt4  11732  sqrt2gt1lt2  11734  abstri  11789  amgm2  11803  maxabslemlub  11892  maxltsup  11903  bdtrilem  11924  efcllemp  12344  efcllem  12345  ege2le3  12357  ef01bndlem  12442  cos01bnd  12444  cos2bnd  12446  cos01gt0  12449  sin02gt0  12450  sincos2sgn  12452  sin4lt0  12453  cos12dec  12454  eirraplem  12463  egt2lt3  12466  epos  12467  ene1  12471  eap1  12472  oexpneg  12563  oddge22np1  12567  evennn02n  12568  evennn2n  12569  nn0ehalf  12589  nno  12592  nn0o  12593  nn0oddm1d2  12595  nnoddm1d2  12596  flodddiv4t2lthalf  12625  bitsp1o  12639  bitsfzolem  12640  bitsfzo  12641  bitsfi  12643  6gcd4e2  12691  ncoprmgcdne1b  12786  prmdc  12827  3lcm2e6  12857  sqrt2irrlem  12858  sqrt2re  12860  sqrt2irraplemnn  12876  sqrt2irrap  12877  4sqlem11  13099  4sqlem12  13100  2expltfac  13137  ballotfilem2  13142  plusgndxnmulrndx  13346  starvndxnplusgndx  13356  scandxnplusgndx  13368  vscandxnplusgndx  13373  ipndxnplusgndx  13386  tsetndxnplusgndx  13405  plendxnplusgndx  13419  dsndxnplusgndx  13434  slotsdifunifndx  13445  bl2in  15268  hoverb  15513  ivthdichlem  15516  reeff1o  15638  cosz12  15645  sin0pilem1  15646  sin0pilem2  15647  pilem3  15648  pipos  15653  sinhalfpilem  15656  sincosq1lem  15690  sincosq4sgn  15694  sinq12gt0  15695  cosq23lt0  15698  coseq00topi  15700  coseq0negpitopi  15701  tangtx  15703  sincos4thpi  15705  tan4thpi  15706  sincos6thpi  15707  cosordlem  15714  cosq34lt1  15715  cos02pilt1  15716  cos0pilt1  15717  2logb9irr  15836  2logb3irr  15838  2logb9irrALT  15839  sqrt2cxp2logb9e3  15840  2logb9irrap  15842  pellexlem2  15846  mersenne  15865  perfectlem1  15867  perfectlem2  15868  lgslem1  15873  lgsdirprm  15907  gausslemma2dlem0c  15924  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem3  15936  gausslemma2dlem4  15937  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem1a1  15959  2lgslem1a2  15960  2lgslem1c  15963  2lgslem4  15976  usgrexmpldifpr  16244  clwwlkext2edg  16417  konigsbergiedgwen  16479  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberg  16488  ex-fl  16493  taupi  16859