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

Theorem remulcli 7794
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 7762 . 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 1480  (class class class)co 5774   RRcr 7633    x. cmul 7639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulrcl 7733
This theorem is referenced by:  addltmul  8970  nn0lele2xi  9042  numltc  9221  ef01bndlem  11476  cos2bnd  11480  sin4lt0  11486  sincosq3sgn  12933  sincosq4sgn  12934  cosq23lt0  12938  coseq0q4123  12939  coseq00topi  12940  coseq0negpitopi  12941  sincos4thpi  12945  cosq34lt1  12955  cos02pilt1  12956  cos0pilt1  12957  taupi  13357
  Copyright terms: Public domain W3C validator