Theorem remulcld 7796

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

Syntax hints:   → wi 4   ∈ wcel 1480  (class class class)co 5774  ℝcr 7619   · cmul 7625

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

This theorem is referenced by:  rimul  8347  ltmul1a  8353  ltmul1  8354  lemul1  8355  reapmul1lem  8356  reapmul1  8357  remulext1  8361  mulext1  8374  recexaplem2  8413  redivclap  8491  prodgt0gt0  8609  prodgt0  8610  prodge0  8612  lemul1a  8616  ltmuldiv  8632  ledivmul  8635  lt2mul2div  8637  lemuldiv  8639  lt2msq1  8643  lt2msq  8644  ltdiv23  8650  lediv23  8651  le2msq  8659  msq11  8660  div4p1lem1div2  8973  mul2lt0rlt0  9546  lincmb01cmp  9786  iccf1o  9787  qbtwnrelemcalc  10033  qbtwnre  10034  flhalf  10075  modqval  10097  modqge0  10105  modqmulnn  10115  bernneq  10412  bernneq3  10414  expnbnd  10415  nn0opthlem2d  10467  faclbnd  10487  faclbnd6  10490  remullem  10643  cvg1nlemres  10757  resqrexlemover  10782  resqrexlemnm  10790  resqrexlemglsq  10794  sqrtmul  10807  abstri  10876  maxabslemlub  10979  maxltsup  10990  bdtrilem  11010  mulcn2  11081  reccn2ap  11082  cvgratnnlembern  11292  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemabsle  11296  cvgratnnlemfm  11298  cvgratnnlemrate  11299  mertenslemi1  11304  efcllem  11365  ege2le3  11377  eftlub  11396  sin02gt0  11470  cos12dec  11474  eirraplem  11483  dvdslelemd  11541  divalglemnqt  11617  oddennn  11905  metss2lem  12666  dveflem  12855  sin0pilem1  12862  sin0pilem2  12863  tangtx  12919  trilpolemclim  13229  trilpolemcl  13230  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234