Theorem remulcld 8060

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

Syntax hints:   → wi 4   ∈ wcel 2167  (class class class)co 5923  ℝcr 7881   · cmul 7887

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

This theorem is referenced by:  rimul  8615  ltmul1a  8621  ltmul1  8622  lemul1  8623  reapmul1lem  8624  reapmul1  8625  remulext1  8629  mulext1  8642  recexaplem2  8682  redivclap  8761  prodgt0gt0  8881  prodgt0  8882  prodge0  8884  lemul1a  8888  ltmuldiv  8904  ledivmul  8907  lt2mul2div  8909  lemuldiv  8911  lt2msq1  8915  lt2msq  8916  ltdiv23  8922  lediv23  8923  le2msq  8931  msq11  8932  div4p1lem1div2  9248  mul2lt0rlt0  9837  lincmb01cmp  10081  iccf1o  10082  qbtwnrelemcalc  10348  qbtwnre  10349  flhalf  10395  modqval  10419  modqge0  10427  modqmulnn  10437  bernneq  10755  bernneq3  10757  expnbnd  10758  nn0opthlem2d  10816  faclbnd  10836  faclbnd6  10839  remullem  11039  cvg1nlemres  11153  resqrexlemover  11178  resqrexlemnm  11186  resqrexlemglsq  11190  sqrtmul  11203  abstri  11272  maxabslemlub  11375  maxltsup  11386  bdtrilem  11407  mulcn2  11480  reccn2ap  11481  cvgratnnlembern  11691  cvgratnnlemnexp  11692  cvgratnnlemmn  11693  cvgratnnlemabsle  11695  cvgratnnlemfm  11697  cvgratnnlemrate  11698  mertenslemi1  11703  fprodge1  11807  efcllem  11827  ege2le3  11839  eftlub  11858  sin02gt0  11932  cos12dec  11936  eirraplem  11945  dvdslelemd  12011  divalglemnqt  12088  bitsp1o  12121  2expltfac  12619  oddennn  12620  metss2lem  14759  dveflem  14988  sin0pilem1  15043  sin0pilem2  15044  tangtx  15100  logdivlti  15143  rpcxpcl  15165  cxpmul  15174  cxplt  15178  rpcxple2  15180  rpcxplt2  15181  apcxp2  15201  rpabscxpbnd  15202  perfectlem2  15262  lgsdilem  15294  gausslemma2dlem0c  15318  gausslemma2dlem2  15329  gausslemma2dlem3  15330  lgsquadlem1  15344  lgsquadlem2  15345  trilpolemclim  15707  trilpolemcl  15708  trilpolemisumle  15709  trilpolemeq1  15711  trilpolemlt1  15712  nconstwlpolemgt0  15735