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

Theorem remulcli 7748
Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
Hypotheses
Ref Expression
recni.1  |-  A  e.  RR
axri.2  |-  B  e.  RR
Assertion
Ref Expression
remulcli  |-  ( A  x.  B )  e.  RR

Proof of Theorem remulcli
StepHypRef Expression
1 recni.1 . 2  |-  A  e.  RR
2 axri.2 . 2  |-  B  e.  RR
3 remulcl 7716 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3mp2an 422 1  |-  ( A  x.  B )  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1465  (class class class)co 5742   RRcr 7587    x. cmul 7593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulrcl 7687
This theorem is referenced by:  addltmul  8924  nn0lele2xi  8996  numltc  9175  ef01bndlem  11390  cos2bnd  11394  sin4lt0  11400  sincosq3sgn  12836  sincosq4sgn  12837  cosq23lt0  12841  coseq0q4123  12842  coseq00topi  12843  coseq0negpitopi  12844  sincos4thpi  12848  cosq34lt1  12858  cos02pilt1  12859  taupi  13166
  Copyright terms: Public domain W3C validator