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

Theorem remulcli 9659
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 9626 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3mp2an 677 1  |-  ( A  x.  B )  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869  (class class class)co 6303   RRcr 9540    x. cmul 9546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9604
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  ledivp1i  10534  ltdivp1i  10535  addltmul  10850  nn0lele2xi  10924  numltc  11073  nn0opthlem2  12456  faclbnd4lem1  12479  ef01bndlem  14231  cos2bnd  14235  sin4lt0  14242  dvdslelem  14342  divalglem1  14365  divalglem6  14371  sincosq3sgn  23447  sincosq4sgn  23448  sincos4thpi  23460  efif1olem1  23483  efif1olem2  23484  efif1olem4  23486  efif1o  23487  efifo  23488  ang180lem1  23730  ang180lem2  23731  log2ublem1  23864  log2ublem2  23865  bpos1lem  24202  bposlem7  24210  bposlem8  24211  bposlem9  24212  chebbnd1lem3  24301  chebbnd1  24302  chto1ub  24306  siilem1  26484  normlem6  26760  normlem7  26761  norm-ii-i  26782  bcsiALT  26824  nmopadjlem  27734  nmopcoi  27740  bdopcoi  27743  nmopcoadji  27746  unierri  27749  problem5  30303  circum  30320  iexpire  30372  taupi  31682  sin2h  31855  tan2h  31857  sumnnodd  37536  sinaover2ne0  37569  stirlinglem11  37772  dirkerper  37784  dirkercncflem2  37792  dirkercncflem4  37794  fourierdlem24  37819  fourierdlem43  37840  fourierdlem44  37841  fourierdlem68  37864  fourierdlem94  37890  fourierdlem111  37907  fourierdlem113  37909  sqwvfoura  37918  sqwvfourb  37919  fourierswlem  37920  fouriersw  37921  tgoldbach  38629
  Copyright terms: Public domain W3C validator