Theorem remulcl 8313

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6088   RRcr 8184   x. cmul 8190

This proof depends on axioms:  ax-mulrcl 8284

This theorem is used by:  remulcli  8346  remulcld  8362  axmulgt0  8403  msqge0  8952  mulge0  8955  recexaplem2  8988  recexap  8989  ltmul12a  9198  lemul12b  9199  mulgt1  9201  ltdivmul  9214  cju  9299  addltmul  9553  zmulcl  9709  irrmul  10064  rpmulcl  10096  ge0mulcl  10401  iccdil  10417  reexpcl  11014  reexpclzap  11017  expge0  11033  expge1  11034  expubnd  11054  bernneq  11119  faclbnd  11201  faclbnd3  11203  facavg  11206  crre  11644  remim  11647  mulreap  11651  amgm2  11907  fprodrecl  12400  fprodreclf  12406  efcllemp  12450  ege2le3  12463  ef01bndlem  12548  cos01gt0  12555  4sqlem11  13209  dveflem  15952  sinq12gt0  16057  tangtx  16065  coskpi  16075  relogexp  16102  logfac  16126  logcxp  16130  rpabscxpbnd  16175  chtublem  16295  chtqub  16296  bpos1lem  16309  bposlem1  16311  bposlem2  16312  bposlem6  16316  bposlem7  16317  bposlem9  16319