Theorem remulcl 8088

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2178  (class class class)co 5967   RRcr 7959   x. cmul 7965

This theorem was proved from axioms:  ax-mulrcl 8059

This theorem is referenced by:  remulcli  8121  remulcld  8138  axmulgt0  8179  msqge0  8724  mulge0  8727  recexaplem2  8760  recexap  8761  ltmul12a  8968  lemul12b  8969  mulgt1  8971  ltdivmul  8984  cju  9069  addltmul  9309  zmulcl  9461  irrmul  9803  rpmulcl  9835  ge0mulcl  10139  iccdil  10155  reexpcl  10738  reexpclzap  10741  expge0  10757  expge1  10758  expubnd  10778  bernneq  10842  faclbnd  10923  faclbnd3  10925  facavg  10928  crre  11283  remim  11286  mulreap  11290  amgm2  11544  fprodrecl  12034  fprodreclf  12040  efcllemp  12084  ege2le3  12097  ef01bndlem  12182  cos01gt0  12189  4sqlem11  12839  dveflem  15313  sinq12gt0  15417  tangtx  15425  coskpi  15435  relogexp  15459  logcxp  15484  rpabscxpbnd  15527