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

Theorem remulcli 9387
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 9354 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3mp2an 665 1  |-  ( A  x.  B )  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755  (class class class)co 6080   RRcr 9268    x. cmul 9274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9332
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ledivp1i  10245  ltdivp1i  10246  addltmul  10547  nn0lele2xi  10619  numltc  10762  nn0opthlem2  12030  faclbnd4lem1  12052  ef01bndlem  13450  cos2bnd  13454  sin4lt0  13461  dvdslelem  13559  divalglem1  13580  divalglem6  13584  sincosq3sgn  21846  sincosq4sgn  21847  sincos4thpi  21859  efif1olem1  21882  efif1olem2  21883  efif1olem4  21885  efif1o  21886  efifo  21887  ang180lem1  22089  ang180lem2  22090  log2ublem1  22225  log2ublem2  22226  bpos1lem  22505  bposlem7  22513  bposlem8  22514  bposlem9  22515  chebbnd1lem3  22604  chebbnd1  22605  chto1ub  22609  siilem1  24073  normlem6  24339  normlem7  24340  norm-ii-i  24361  normpar2i  24380  bcsiALT  24403  nmopadjlem  25315  nmopcoi  25321  bdopcoi  25324  nmopcoadji  25327  unierri  25330  problem5  27149  circum  27165  sin2h  28263  tan2h  28265  stirlinglem11  29722  taupi  35187
  Copyright terms: Public domain W3C validator