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

Theorem remulcli 8851
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 8822 . 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 1684  (class class class)co 5858   RRcr 8736    x. cmul 8742
This theorem is referenced by:  ledivp1i  9682  ltdivp1i  9683  addltmul  9947  nn0lele2xi  10016  numltc  10144  nn0opthlem2  11284  faclbnd4lem1  11306  ef01bndlem  12464  cos2bnd  12468  sin4lt0  12475  dvdslelem  12573  divalglem1  12593  divalglem6  12597  sincosq3sgn  19868  sincosq4sgn  19869  sincos4thpi  19881  efif1olem1  19904  efif1olem2  19905  efif1olem4  19907  efif1o  19908  efifo  19909  ang180lem1  20107  ang180lem2  20108  log2ublem1  20242  log2ublem2  20243  bpos1lem  20521  bposlem7  20529  bposlem8  20530  bposlem9  20531  chebbnd1lem3  20620  chebbnd1  20621  chto1ub  20625  siilem1  21429  normlem6  21694  normlem7  21695  norm-ii-i  21716  normpar2i  21735  bcsiALT  21758  nmopadjlem  22669  nmopcoi  22675  bdopcoi  22678  nmopcoadji  22681  unierri  22684  circum  24007  stirlinglem11  27833
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulrcl 8800
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator