Theorem remulcld 7789

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

Syntax hints:   → wi 4   ∈ wcel 1480  (class class class)co 5767  ℝcr 7612   · cmul 7618

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

This theorem is referenced by:  rimul  8340  ltmul1a  8346  ltmul1  8347  lemul1  8348  reapmul1lem  8349  reapmul1  8350  remulext1  8354  mulext1  8367  recexaplem2  8406  redivclap  8484  prodgt0gt0  8602  prodgt0  8603  prodge0  8605  lemul1a  8609  ltmuldiv  8625  ledivmul  8628  lt2mul2div  8630  lemuldiv  8632  lt2msq1  8636  lt2msq  8637  ltdiv23  8643  lediv23  8644  le2msq  8652  msq11  8653  div4p1lem1div2  8966  mul2lt0rlt0  9539  lincmb01cmp  9779  iccf1o  9780  qbtwnrelemcalc  10026  qbtwnre  10027  flhalf  10068  modqval  10090  modqge0  10098  modqmulnn  10108  bernneq  10405  bernneq3  10407  expnbnd  10408  nn0opthlem2d  10460  faclbnd  10480  faclbnd6  10483  remullem  10636  cvg1nlemres  10750  resqrexlemover  10775  resqrexlemnm  10783  resqrexlemglsq  10787  sqrtmul  10800  abstri  10869  maxabslemlub  10972  maxltsup  10983  bdtrilem  11003  mulcn2  11074  reccn2ap  11075  cvgratnnlembern  11285  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemabsle  11289  cvgratnnlemfm  11291  cvgratnnlemrate  11292  mertenslemi1  11297  efcllem  11354  ege2le3  11366  eftlub  11385  sin02gt0  11459  cos12dec  11463  eirraplem  11472  dvdslelemd  11530  divalglemnqt  11606  oddennn  11894  metss2lem  12655  dveflem  12844  sin0pilem1  12851  sin0pilem2  12852  tangtx  12908  trilpolemclim  13218  trilpolemcl  13219  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223