MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  remulcli Structured version   Unicode version

Theorem remulcli 9104
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 9075 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3mp2an 654 1  |-  ( A  x.  B )  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1725  (class class class)co 6081   RRcr 8989    x. cmul 8995
This theorem is referenced by:  ledivp1i  9936  ltdivp1i  9937  addltmul  10203  nn0lele2xi  10272  numltc  10402  nn0opthlem2  11562  faclbnd4lem1  11584  ef01bndlem  12785  cos2bnd  12789  sin4lt0  12796  dvdslelem  12894  divalglem1  12914  divalglem6  12918  sincosq3sgn  20408  sincosq4sgn  20409  sincos4thpi  20421  efif1olem1  20444  efif1olem2  20445  efif1olem4  20447  efif1o  20448  efifo  20449  ang180lem1  20651  ang180lem2  20652  log2ublem1  20786  log2ublem2  20787  bpos1lem  21066  bposlem7  21074  bposlem8  21075  bposlem9  21076  chebbnd1lem3  21165  chebbnd1  21166  chto1ub  21170  siilem1  22352  normlem6  22617  normlem7  22618  norm-ii-i  22639  normpar2i  22658  bcsiALT  22681  nmopadjlem  23592  nmopcoi  23598  bdopcoi  23601  nmopcoadji  23604  unierri  23607  circum  25111  stirlinglem11  27809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulrcl 9053
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator