Theorem remulcld 7572

Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	|- ( ph -> A e. RR )
readdcld.2	|- ( ph -> B e. RR )

Assertion

Ref	Expression
remulcld	|- ( ph -> ( A x. B ) e. RR )

Proof of Theorem remulcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- ( ph -> A e. RR )
2		readdcld.2	. 2 |- ( ph -> B e. RR )
3		remulcl 7524	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	syl2anc 404	1 |- ( ph -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 1439  (class class class)co 5666   RRcr 7403   x. cmul 7409

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

This theorem is referenced by:  rimul  8116  ltmul1a  8122  ltmul1  8123  lemul1  8124  reapmul1lem  8125  reapmul1  8126  remulext1  8130  mulext1  8143  recexaplem2  8175  redivclap  8252  prodgt0gt0  8366  prodgt0  8367  prodge0  8369  lemul1a  8373  ltmuldiv  8389  ledivmul  8392  lt2mul2div  8394  lemuldiv  8396  lt2msq1  8400  lt2msq  8401  ltdiv23  8407  lediv23  8408  le2msq  8416  msq11  8417  div4p1lem1div2  8723  lincmb01cmp  9474  iccf1o  9475  qbtwnrelemcalc  9721  qbtwnre  9722  flhalf  9763  modqval  9785  modqge0  9793  modqmulnn  9803  bernneq  10128  bernneq3  10130  expnbnd  10131  nn0opthlem2d  10183  faclbnd  10203  faclbnd6  10206  remullem  10359  cvg1nlemres  10472  resqrexlemover  10497  resqrexlemnm  10505  resqrexlemglsq  10509  sqrtmul  10522  abstri  10591  maxabslemlub  10694  maxltsup  10705  mulcn2  10755  cvgratnnlembern  10971  cvgratnnlemnexp  10972  cvgratnnlemmn  10973  cvgratnnlemabsle  10975  cvgratnnlemfm  10977  cvgratnnlemrate  10978  mertenslemi1  10983  efcllem  11003  ege2le3  11015  eftlub  11034  sin02gt0  11108  eirraplem  11118  dvdslelemd  11176  divalglemnqt  11252  oddennn  11537