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

Theorem remulcli 9601
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 9568 . 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 1762  (class class class)co 6277   RRcr 9482    x. cmul 9488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9546
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ledivp1i  10462  ltdivp1i  10463  addltmul  10765  nn0lele2xi  10839  numltc  10987  nn0opthlem2  12306  faclbnd4lem1  12328  ef01bndlem  13771  cos2bnd  13775  sin4lt0  13782  dvdslelem  13880  divalglem1  13902  divalglem6  13906  sincosq3sgn  22621  sincosq4sgn  22622  sincos4thpi  22634  efif1olem1  22657  efif1olem2  22658  efif1olem4  22660  efif1o  22661  efifo  22662  ang180lem1  22864  ang180lem2  22865  log2ublem1  23000  log2ublem2  23001  bpos1lem  23280  bposlem7  23288  bposlem8  23289  bposlem9  23290  chebbnd1lem3  23379  chebbnd1  23380  chto1ub  23384  siilem1  25430  normlem6  25696  normlem7  25697  norm-ii-i  25718  normpar2i  25737  bcsiALT  25760  nmopadjlem  26672  nmopcoi  26678  bdopcoi  26681  nmopcoadji  26684  unierri  26687  problem5  28486  circum  28503  sin2h  29611  tan2h  29613  sumnnodd  31129  sinaover2ne0  31161  stirlinglem11  31341  dirkerper  31353  dirkercncflem2  31361  dirkercncflem4  31363  fourierdlem24  31388  fourierdlem43  31407  fourierdlem44  31408  fourierdlem68  31432  fourierdlem94  31458  fourierdlem111  31475  fourierdlem113  31477  sqwvfoura  31486  sqwvfourb  31487  fourierswlem  31488  fouriersw  31489  taupi  36646
  Copyright terms: Public domain W3C validator