Theorem remulcld 7114

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

Syntax hints:   → wi 4   ∈ wcel 1409  (class class class)co 5539  ℝcr 6945   · cmul 6951

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

This theorem is referenced by:  rimul  7649  ltmul1a  7655  ltmul1  7656  lemul1  7657  reapmul1lem  7658  reapmul1  7659  remulext1  7663  mulext1  7676  recexaplem2  7706  redivclap  7781  prodgt0gt0  7891  prodgt0  7892  prodge0  7894  lemul1a  7898  ltmuldiv  7914  ledivmul  7917  lt2mul2div  7919  lemuldiv  7921  lt2msq1  7925  lt2msq  7926  ltdiv23  7932  lediv23  7933  le2msq  7941  msq11  7942  div4p1lem1div2  8234  lincmb01cmp  8971  iccf1o  8972  qbtwnrelemcalc  9211  qbtwnre  9212  flhalf  9246  modqval  9268  modqge0  9276  modqmulnn  9286  bernneq  9530  bernneq3  9532  expnbnd  9533  nn0opthlem2d  9582  faclbnd  9602  faclbnd6  9605  remullem  9692  cvg1nlemres  9805  resqrexlemover  9829  resqrexlemnm  9837  resqrexlemglsq  9841  sqrtmul  9854  abstri  9923  mulcn2  10056  dvdslelemd  10147