Theorem remulcld 7929

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

Syntax hints:   → wi 4   ∈ wcel 2136  (class class class)co 5842  ℝcr 7752   · cmul 7758

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

This theorem is referenced by:  rimul  8483  ltmul1a  8489  ltmul1  8490  lemul1  8491  reapmul1lem  8492  reapmul1  8493  remulext1  8497  mulext1  8510  recexaplem2  8549  redivclap  8627  prodgt0gt0  8746  prodgt0  8747  prodge0  8749  lemul1a  8753  ltmuldiv  8769  ledivmul  8772  lt2mul2div  8774  lemuldiv  8776  lt2msq1  8780  lt2msq  8781  ltdiv23  8787  lediv23  8788  le2msq  8796  msq11  8797  div4p1lem1div2  9110  mul2lt0rlt0  9695  lincmb01cmp  9939  iccf1o  9940  qbtwnrelemcalc  10191  qbtwnre  10192  flhalf  10237  modqval  10259  modqge0  10267  modqmulnn  10277  bernneq  10575  bernneq3  10577  expnbnd  10578  nn0opthlem2d  10634  faclbnd  10654  faclbnd6  10657  remullem  10813  cvg1nlemres  10927  resqrexlemover  10952  resqrexlemnm  10960  resqrexlemglsq  10964  sqrtmul  10977  abstri  11046  maxabslemlub  11149  maxltsup  11160  bdtrilem  11180  mulcn2  11253  reccn2ap  11254  cvgratnnlembern  11464  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemabsle  11468  cvgratnnlemfm  11470  cvgratnnlemrate  11471  mertenslemi1  11476  fprodge1  11580  efcllem  11600  ege2le3  11612  eftlub  11631  sin02gt0  11704  cos12dec  11708  eirraplem  11717  dvdslelemd  11781  divalglemnqt  11857  oddennn  12325  metss2lem  13137  dveflem  13327  sin0pilem1  13342  sin0pilem2  13343  tangtx  13399  logdivlti  13442  rpcxpcl  13464  cxpmul  13473  cxplt  13476  rpcxple2  13478  rpcxplt2  13479  apcxp2  13498  rpabscxpbnd  13499  lgsdilem  13568  trilpolemclim  13915  trilpolemcl  13916  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  nconstwlpolemgt0  13942