Theorem remulcl 8308

Description: Alias for ax-mulrcl 8279, for naming consistency with remulcli 8341. (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 8279	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 6085   RRcr 8179   x. cmul 8185

This proof depends on axioms:  ax-mulrcl 8279

This theorem is used by:  remulcli  8341  remulcld  8357  axmulgt0  8398  msqge0  8947  mulge0  8950  recexaplem2  8983  recexap  8984  ltmul12a  9193  lemul12b  9194  mulgt1  9196  ltdivmul  9209  cju  9294  addltmul  9547  zmulcl  9703  irrmul  10058  rpmulcl  10090  ge0mulcl  10395  iccdil  10411  reexpcl  11008  reexpclzap  11011  expge0  11027  expge1  11028  expubnd  11048  bernneq  11113  faclbnd  11195  faclbnd3  11197  facavg  11200  crre  11638  remim  11641  mulreap  11645  amgm2  11901  fprodrecl  12394  fprodreclf  12400  efcllemp  12444  ege2le3  12457  ef01bndlem  12542  cos01gt0  12549  4sqlem11  13203  dveflem  15926  sinq12gt0  16031  tangtx  16039  coskpi  16049  relogexp  16076  logfac  16100  logcxp  16104  rpabscxpbnd  16149  chtublem  16269  chtqub  16270  bpos1lem  16283  bposlem1  16285  bposlem2  16286  bposlem6  16290  bposlem7  16291  bposlem9  16293