Theorem remulcld 8188

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6007  ℝcr 8009   · cmul 8015

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

This theorem is referenced by:  rimul  8743  ltmul1a  8749  ltmul1  8750  lemul1  8751  reapmul1lem  8752  reapmul1  8753  remulext1  8757  mulext1  8770  recexaplem2  8810  redivclap  8889  prodgt0gt0  9009  prodgt0  9010  prodge0  9012  lemul1a  9016  ltmuldiv  9032  ledivmul  9035  lt2mul2div  9037  lemuldiv  9039  lt2msq1  9043  lt2msq  9044  ltdiv23  9050  lediv23  9051  le2msq  9059  msq11  9060  div4p1lem1div2  9376  mul2lt0rlt0  9967  lincmb01cmp  10211  iccf1o  10212  qbtwnrelemcalc  10487  qbtwnre  10488  flhalf  10534  modqval  10558  modqge0  10566  modqmulnn  10576  bernneq  10894  bernneq3  10896  expnbnd  10897  nn0opthlem2d  10955  faclbnd  10975  faclbnd6  10978  remullem  11398  cvg1nlemres  11512  resqrexlemover  11537  resqrexlemnm  11545  resqrexlemglsq  11549  sqrtmul  11562  abstri  11631  maxabslemlub  11734  maxltsup  11745  bdtrilem  11766  mulcn2  11839  reccn2ap  11840  cvgratnnlembern  12050  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  cvgratnnlemabsle  12054  cvgratnnlemfm  12056  cvgratnnlemrate  12057  mertenslemi1  12062  fprodge1  12166  efcllem  12186  ege2le3  12198  eftlub  12217  sin02gt0  12291  cos12dec  12295  eirraplem  12304  dvdslelemd  12370  divalglemnqt  12447  bitsp1o  12480  2expltfac  12978  oddennn  12979  metss2lem  15187  dveflem  15416  sin0pilem1  15471  sin0pilem2  15472  tangtx  15528  logdivlti  15571  rpcxpcl  15593  cxpmul  15602  cxplt  15606  rpcxple2  15608  rpcxplt2  15609  apcxp2  15629  rpabscxpbnd  15630  perfectlem2  15690  lgsdilem  15722  gausslemma2dlem0c  15746  gausslemma2dlem2  15757  gausslemma2dlem3  15758  lgsquadlem1  15772  lgsquadlem2  15773  trilpolemclim  16492  trilpolemcl  16493  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  nconstwlpolemgt0  16520