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

Theorem remulcl 7009
Description: Alias for ax-mulrcl 6983, for naming consistency with remulcli 7041. (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 6983 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    e. wcel 1393  (class class class)co 5512   RRcr 6888    x. cmul 6894
This theorem was proved from axioms:  ax-mulrcl 6983
This theorem is referenced by:  remulcli  7041  remulcld  7056  axmulgt0  7091  msqge0  7607  mulge0  7610  recexaplem2  7633  recexap  7634  ltmul12a  7826  lemul12b  7827  mulgt1  7829  ltdivmul  7842  cju  7913  addltmul  8161  zmulcl  8297  irrmul  8581  rpmulcl  8607  ge0mulcl  8851  iccdil  8866  reexpcl  9272  reexpclzap  9275  expge0  9291  expge1  9292  expubnd  9311  bernneq  9369  crre  9457  remim  9460  mulreap  9464  amgm2  9714
  Copyright terms: Public domain W3C validator