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

Theorem remulcli 9421
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 9388 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3mp2an 672 1  |-  ( A  x.  B )  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756  (class class class)co 6112   RRcr 9302    x. cmul 9308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9366
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ledivp1i  10279  ltdivp1i  10280  addltmul  10581  nn0lele2xi  10653  numltc  10796  nn0opthlem2  12068  faclbnd4lem1  12090  ef01bndlem  13489  cos2bnd  13493  sin4lt0  13500  dvdslelem  13598  divalglem1  13619  divalglem6  13623  sincosq3sgn  21984  sincosq4sgn  21985  sincos4thpi  21997  efif1olem1  22020  efif1olem2  22021  efif1olem4  22023  efif1o  22024  efifo  22025  ang180lem1  22227  ang180lem2  22228  log2ublem1  22363  log2ublem2  22364  bpos1lem  22643  bposlem7  22651  bposlem8  22652  bposlem9  22653  chebbnd1lem3  22742  chebbnd1  22743  chto1ub  22747  siilem1  24273  normlem6  24539  normlem7  24540  norm-ii-i  24561  normpar2i  24580  bcsiALT  24603  nmopadjlem  25515  nmopcoi  25521  bdopcoi  25524  nmopcoadji  25527  unierri  25530  problem5  27324  circum  27341  sin2h  28448  tan2h  28450  stirlinglem11  29905  taupi  35713
  Copyright terms: Public domain W3C validator