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  9707  irrmul  10063  rpmulcl  10095  ge0mulcl  10400  iccdil  10416  reexpcl  11013  reexpclzap  11016  expge0  11032  expge1  11033  expubnd  11053  bernneq  11118  faclbnd  11200  faclbnd3  11202  facavg  11205  crre  11643  remim  11646  mulreap  11650  amgm2  11906  fprodrecl  12399  fprodreclf  12405  efcllemp  12449  ege2le3  12462  ef01bndlem  12547  cos01gt0  12554  4sqlem11  13208  dveflem  15969  sinq12gt0  16074  tangtx  16082  coskpi  16092  relogexp  16119  logfac  16143  logcxp  16147  rpabscxpbnd  16192  chtublem  16312  chtqub  16313  bpos1lem  16326  bposlem1  16328  bposlem2  16329  bposlem6  16333  bposlem7  16334  bposlem9  16336