Theorem remulcld 7891

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

Syntax hints:   → wi 4   ∈ wcel 2128  (class class class)co 5818  ℝcr 7714   · cmul 7720

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

This theorem is referenced by:  rimul  8443  ltmul1a  8449  ltmul1  8450  lemul1  8451  reapmul1lem  8452  reapmul1  8453  remulext1  8457  mulext1  8470  recexaplem2  8509  redivclap  8587  prodgt0gt0  8705  prodgt0  8706  prodge0  8708  lemul1a  8712  ltmuldiv  8728  ledivmul  8731  lt2mul2div  8733  lemuldiv  8735  lt2msq1  8739  lt2msq  8740  ltdiv23  8746  lediv23  8747  le2msq  8755  msq11  8756  div4p1lem1div2  9069  mul2lt0rlt0  9648  lincmb01cmp  9889  iccf1o  9890  qbtwnrelemcalc  10137  qbtwnre  10138  flhalf  10183  modqval  10205  modqge0  10213  modqmulnn  10223  bernneq  10520  bernneq3  10522  expnbnd  10523  nn0opthlem2d  10577  faclbnd  10597  faclbnd6  10600  remullem  10753  cvg1nlemres  10867  resqrexlemover  10892  resqrexlemnm  10900  resqrexlemglsq  10904  sqrtmul  10917  abstri  10986  maxabslemlub  11089  maxltsup  11100  bdtrilem  11120  mulcn2  11191  reccn2ap  11192  cvgratnnlembern  11402  cvgratnnlemnexp  11403  cvgratnnlemmn  11404  cvgratnnlemabsle  11406  cvgratnnlemfm  11408  cvgratnnlemrate  11409  mertenslemi1  11414  fprodge1  11518  efcllem  11538  ege2le3  11550  eftlub  11569  sin02gt0  11642  cos12dec  11646  eirraplem  11655  dvdslelemd  11716  divalglemnqt  11792  oddennn  12093  metss2lem  12857  dveflem  13047  sin0pilem1  13062  sin0pilem2  13063  tangtx  13119  logdivlti  13162  rpcxpcl  13184  cxpmul  13193  cxplt  13196  rpcxple2  13198  rpcxplt2  13199  apcxp2  13218  rpabscxpbnd  13219  trilpolemclim  13569  trilpolemcl  13570  trilpolemisumle  13571  trilpolemeq1  13573  trilpolemlt1  13574  nconstwlpolemgt0  13596