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

Theorem remulcli 9560
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 9527 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3mp2an 670 1  |-  ( A  x.  B )  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842  (class class class)co 6234   RRcr 9441    x. cmul 9447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9505
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  ledivp1i  10431  ltdivp1i  10432  addltmul  10735  nn0lele2xi  10809  numltc  10959  nn0opthlem2  12303  faclbnd4lem1  12325  ef01bndlem  14020  cos2bnd  14024  sin4lt0  14031  dvdslelem  14131  divalglem1  14153  divalglem6  14157  sincosq3sgn  23077  sincosq4sgn  23078  sincos4thpi  23090  efif1olem1  23113  efif1olem2  23114  efif1olem4  23116  efif1o  23117  efifo  23118  ang180lem1  23360  ang180lem2  23361  log2ublem1  23494  log2ublem2  23495  bpos1lem  23830  bposlem7  23838  bposlem8  23839  bposlem9  23840  chebbnd1lem3  23929  chebbnd1  23930  chto1ub  23934  siilem1  26060  normlem6  26326  normlem7  26327  norm-ii-i  26348  bcsiALT  26390  nmopadjlem  27301  nmopcoi  27307  bdopcoi  27310  nmopcoadji  27313  unierri  27316  problem5  29756  circum  29773  iexpire  29830  taupi  31237  sin2h  31398  tan2h  31400  sumnnodd  36986  sinaover2ne0  37018  stirlinglem11  37216  dirkerper  37228  dirkercncflem2  37236  dirkercncflem4  37238  fourierdlem24  37263  fourierdlem43  37282  fourierdlem44  37283  fourierdlem68  37307  fourierdlem94  37333  fourierdlem111  37350  fourierdlem113  37352  sqwvfoura  37361  sqwvfourb  37362  fourierswlem  37363  fouriersw  37364
  Copyright terms: Public domain W3C validator