Theorem remulcld 8006

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

Syntax hints:   → wi 4   ∈ wcel 2160  (class class class)co 5891  ℝcr 7828   · cmul 7834

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

This theorem is referenced by:  rimul  8560  ltmul1a  8566  ltmul1  8567  lemul1  8568  reapmul1lem  8569  reapmul1  8570  remulext1  8574  mulext1  8587  recexaplem2  8627  redivclap  8706  prodgt0gt0  8826  prodgt0  8827  prodge0  8829  lemul1a  8833  ltmuldiv  8849  ledivmul  8852  lt2mul2div  8854  lemuldiv  8856  lt2msq1  8860  lt2msq  8861  ltdiv23  8867  lediv23  8868  le2msq  8876  msq11  8877  div4p1lem1div2  9190  mul2lt0rlt0  9777  lincmb01cmp  10021  iccf1o  10022  qbtwnrelemcalc  10274  qbtwnre  10275  flhalf  10320  modqval  10342  modqge0  10350  modqmulnn  10360  bernneq  10659  bernneq3  10661  expnbnd  10662  nn0opthlem2d  10719  faclbnd  10739  faclbnd6  10742  remullem  10898  cvg1nlemres  11012  resqrexlemover  11037  resqrexlemnm  11045  resqrexlemglsq  11049  sqrtmul  11062  abstri  11131  maxabslemlub  11234  maxltsup  11245  bdtrilem  11265  mulcn2  11338  reccn2ap  11339  cvgratnnlembern  11549  cvgratnnlemnexp  11550  cvgratnnlemmn  11551  cvgratnnlemabsle  11553  cvgratnnlemfm  11555  cvgratnnlemrate  11556  mertenslemi1  11561  fprodge1  11665  efcllem  11685  ege2le3  11697  eftlub  11716  sin02gt0  11789  cos12dec  11793  eirraplem  11802  dvdslelemd  11867  divalglemnqt  11943  oddennn  12411  metss2lem  14394  dveflem  14584  sin0pilem1  14599  sin0pilem2  14600  tangtx  14656  logdivlti  14699  rpcxpcl  14721  cxpmul  14730  cxplt  14733  rpcxple2  14735  rpcxplt2  14736  apcxp2  14755  rpabscxpbnd  14756  lgsdilem  14825  trilpolemclim  15182  trilpolemcl  15183  trilpolemisumle  15184  trilpolemeq1  15186  trilpolemlt1  15187  nconstwlpolemgt0  15210