Theorem remulcld 8103

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

Syntax hints:   → wi 4   ∈ wcel 2176  (class class class)co 5944  ℝcr 7924   · cmul 7930

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

This theorem is referenced by:  rimul  8658  ltmul1a  8664  ltmul1  8665  lemul1  8666  reapmul1lem  8667  reapmul1  8668  remulext1  8672  mulext1  8685  recexaplem2  8725  redivclap  8804  prodgt0gt0  8924  prodgt0  8925  prodge0  8927  lemul1a  8931  ltmuldiv  8947  ledivmul  8950  lt2mul2div  8952  lemuldiv  8954  lt2msq1  8958  lt2msq  8959  ltdiv23  8965  lediv23  8966  le2msq  8974  msq11  8975  div4p1lem1div2  9291  mul2lt0rlt0  9881  lincmb01cmp  10125  iccf1o  10126  qbtwnrelemcalc  10398  qbtwnre  10399  flhalf  10445  modqval  10469  modqge0  10477  modqmulnn  10487  bernneq  10805  bernneq3  10807  expnbnd  10808  nn0opthlem2d  10866  faclbnd  10886  faclbnd6  10889  remullem  11182  cvg1nlemres  11296  resqrexlemover  11321  resqrexlemnm  11329  resqrexlemglsq  11333  sqrtmul  11346  abstri  11415  maxabslemlub  11518  maxltsup  11529  bdtrilem  11550  mulcn2  11623  reccn2ap  11624  cvgratnnlembern  11834  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratnnlemabsle  11838  cvgratnnlemfm  11840  cvgratnnlemrate  11841  mertenslemi1  11846  fprodge1  11950  efcllem  11970  ege2le3  11982  eftlub  12001  sin02gt0  12075  cos12dec  12079  eirraplem  12088  dvdslelemd  12154  divalglemnqt  12231  bitsp1o  12264  2expltfac  12762  oddennn  12763  metss2lem  14969  dveflem  15198  sin0pilem1  15253  sin0pilem2  15254  tangtx  15310  logdivlti  15353  rpcxpcl  15375  cxpmul  15384  cxplt  15388  rpcxple2  15390  rpcxplt2  15391  apcxp2  15411  rpabscxpbnd  15412  perfectlem2  15472  lgsdilem  15504  gausslemma2dlem0c  15528  gausslemma2dlem2  15539  gausslemma2dlem3  15540  lgsquadlem1  15554  lgsquadlem2  15555  trilpolemclim  15975  trilpolemcl  15976  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  nconstwlpolemgt0  16003