Theorem remulcld 8177

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6001  ℝcr 7998   · cmul 8004

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

This theorem is referenced by:  rimul  8732  ltmul1a  8738  ltmul1  8739  lemul1  8740  reapmul1lem  8741  reapmul1  8742  remulext1  8746  mulext1  8759  recexaplem2  8799  redivclap  8878  prodgt0gt0  8998  prodgt0  8999  prodge0  9001  lemul1a  9005  ltmuldiv  9021  ledivmul  9024  lt2mul2div  9026  lemuldiv  9028  lt2msq1  9032  lt2msq  9033  ltdiv23  9039  lediv23  9040  le2msq  9048  msq11  9049  div4p1lem1div2  9365  mul2lt0rlt0  9955  lincmb01cmp  10199  iccf1o  10200  qbtwnrelemcalc  10475  qbtwnre  10476  flhalf  10522  modqval  10546  modqge0  10554  modqmulnn  10564  bernneq  10882  bernneq3  10884  expnbnd  10885  nn0opthlem2d  10943  faclbnd  10963  faclbnd6  10966  remullem  11382  cvg1nlemres  11496  resqrexlemover  11521  resqrexlemnm  11529  resqrexlemglsq  11533  sqrtmul  11546  abstri  11615  maxabslemlub  11718  maxltsup  11729  bdtrilem  11750  mulcn2  11823  reccn2ap  11824  cvgratnnlembern  12034  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemabsle  12038  cvgratnnlemfm  12040  cvgratnnlemrate  12041  mertenslemi1  12046  fprodge1  12150  efcllem  12170  ege2le3  12182  eftlub  12201  sin02gt0  12275  cos12dec  12279  eirraplem  12288  dvdslelemd  12354  divalglemnqt  12431  bitsp1o  12464  2expltfac  12962  oddennn  12963  metss2lem  15171  dveflem  15400  sin0pilem1  15455  sin0pilem2  15456  tangtx  15512  logdivlti  15555  rpcxpcl  15577  cxpmul  15586  cxplt  15590  rpcxple2  15592  rpcxplt2  15593  apcxp2  15613  rpabscxpbnd  15614  perfectlem2  15674  lgsdilem  15706  gausslemma2dlem0c  15730  gausslemma2dlem2  15741  gausslemma2dlem3  15742  lgsquadlem1  15756  lgsquadlem2  15757  trilpolemclim  16404  trilpolemcl  16405  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  nconstwlpolemgt0  16432