Theorem remulcld 7263

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

Syntax hints:   → wi 4   ∈ wcel 1434  (class class class)co 5563  ℝcr 7094   · cmul 7100

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

This theorem is referenced by:  rimul  7804  ltmul1a  7810  ltmul1  7811  lemul1  7812  reapmul1lem  7813  reapmul1  7814  remulext1  7818  mulext1  7831  recexaplem2  7861  redivclap  7938  prodgt0gt0  8048  prodgt0  8049  prodge0  8051  lemul1a  8055  ltmuldiv  8071  ledivmul  8074  lt2mul2div  8076  lemuldiv  8078  lt2msq1  8082  lt2msq  8083  ltdiv23  8089  lediv23  8090  le2msq  8098  msq11  8099  div4p1lem1div2  8403  lincmb01cmp  9153  iccf1o  9154  qbtwnrelemcalc  9394  qbtwnre  9395  flhalf  9436  modqval  9458  modqge0  9466  modqmulnn  9476  bernneq  9742  bernneq3  9744  expnbnd  9745  nn0opthlem2d  9797  faclbnd  9817  faclbnd6  9820  remullem  9959  cvg1nlemres  10072  resqrexlemover  10097  resqrexlemnm  10105  resqrexlemglsq  10109  sqrtmul  10122  abstri  10191  maxabslemlub  10294  maxltsup  10305  mulcn2  10352  dvdslelemd  10451  divalglemnqt  10527  oddennn  10812