Theorem remulcl 8009

Description: Alias for ax-mulrcl 7980, for naming consistency with remulcli 8042. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
remulcl	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Proof of Theorem remulcl

Step	Hyp	Ref	Expression
1		ax-mulrcl 7980	1 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2167  (class class class)co 5923   RRcr 7880   x. cmul 7886

This theorem was proved from axioms:  ax-mulrcl 7980

This theorem is referenced by:  remulcli  8042  remulcld  8059  axmulgt0  8100  msqge0  8645  mulge0  8648  recexaplem2  8681  recexap  8682  ltmul12a  8889  lemul12b  8890  mulgt1  8892  ltdivmul  8905  cju  8990  addltmul  9230  zmulcl  9381  irrmul  9723  rpmulcl  9755  ge0mulcl  10059  iccdil  10075  reexpcl  10650  reexpclzap  10653  expge0  10669  expge1  10670  expubnd  10690  bernneq  10754  faclbnd  10835  faclbnd3  10837  facavg  10840  crre  11024  remim  11027  mulreap  11031  amgm2  11285  fprodrecl  11775  fprodreclf  11781  efcllemp  11825  ege2le3  11838  ef01bndlem  11923  cos01gt0  11930  4sqlem11  12580  dveflem  14972  sinq12gt0  15076  tangtx  15084  coskpi  15094  relogexp  15118  logcxp  15143  rpabscxpbnd  15186