Theorem remulcl 8053

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2176  (class class class)co 5944   RRcr 7924   x. cmul 7930

This theorem was proved from axioms:  ax-mulrcl 8024

This theorem is referenced by:  remulcli  8086  remulcld  8103  axmulgt0  8144  msqge0  8689  mulge0  8692  recexaplem2  8725  recexap  8726  ltmul12a  8933  lemul12b  8934  mulgt1  8936  ltdivmul  8949  cju  9034  addltmul  9274  zmulcl  9426  irrmul  9768  rpmulcl  9800  ge0mulcl  10104  iccdil  10120  reexpcl  10701  reexpclzap  10704  expge0  10720  expge1  10721  expubnd  10741  bernneq  10805  faclbnd  10886  faclbnd3  10888  facavg  10891  crre  11168  remim  11171  mulreap  11175  amgm2  11429  fprodrecl  11919  fprodreclf  11925  efcllemp  11969  ege2le3  11982  ef01bndlem  12067  cos01gt0  12074  4sqlem11  12724  dveflem  15198  sinq12gt0  15302  tangtx  15310  coskpi  15320  relogexp  15344  logcxp  15369  rpabscxpbnd  15412