Theorem remulcld 7717

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

Syntax hints:   → wi 4   ∈ wcel 1463  (class class class)co 5728  ℝcr 7543   · cmul 7549

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

This theorem is referenced by:  rimul  8262  ltmul1a  8268  ltmul1  8269  lemul1  8270  reapmul1lem  8271  reapmul1  8272  remulext1  8276  mulext1  8289  recexaplem2  8323  redivclap  8401  prodgt0gt0  8516  prodgt0  8517  prodge0  8519  lemul1a  8523  ltmuldiv  8539  ledivmul  8542  lt2mul2div  8544  lemuldiv  8546  lt2msq1  8550  lt2msq  8551  ltdiv23  8557  lediv23  8558  le2msq  8566  msq11  8567  div4p1lem1div2  8874  lincmb01cmp  9676  iccf1o  9677  qbtwnrelemcalc  9923  qbtwnre  9924  flhalf  9965  modqval  9987  modqge0  9995  modqmulnn  10005  bernneq  10302  bernneq3  10304  expnbnd  10305  nn0opthlem2d  10357  faclbnd  10377  faclbnd6  10380  remullem  10533  cvg1nlemres  10646  resqrexlemover  10671  resqrexlemnm  10679  resqrexlemglsq  10683  sqrtmul  10696  abstri  10765  maxabslemlub  10868  maxltsup  10879  bdtrilem  10899  mulcn2  10970  reccn2ap  10971  cvgratnnlembern  11181  cvgratnnlemnexp  11182  cvgratnnlemmn  11183  cvgratnnlemabsle  11185  cvgratnnlemfm  11187  cvgratnnlemrate  11188  mertenslemi1  11193  efcllem  11213  ege2le3  11225  eftlub  11244  sin02gt0  11318  eirraplem  11328  dvdslelemd  11386  divalglemnqt  11462  oddennn  11747  metss2lem  12483  trilpolemclim  12913  trilpolemcl  12914  trilpolemisumle  12915  trilpolemeq1  12917  trilpolemlt1  12918