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

Theorem remulcl 7716
Description: Alias for ax-mulrcl 7687, for naming consistency with remulcli 7748. (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 7687 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 1465  (class class class)co 5742   RRcr 7587    x. cmul 7593
This theorem was proved from axioms:  ax-mulrcl 7687
This theorem is referenced by:  remulcli  7748  remulcld  7764  axmulgt0  7804  msqge0  8346  mulge0  8349  recexaplem2  8381  recexap  8382  ltmul12a  8586  lemul12b  8587  mulgt1  8589  ltdivmul  8602  cju  8687  addltmul  8924  zmulcl  9075  irrmul  9407  rpmulcl  9434  ge0mulcl  9733  iccdil  9749  reexpcl  10278  reexpclzap  10281  expge0  10297  expge1  10298  expubnd  10318  bernneq  10380  faclbnd  10455  faclbnd3  10457  facavg  10460  crre  10597  remim  10600  mulreap  10604  amgm2  10858  efcllemp  11291  ege2le3  11304  ef01bndlem  11390  cos01gt0  11396  dveflem  12782  sinq12gt0  12838  tangtx  12846  coskpi  12856
  Copyright terms: Public domain W3C validator