Theorem remulcld 8002

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 7953	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 2158  (class class class)co 5888   RRcr 7824   x. cmul 7830

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

This theorem is referenced by:  rimul  8556  ltmul1a  8562  ltmul1  8563  lemul1  8564  reapmul1lem  8565  reapmul1  8566  remulext1  8570  mulext1  8583  recexaplem2  8623  redivclap  8702  prodgt0gt0  8822  prodgt0  8823  prodge0  8825  lemul1a  8829  ltmuldiv  8845  ledivmul  8848  lt2mul2div  8850  lemuldiv  8852  lt2msq1  8856  lt2msq  8857  ltdiv23  8863  lediv23  8864  le2msq  8872  msq11  8873  div4p1lem1div2  9186  mul2lt0rlt0  9773  lincmb01cmp  10017  iccf1o  10018  qbtwnrelemcalc  10270  qbtwnre  10271  flhalf  10316  modqval  10338  modqge0  10346  modqmulnn  10356  bernneq  10655  bernneq3  10657  expnbnd  10658  nn0opthlem2d  10715  faclbnd  10735  faclbnd6  10738  remullem  10894  cvg1nlemres  11008  resqrexlemover  11033  resqrexlemnm  11041  resqrexlemglsq  11045  sqrtmul  11058  abstri  11127  maxabslemlub  11230  maxltsup  11241  bdtrilem  11261  mulcn2  11334  reccn2ap  11335  cvgratnnlembern  11545  cvgratnnlemnexp  11546  cvgratnnlemmn  11547  cvgratnnlemabsle  11549  cvgratnnlemfm  11551  cvgratnnlemrate  11552  mertenslemi1  11557  fprodge1  11661  efcllem  11681  ege2le3  11693  eftlub  11712  sin02gt0  11785  cos12dec  11789  eirraplem  11798  dvdslelemd  11863  divalglemnqt  11939  oddennn  12407  metss2lem  14293  dveflem  14483  sin0pilem1  14498  sin0pilem2  14499  tangtx  14555  logdivlti  14598  rpcxpcl  14620  cxpmul  14629  cxplt  14632  rpcxple2  14634  rpcxplt2  14635  apcxp2  14654  rpabscxpbnd  14655  lgsdilem  14724  trilpolemclim  15081  trilpolemcl  15082  trilpolemisumle  15083  trilpolemeq1  15085  trilpolemlt1  15086  nconstwlpolemgt0  15109