Theorem remulcld 8304

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

Syntax hints:   → wi 4   ∈ wcel 2203  (class class class)co 6050  ℝcr 8126   · cmul 8132

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

This theorem is referenced by:  rimul  8859  ltmul1a  8865  ltmul1  8866  lemul1  8867  reapmul1lem  8868  reapmul1  8869  remulext1  8873  mulext1  8886  recexaplem2  8926  redivclap  9005  prodgt0gt0  9125  prodgt0  9126  prodge0  9128  lemul1a  9132  ltmuldiv  9148  ledivmul  9151  lt2mul2div  9153  lemuldiv  9155  lt2msq1  9159  lt2msq  9160  ltdiv23  9166  lediv23  9167  le2msq  9175  msq11  9176  div4p1lem1div2  9492  mul2lt0rlt0  10092  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  qbtwnrelemcalc  10615  qbtwnre  10616  flhalf  10662  modqval  10686  modqge0  10694  modqmulnn  10704  bernneq  11022  bernneq3  11024  expnbnd  11025  nn0opthlem2d  11083  faclbnd  11103  faclbnd6  11106  remullem  11556  cvg1nlemres  11670  resqrexlemover  11695  resqrexlemnm  11703  resqrexlemglsq  11707  sqrtmul  11720  abstri  11789  maxabslemlub  11892  maxltsup  11903  bdtrilem  11924  mulcn2  11997  reccn2ap  11998  cvgratnnlembern  12209  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratnnlemabsle  12213  cvgratnnlemfm  12215  cvgratnnlemrate  12216  mertenslemi1  12221  fprodge1  12325  efcllem  12345  ege2le3  12357  eftlub  12376  sin02gt0  12450  cos12dec  12454  eirraplem  12463  dvdslelemd  12529  divalglemnqt  12606  bitsp1o  12639  2expltfac  13137  oddennn  13143  metss2lem  15362  dveflem  15591  sin0pilem1  15646  sin0pilem2  15647  tangtx  15703  logdivlti  15746  rpcxpcl  15768  cxpmul  15777  cxplt  15781  rpcxple2  15783  rpcxplt2  15784  apcxp2  15804  rpabscxpbnd  15805  pellexlem2  15846  perfectlem2  15868  lgsdilem  15900  gausslemma2dlem0c  15924  gausslemma2dlem2  15935  gausslemma2dlem3  15936  lgsquadlem1  15950  lgsquadlem2  15951  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  nconstwlpolemgt0  16850