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

Theorem remulcli 8867
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 8838 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3mp2an 653 1  |-  ( A  x.  B )  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1696  (class class class)co 5874   RRcr 8752    x. cmul 8758
This theorem is referenced by:  ledivp1i  9698  ltdivp1i  9699  addltmul  9963  nn0lele2xi  10032  numltc  10160  nn0opthlem2  11300  faclbnd4lem1  11322  ef01bndlem  12480  cos2bnd  12484  sin4lt0  12491  dvdslelem  12589  divalglem1  12609  divalglem6  12613  sincosq3sgn  19884  sincosq4sgn  19885  sincos4thpi  19897  efif1olem1  19920  efif1olem2  19921  efif1olem4  19923  efif1o  19924  efifo  19925  ang180lem1  20123  ang180lem2  20124  log2ublem1  20258  log2ublem2  20259  bpos1lem  20537  bposlem7  20545  bposlem8  20546  bposlem9  20547  chebbnd1lem3  20636  chebbnd1  20637  chto1ub  20641  siilem1  21445  normlem6  21710  normlem7  21711  norm-ii-i  21732  normpar2i  21751  bcsiALT  21774  nmopadjlem  22685  nmopcoi  22691  bdopcoi  22694  nmopcoadji  22697  unierri  22700  circum  24022  stirlinglem11  27936
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulrcl 8816
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator