Theorem remulcld 8356

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178   · cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8278

This theorem is used by:  rimul  8915  ltmul1a  8921  ltmul1  8922  lemul1  8923  reapmul1lem  8924  reapmul1  8925  remulext1  8929  mulext1  8942  recexaplem2  8982  redivclap  9063  prodgt0gt0  9183  prodgt0  9184  prodge0  9186  lemul1a  9190  ltmuldiv  9206  ledivmul  9209  lt2mul2div  9211  lemuldiv  9213  lt2msq1  9217  lt2msq  9218  ltdiv23  9224  lediv23  9225  le2msq  9233  msq11  9234  div4p1lem1div2  9563  mul2lt0rlt0  10170  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  qbtwnrelemcalc  10700  qbtwnre  10701  flhalf  10750  modqval  10774  modqge0  10782  modqmulnn  10792  bernneq  11111  bernneq3  11113  expnbnd  11114  nn0opthlem2d  11173  faclbnd  11193  faclbnd6  11196  remullem  11650  sq01  11674  cvg1nlemres  11765  resqrexlemover  11790  resqrexlemnm  11798  resqrexlemglsq  11802  sqrtmul  11815  abstri  11885  maxabslemlub  11988  maxltsup  11999  bdtrilem  12021  mulcn2  12094  reccn2ap  12095  cvgratnnlembern  12306  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemabsle  12310  cvgratnnlemfm  12312  cvgratnnlemrate  12313  mertenslemi1  12318  fprodge1  12422  efcllem  12442  ege2le3  12454  eftlub  12473  sin02gt0  12547  cos12dec  12551  eirraplem  12560  dvdslelemd  12626  divalglemnqt  12703  bitsp1o  12736  2expltfac  13239  oddennn  13332  metss2lem  15647  dveflem  15876  sin0pilem1  15932  sin0pilem2  15933  tangtx  15989  logdivlti  16033  rpcxpcl  16058  cxpmul  16067  cxplt  16071  rpcxple2  16073  rpcxplt2  16074  apcxp2  16094  rpabscxpbnd  16095  log2tlbndlog2  16139  pellexlem2  16149  perfectlem2  16198  bclbnd  16205  prmefexple  16206  bposlem1  16209  bposlem2  16210  lgsdilem  16244  gausslemma2dlem0c  16268  gausslemma2dlem2  16279  gausslemma2dlem3  16280  lgsquadlem1  16294  lgsquadlem2  16295  dichmul0orlem1  16851  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  nconstwlpolemgt0  17212