Theorem remulcld 7056

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 7009	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 391	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1393  (class class class)co 5512  ℝcr 6888   · cmul 6894

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

This theorem is referenced by:  rimul  7576  ltmul1a  7582  ltmul1  7583  lemul1  7584  reapmul1lem  7585  reapmul1  7586  remulext1  7590  mulext1  7603  recexaplem2  7633  redivclap  7707  prodgt0gt0  7817  prodgt0  7818  prodge0  7820  lemul1a  7824  ltmuldiv  7840  ledivmul  7843  lt2mul2div  7845  lemuldiv  7847  lt2msq1  7851  lt2msq  7852  ltdiv23  7858  lediv23  7859  le2msq  7867  msq11  7868  div4p1lem1div2  8177  lincmb01cmp  8871  iccf1o  8872  qbtwnrelemcalc  9110  qbtwnre  9111  flhalf  9144  modqval  9166  modqge0  9174  modqmulnn  9184  bernneq  9369  bernneq3  9371  expnbnd  9372  remullem  9471  cvg1nlemres  9584  resqrexlemover  9608  resqrexlemnm  9616  resqrexlemglsq  9620  sqrtmul  9633  abstri  9700  mulcn2  9833