Theorem remulcld 7990

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

Syntax hints:   → wi 4   ∈ wcel 2148  (class class class)co 5877  ℝcr 7812   · cmul 7818

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

This theorem is referenced by:  rimul  8544  ltmul1a  8550  ltmul1  8551  lemul1  8552  reapmul1lem  8553  reapmul1  8554  remulext1  8558  mulext1  8571  recexaplem2  8611  redivclap  8690  prodgt0gt0  8810  prodgt0  8811  prodge0  8813  lemul1a  8817  ltmuldiv  8833  ledivmul  8836  lt2mul2div  8838  lemuldiv  8840  lt2msq1  8844  lt2msq  8845  ltdiv23  8851  lediv23  8852  le2msq  8860  msq11  8861  div4p1lem1div2  9174  mul2lt0rlt0  9761  lincmb01cmp  10005  iccf1o  10006  qbtwnrelemcalc  10258  qbtwnre  10259  flhalf  10304  modqval  10326  modqge0  10334  modqmulnn  10344  bernneq  10643  bernneq3  10645  expnbnd  10646  nn0opthlem2d  10703  faclbnd  10723  faclbnd6  10726  remullem  10882  cvg1nlemres  10996  resqrexlemover  11021  resqrexlemnm  11029  resqrexlemglsq  11033  sqrtmul  11046  abstri  11115  maxabslemlub  11218  maxltsup  11229  bdtrilem  11249  mulcn2  11322  reccn2ap  11323  cvgratnnlembern  11533  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratnnlemabsle  11537  cvgratnnlemfm  11539  cvgratnnlemrate  11540  mertenslemi1  11545  fprodge1  11649  efcllem  11669  ege2le3  11681  eftlub  11700  sin02gt0  11773  cos12dec  11777  eirraplem  11786  dvdslelemd  11851  divalglemnqt  11927  oddennn  12395  metss2lem  14036  dveflem  14226  sin0pilem1  14241  sin0pilem2  14242  tangtx  14298  logdivlti  14341  rpcxpcl  14363  cxpmul  14372  cxplt  14375  rpcxple2  14377  rpcxplt2  14378  apcxp2  14397  rpabscxpbnd  14398  lgsdilem  14467  trilpolemclim  14823  trilpolemcl  14824  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  nconstwlpolemgt0  14851