Theorem remulcld 8076

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

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

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

This theorem is referenced by:  rimul  8631  ltmul1a  8637  ltmul1  8638  lemul1  8639  reapmul1lem  8640  reapmul1  8641  remulext1  8645  mulext1  8658  recexaplem2  8698  redivclap  8777  prodgt0gt0  8897  prodgt0  8898  prodge0  8900  lemul1a  8904  ltmuldiv  8920  ledivmul  8923  lt2mul2div  8925  lemuldiv  8927  lt2msq1  8931  lt2msq  8932  ltdiv23  8938  lediv23  8939  le2msq  8947  msq11  8948  div4p1lem1div2  9264  mul2lt0rlt0  9853  lincmb01cmp  10097  iccf1o  10098  qbtwnrelemcalc  10364  qbtwnre  10365  flhalf  10411  modqval  10435  modqge0  10443  modqmulnn  10453  bernneq  10771  bernneq3  10773  expnbnd  10774  nn0opthlem2d  10832  faclbnd  10852  faclbnd6  10855  remullem  11055  cvg1nlemres  11169  resqrexlemover  11194  resqrexlemnm  11202  resqrexlemglsq  11206  sqrtmul  11219  abstri  11288  maxabslemlub  11391  maxltsup  11402  bdtrilem  11423  mulcn2  11496  reccn2ap  11497  cvgratnnlembern  11707  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemabsle  11711  cvgratnnlemfm  11713  cvgratnnlemrate  11714  mertenslemi1  11719  fprodge1  11823  efcllem  11843  ege2le3  11855  eftlub  11874  sin02gt0  11948  cos12dec  11952  eirraplem  11961  dvdslelemd  12027  divalglemnqt  12104  bitsp1o  12137  2expltfac  12635  oddennn  12636  metss2lem  14841  dveflem  15070  sin0pilem1  15125  sin0pilem2  15126  tangtx  15182  logdivlti  15225  rpcxpcl  15247  cxpmul  15256  cxplt  15260  rpcxple2  15262  rpcxplt2  15263  apcxp2  15283  rpabscxpbnd  15284  perfectlem2  15344  lgsdilem  15376  gausslemma2dlem0c  15400  gausslemma2dlem2  15411  gausslemma2dlem3  15412  lgsquadlem1  15426  lgsquadlem2  15427  trilpolemclim  15793  trilpolemcl  15794  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  nconstwlpolemgt0  15821