Theorem remulcld 8001

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

Syntax hints:   → wi 4   ∈ wcel 2158  (class class class)co 5888  ℝcr 7823   · cmul 7829

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

This theorem is referenced by:  rimul  8555  ltmul1a  8561  ltmul1  8562  lemul1  8563  reapmul1lem  8564  reapmul1  8565  remulext1  8569  mulext1  8582  recexaplem2  8622  redivclap  8701  prodgt0gt0  8821  prodgt0  8822  prodge0  8824  lemul1a  8828  ltmuldiv  8844  ledivmul  8847  lt2mul2div  8849  lemuldiv  8851  lt2msq1  8855  lt2msq  8856  ltdiv23  8862  lediv23  8863  le2msq  8871  msq11  8872  div4p1lem1div2  9185  mul2lt0rlt0  9772  lincmb01cmp  10016  iccf1o  10017  qbtwnrelemcalc  10269  qbtwnre  10270  flhalf  10315  modqval  10337  modqge0  10345  modqmulnn  10355  bernneq  10654  bernneq3  10656  expnbnd  10657  nn0opthlem2d  10714  faclbnd  10734  faclbnd6  10737  remullem  10893  cvg1nlemres  11007  resqrexlemover  11032  resqrexlemnm  11040  resqrexlemglsq  11044  sqrtmul  11057  abstri  11126  maxabslemlub  11229  maxltsup  11240  bdtrilem  11260  mulcn2  11333  reccn2ap  11334  cvgratnnlembern  11544  cvgratnnlemnexp  11545  cvgratnnlemmn  11546  cvgratnnlemabsle  11548  cvgratnnlemfm  11550  cvgratnnlemrate  11551  mertenslemi1  11556  fprodge1  11660  efcllem  11680  ege2le3  11692  eftlub  11711  sin02gt0  11784  cos12dec  11788  eirraplem  11797  dvdslelemd  11862  divalglemnqt  11938  oddennn  12406  metss2lem  14237  dveflem  14427  sin0pilem1  14442  sin0pilem2  14443  tangtx  14499  logdivlti  14542  rpcxpcl  14564  cxpmul  14573  cxplt  14576  rpcxple2  14578  rpcxplt2  14579  apcxp2  14598  rpabscxpbnd  14599  lgsdilem  14668  trilpolemclim  15025  trilpolemcl  15026  trilpolemisumle  15027  trilpolemeq1  15029  trilpolemlt1  15030  nconstwlpolemgt0  15053