Theorem remulcld 7820

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

Syntax hints:   -> wi 4   e. wcel 1481  (class class class)co 5782   RRcr 7643   x. cmul 7649

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

This theorem is referenced by:  rimul  8371  ltmul1a  8377  ltmul1  8378  lemul1  8379  reapmul1lem  8380  reapmul1  8381  remulext1  8385  mulext1  8398  recexaplem2  8437  redivclap  8515  prodgt0gt0  8633  prodgt0  8634  prodge0  8636  lemul1a  8640  ltmuldiv  8656  ledivmul  8659  lt2mul2div  8661  lemuldiv  8663  lt2msq1  8667  lt2msq  8668  ltdiv23  8674  lediv23  8675  le2msq  8683  msq11  8684  div4p1lem1div2  8997  mul2lt0rlt0  9576  lincmb01cmp  9816  iccf1o  9817  qbtwnrelemcalc  10064  qbtwnre  10065  flhalf  10106  modqval  10128  modqge0  10136  modqmulnn  10146  bernneq  10443  bernneq3  10445  expnbnd  10446  nn0opthlem2d  10499  faclbnd  10519  faclbnd6  10522  remullem  10675  cvg1nlemres  10789  resqrexlemover  10814  resqrexlemnm  10822  resqrexlemglsq  10826  sqrtmul  10839  abstri  10908  maxabslemlub  11011  maxltsup  11022  bdtrilem  11042  mulcn2  11113  reccn2ap  11114  cvgratnnlembern  11324  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemabsle  11328  cvgratnnlemfm  11330  cvgratnnlemrate  11331  mertenslemi1  11336  efcllem  11402  ege2le3  11414  eftlub  11433  sin02gt0  11506  cos12dec  11510  eirraplem  11519  dvdslelemd  11577  divalglemnqt  11653  oddennn  11941  metss2lem  12705  dveflem  12895  sin0pilem1  12910  sin0pilem2  12911  tangtx  12967  logdivlti  13010  rpcxpcl  13032  cxpmul  13041  cxplt  13044  rpcxple2  13046  rpcxplt2  13047  apcxp2  13066  rpabscxpbnd  13067  trilpolemclim  13404  trilpolemcl  13405  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409