Theorem remulcl 7839

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2125  (class class class)co 5814   RRcr 7710   x. cmul 7716

This theorem was proved from axioms:  ax-mulrcl 7810

This theorem is referenced by:  remulcli  7871  remulcld  7887  axmulgt0  7928  msqge0  8470  mulge0  8473  recexaplem2  8505  recexap  8506  ltmul12a  8710  lemul12b  8711  mulgt1  8713  ltdivmul  8726  cju  8811  addltmul  9048  zmulcl  9199  irrmul  9534  rpmulcl  9563  ge0mulcl  9864  iccdil  9880  reexpcl  10414  reexpclzap  10417  expge0  10433  expge1  10434  expubnd  10454  bernneq  10516  faclbnd  10592  faclbnd3  10594  facavg  10597  crre  10734  remim  10737  mulreap  10741  amgm2  10995  fprodrecl  11482  fprodreclf  11488  efcllemp  11532  ege2le3  11545  ef01bndlem  11630  cos01gt0  11636  dveflem  13034  sinq12gt0  13098  tangtx  13106  coskpi  13116  relogexp  13140  logcxp  13165  rpabscxpbnd  13206