Theorem remulcld 8074

Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
readdcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
remulcld	⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

Proof of Theorem remulcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		remulcl 8024	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2167  (class class class)co 5925  ℝcr 7895   · cmul 7901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 7995

This theorem is referenced by:  rimul  8629  ltmul1a  8635  ltmul1  8636  lemul1  8637  reapmul1lem  8638  reapmul1  8639  remulext1  8643  mulext1  8656  recexaplem2  8696  redivclap  8775  prodgt0gt0  8895  prodgt0  8896  prodge0  8898  lemul1a  8902  ltmuldiv  8918  ledivmul  8921  lt2mul2div  8923  lemuldiv  8925  lt2msq1  8929  lt2msq  8930  ltdiv23  8936  lediv23  8937  le2msq  8945  msq11  8946  div4p1lem1div2  9262  mul2lt0rlt0  9851  lincmb01cmp  10095  iccf1o  10096  qbtwnrelemcalc  10362  qbtwnre  10363  flhalf  10409  modqval  10433  modqge0  10441  modqmulnn  10451  bernneq  10769  bernneq3  10771  expnbnd  10772  nn0opthlem2d  10830  faclbnd  10850  faclbnd6  10853  remullem  11053  cvg1nlemres  11167  resqrexlemover  11192  resqrexlemnm  11200  resqrexlemglsq  11204  sqrtmul  11217  abstri  11286  maxabslemlub  11389  maxltsup  11400  bdtrilem  11421  mulcn2  11494  reccn2ap  11495  cvgratnnlembern  11705  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemabsle  11709  cvgratnnlemfm  11711  cvgratnnlemrate  11712  mertenslemi1  11717  fprodge1  11821  efcllem  11841  ege2le3  11853  eftlub  11872  sin02gt0  11946  cos12dec  11950  eirraplem  11959  dvdslelemd  12025  divalglemnqt  12102  bitsp1o  12135  2expltfac  12633  oddennn  12634  metss2lem  14817  dveflem  15046  sin0pilem1  15101  sin0pilem2  15102  tangtx  15158  logdivlti  15201  rpcxpcl  15223  cxpmul  15232  cxplt  15236  rpcxple2  15238  rpcxplt2  15239  apcxp2  15259  rpabscxpbnd  15260  perfectlem2  15320  lgsdilem  15352  gausslemma2dlem0c  15376  gausslemma2dlem2  15387  gausslemma2dlem3  15388  lgsquadlem1  15402  lgsquadlem2  15403  trilpolemclim  15767  trilpolemcl  15768  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  nconstwlpolemgt0  15795