Theorem remulcl 7939

Description: Alias for ax-mulrcl 7910, for naming consistency with remulcli 7971. (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 7910	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 5875   RRcr 7810   x. cmul 7816

This theorem was proved from axioms:  ax-mulrcl 7910

This theorem is referenced by:  remulcli  7971  remulcld  7988  axmulgt0  8029  msqge0  8573  mulge0  8576  recexaplem2  8609  recexap  8610  ltmul12a  8817  lemul12b  8818  mulgt1  8820  ltdivmul  8833  cju  8918  addltmul  9155  zmulcl  9306  irrmul  9647  rpmulcl  9678  ge0mulcl  9982  iccdil  9998  reexpcl  10537  reexpclzap  10540  expge0  10556  expge1  10557  expubnd  10577  bernneq  10641  faclbnd  10721  faclbnd3  10723  facavg  10726  crre  10866  remim  10869  mulreap  10873  amgm2  11127  fprodrecl  11616  fprodreclf  11622  efcllemp  11666  ege2le3  11679  ef01bndlem  11764  cos01gt0  11770  dveflem  14190  sinq12gt0  14254  tangtx  14262  coskpi  14272  relogexp  14296  logcxp  14321  rpabscxpbnd  14362