Theorem remulcl 7938

Description: Alias for ax-mulrcl 7909, for naming consistency with remulcli 7970. (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 7909	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 5874   RRcr 7809   x. cmul 7815

This theorem was proved from axioms:  ax-mulrcl 7909

This theorem is referenced by:  remulcli  7970  remulcld  7987  axmulgt0  8028  msqge0  8572  mulge0  8575  recexaplem2  8608  recexap  8609  ltmul12a  8816  lemul12b  8817  mulgt1  8819  ltdivmul  8832  cju  8917  addltmul  9154  zmulcl  9305  irrmul  9646  rpmulcl  9677  ge0mulcl  9981  iccdil  9997  reexpcl  10536  reexpclzap  10539  expge0  10555  expge1  10556  expubnd  10576  bernneq  10640  faclbnd  10720  faclbnd3  10722  facavg  10725  crre  10865  remim  10868  mulreap  10872  amgm2  11126  fprodrecl  11615  fprodreclf  11621  efcllemp  11665  ege2le3  11678  ef01bndlem  11763  cos01gt0  11769  dveflem  14157  sinq12gt0  14221  tangtx  14229  coskpi  14239  relogexp  14263  logcxp  14288  rpabscxpbnd  14329