Theorem remulcl 8127

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6001   RRcr 7998   x. cmul 8004

This theorem was proved from axioms:  ax-mulrcl 8098

This theorem is referenced by:  remulcli  8160  remulcld  8177  axmulgt0  8218  msqge0  8763  mulge0  8766  recexaplem2  8799  recexap  8800  ltmul12a  9007  lemul12b  9008  mulgt1  9010  ltdivmul  9023  cju  9108  addltmul  9348  zmulcl  9500  irrmul  9842  rpmulcl  9874  ge0mulcl  10178  iccdil  10194  reexpcl  10778  reexpclzap  10781  expge0  10797  expge1  10798  expubnd  10818  bernneq  10882  faclbnd  10963  faclbnd3  10965  facavg  10968  crre  11368  remim  11371  mulreap  11375  amgm2  11629  fprodrecl  12119  fprodreclf  12125  efcllemp  12169  ege2le3  12182  ef01bndlem  12267  cos01gt0  12274  4sqlem11  12924  dveflem  15400  sinq12gt0  15504  tangtx  15512  coskpi  15522  relogexp  15546  logcxp  15571  rpabscxpbnd  15614