Theorem remulcl 7934

Description: Alias for ax-mulrcl 7905, for naming consistency with remulcli 7966. (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 7905	1 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148  (class class class)co 5870   RRcr 7805   x. cmul 7811

This theorem was proved from axioms:  ax-mulrcl 7905

This theorem is referenced by:  remulcli  7966  remulcld  7982  axmulgt0  8023  msqge0  8567  mulge0  8570  recexaplem2  8603  recexap  8604  ltmul12a  8811  lemul12b  8812  mulgt1  8814  ltdivmul  8827  cju  8912  addltmul  9149  zmulcl  9300  irrmul  9641  rpmulcl  9672  ge0mulcl  9976  iccdil  9992  reexpcl  10530  reexpclzap  10533  expge0  10549  expge1  10550  expubnd  10570  bernneq  10633  faclbnd  10712  faclbnd3  10714  facavg  10717  crre  10857  remim  10860  mulreap  10864  amgm2  11118  fprodrecl  11607  fprodreclf  11613  efcllemp  11657  ege2le3  11670  ef01bndlem  11755  cos01gt0  11761  dveflem  13969  sinq12gt0  14033  tangtx  14041  coskpi  14051  relogexp  14075  logcxp  14100  rpabscxpbnd  14141