Theorem remulcld 8252

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6028  ℝcr 8074   · cmul 8080

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

This theorem is referenced by:  rimul  8807  ltmul1a  8813  ltmul1  8814  lemul1  8815  reapmul1lem  8816  reapmul1  8817  remulext1  8821  mulext1  8834  recexaplem2  8874  redivclap  8953  prodgt0gt0  9073  prodgt0  9074  prodge0  9076  lemul1a  9080  ltmuldiv  9096  ledivmul  9099  lt2mul2div  9101  lemuldiv  9103  lt2msq1  9107  lt2msq  9108  ltdiv23  9114  lediv23  9115  le2msq  9123  msq11  9124  div4p1lem1div2  9440  mul2lt0rlt0  10038  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  qbtwnrelemcalc  10561  qbtwnre  10562  flhalf  10608  modqval  10632  modqge0  10640  modqmulnn  10650  bernneq  10968  bernneq3  10970  expnbnd  10971  nn0opthlem2d  11029  faclbnd  11049  faclbnd6  11052  remullem  11494  cvg1nlemres  11608  resqrexlemover  11633  resqrexlemnm  11641  resqrexlemglsq  11645  sqrtmul  11658  abstri  11727  maxabslemlub  11830  maxltsup  11841  bdtrilem  11862  mulcn2  11935  reccn2ap  11936  cvgratnnlembern  12147  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemabsle  12151  cvgratnnlemfm  12153  cvgratnnlemrate  12154  mertenslemi1  12159  fprodge1  12263  efcllem  12283  ege2le3  12295  eftlub  12314  sin02gt0  12388  cos12dec  12392  eirraplem  12401  dvdslelemd  12467  divalglemnqt  12544  bitsp1o  12577  2expltfac  13075  oddennn  13076  metss2lem  15291  dveflem  15520  sin0pilem1  15575  sin0pilem2  15576  tangtx  15632  logdivlti  15675  rpcxpcl  15697  cxpmul  15706  cxplt  15710  rpcxple2  15712  rpcxplt2  15713  apcxp2  15733  rpabscxpbnd  15734  pellexlem2  15775  perfectlem2  15797  lgsdilem  15829  gausslemma2dlem0c  15853  gausslemma2dlem2  15864  gausslemma2dlem3  15865  lgsquadlem1  15879  lgsquadlem2  15880  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  nconstwlpolemgt0  16780