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

Theorem remulcl 7468
Description: Alias for ax-mulrcl 7442, for naming consistency with remulcli 7500. (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 7442 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1438  (class class class)co 5652   RRcr 7347    x. cmul 7353
This theorem was proved from axioms:  ax-mulrcl 7442
This theorem is referenced by:  remulcli  7500  remulcld  7516  axmulgt0  7556  msqge0  8091  mulge0  8094  recexaplem2  8119  recexap  8120  ltmul12a  8319  lemul12b  8320  mulgt1  8322  ltdivmul  8335  cju  8419  addltmul  8650  zmulcl  8801  irrmul  9130  rpmulcl  9156  ge0mulcl  9398  iccdil  9413  reexpcl  9968  reexpclzap  9971  expge0  9987  expge1  9988  expubnd  10008  bernneq  10070  faclbnd  10145  faclbnd3  10147  facavg  10150  crre  10287  remim  10290  mulreap  10294  amgm2  10547  efcllemp  10944  ege2le3  10957  ef01bndlem  11043  cos01gt0  11049
  Copyright terms: Public domain W3C validator