Theorem remulcld 7987

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

Syntax hints:   → wi 4   ∈ wcel 2148  (class class class)co 5874  ℝcr 7809   · cmul 7815

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

This theorem is referenced by:  rimul  8541  ltmul1a  8547  ltmul1  8548  lemul1  8549  reapmul1lem  8550  reapmul1  8551  remulext1  8555  mulext1  8568  recexaplem2  8608  redivclap  8687  prodgt0gt0  8807  prodgt0  8808  prodge0  8810  lemul1a  8814  ltmuldiv  8830  ledivmul  8833  lt2mul2div  8835  lemuldiv  8837  lt2msq1  8841  lt2msq  8842  ltdiv23  8848  lediv23  8849  le2msq  8857  msq11  8858  div4p1lem1div2  9171  mul2lt0rlt0  9758  lincmb01cmp  10002  iccf1o  10003  qbtwnrelemcalc  10255  qbtwnre  10256  flhalf  10301  modqval  10323  modqge0  10331  modqmulnn  10341  bernneq  10640  bernneq3  10642  expnbnd  10643  nn0opthlem2d  10700  faclbnd  10720  faclbnd6  10723  remullem  10879  cvg1nlemres  10993  resqrexlemover  11018  resqrexlemnm  11026  resqrexlemglsq  11030  sqrtmul  11043  abstri  11112  maxabslemlub  11215  maxltsup  11226  bdtrilem  11246  mulcn2  11319  reccn2ap  11320  cvgratnnlembern  11530  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratnnlemabsle  11534  cvgratnnlemfm  11536  cvgratnnlemrate  11537  mertenslemi1  11542  fprodge1  11646  efcllem  11666  ege2le3  11678  eftlub  11697  sin02gt0  11770  cos12dec  11774  eirraplem  11783  dvdslelemd  11848  divalglemnqt  11924  oddennn  12392  metss2lem  13967  dveflem  14157  sin0pilem1  14172  sin0pilem2  14173  tangtx  14229  logdivlti  14272  rpcxpcl  14294  cxpmul  14303  cxplt  14306  rpcxple2  14308  rpcxplt2  14309  apcxp2  14328  rpabscxpbnd  14329  lgsdilem  14398  trilpolemclim  14754  trilpolemcl  14755  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  nconstwlpolemgt0  14781