Theorem remulcld 8052

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

Syntax hints:   → wi 4   ∈ wcel 2164  (class class class)co 5919  ℝcr 7873   · cmul 7879

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

This theorem is referenced by:  rimul  8606  ltmul1a  8612  ltmul1  8613  lemul1  8614  reapmul1lem  8615  reapmul1  8616  remulext1  8620  mulext1  8633  recexaplem2  8673  redivclap  8752  prodgt0gt0  8872  prodgt0  8873  prodge0  8875  lemul1a  8879  ltmuldiv  8895  ledivmul  8898  lt2mul2div  8900  lemuldiv  8902  lt2msq1  8906  lt2msq  8907  ltdiv23  8913  lediv23  8914  le2msq  8922  msq11  8923  div4p1lem1div2  9239  mul2lt0rlt0  9828  lincmb01cmp  10072  iccf1o  10073  qbtwnrelemcalc  10327  qbtwnre  10328  flhalf  10374  modqval  10398  modqge0  10406  modqmulnn  10416  bernneq  10734  bernneq3  10736  expnbnd  10737  nn0opthlem2d  10795  faclbnd  10815  faclbnd6  10818  remullem  11018  cvg1nlemres  11132  resqrexlemover  11157  resqrexlemnm  11165  resqrexlemglsq  11169  sqrtmul  11182  abstri  11251  maxabslemlub  11354  maxltsup  11365  bdtrilem  11385  mulcn2  11458  reccn2ap  11459  cvgratnnlembern  11669  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemabsle  11673  cvgratnnlemfm  11675  cvgratnnlemrate  11676  mertenslemi1  11681  fprodge1  11785  efcllem  11805  ege2le3  11817  eftlub  11836  sin02gt0  11910  cos12dec  11914  eirraplem  11923  dvdslelemd  11988  divalglemnqt  12064  oddennn  12552  metss2lem  14676  dveflem  14905  sin0pilem1  14957  sin0pilem2  14958  tangtx  15014  logdivlti  15057  rpcxpcl  15079  cxpmul  15088  cxplt  15091  rpcxple2  15093  rpcxplt2  15094  apcxp2  15113  rpabscxpbnd  15114  lgsdilem  15184  gausslemma2dlem0c  15208  gausslemma2dlem2  15219  gausslemma2dlem3  15220  lgsquadlem1  15234  lgsquadlem2  15235  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  nconstwlpolemgt0  15624