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

Theorem remulcl 7067
Description: Alias for ax-mulrcl 7041, for naming consistency with remulcli 7099. (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 7041 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    e. wcel 1409  (class class class)co 5540   RRcr 6946    x. cmul 6952
This theorem was proved from axioms:  ax-mulrcl 7041
This theorem is referenced by:  remulcli  7099  remulcld  7115  axmulgt0  7150  msqge0  7681  mulge0  7684  recexaplem2  7707  recexap  7708  ltmul12a  7901  lemul12b  7902  mulgt1  7904  ltdivmul  7917  cju  7989  addltmul  8218  zmulcl  8355  irrmul  8679  rpmulcl  8705  ge0mulcl  8952  iccdil  8967  reexpcl  9437  reexpclzap  9440  expge0  9456  expge1  9457  expubnd  9477  bernneq  9537  faclbnd  9609  faclbnd3  9611  facavg  9614  crre  9685  remim  9688  mulreap  9692  amgm2  9945
  Copyright terms: Public domain W3C validator