ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  remulcl Unicode version

Theorem remulcl 7712
Description: Alias for ax-mulrcl 7683, for naming consistency with remulcli 7744. (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
StepHypRef Expression
1 ax-mulrcl 7683 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1463  (class class class)co 5740   RRcr 7583    x. cmul 7589
This theorem was proved from axioms:  ax-mulrcl 7683
This theorem is referenced by:  remulcli  7744  remulcld  7760  axmulgt0  7800  msqge0  8341  mulge0  8344  recexaplem2  8376  recexap  8377  ltmul12a  8578  lemul12b  8579  mulgt1  8581  ltdivmul  8594  cju  8679  addltmul  8910  zmulcl  9061  irrmul  9391  rpmulcl  9417  ge0mulcl  9716  iccdil  9732  reexpcl  10261  reexpclzap  10264  expge0  10280  expge1  10281  expubnd  10301  bernneq  10363  faclbnd  10438  faclbnd3  10440  facavg  10443  crre  10580  remim  10583  mulreap  10587  amgm2  10841  efcllemp  11274  ege2le3  11287  ef01bndlem  11373  cos01gt0  11379  dveflem  12761
  Copyright terms: Public domain W3C validator