Theorem remulcld 8269

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

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

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

This theorem is referenced by:  rimul  8824  ltmul1a  8830  ltmul1  8831  lemul1  8832  reapmul1lem  8833  reapmul1  8834  remulext1  8838  mulext1  8851  recexaplem2  8891  redivclap  8970  prodgt0gt0  9090  prodgt0  9091  prodge0  9093  lemul1a  9097  ltmuldiv  9113  ledivmul  9116  lt2mul2div  9118  lemuldiv  9120  lt2msq1  9124  lt2msq  9125  ltdiv23  9131  lediv23  9132  le2msq  9140  msq11  9141  div4p1lem1div2  9457  mul2lt0rlt0  10055  lincmb01cmp  10299  lincmble  10300  iccf1o  10301  qbtwnrelemcalc  10578  qbtwnre  10579  flhalf  10625  modqval  10649  modqge0  10657  modqmulnn  10667  bernneq  10985  bernneq3  10987  expnbnd  10988  nn0opthlem2d  11046  faclbnd  11066  faclbnd6  11069  remullem  11511  cvg1nlemres  11625  resqrexlemover  11650  resqrexlemnm  11658  resqrexlemglsq  11662  sqrtmul  11675  abstri  11744  maxabslemlub  11847  maxltsup  11858  bdtrilem  11879  mulcn2  11952  reccn2ap  11953  cvgratnnlembern  12164  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  cvgratnnlemabsle  12168  cvgratnnlemfm  12170  cvgratnnlemrate  12171  mertenslemi1  12176  fprodge1  12280  efcllem  12300  ege2le3  12312  eftlub  12331  sin02gt0  12405  cos12dec  12409  eirraplem  12418  dvdslelemd  12484  divalglemnqt  12561  bitsp1o  12594  2expltfac  13092  oddennn  13093  metss2lem  15308  dveflem  15537  sin0pilem1  15592  sin0pilem2  15593  tangtx  15649  logdivlti  15692  rpcxpcl  15714  cxpmul  15723  cxplt  15727  rpcxple2  15729  rpcxplt2  15730  apcxp2  15750  rpabscxpbnd  15751  pellexlem2  15792  perfectlem2  15814  lgsdilem  15846  gausslemma2dlem0c  15870  gausslemma2dlem2  15881  gausslemma2dlem3  15882  lgsquadlem1  15896  lgsquadlem2  15897  trilpolemclim  16768  trilpolemcl  16769  trilpolemisumle  16770  trilpolemeq1  16772  trilpolemlt1  16773  nconstwlpolemgt0  16797