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

Theorem remulcli 11178
Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
Hypotheses
Ref Expression
recni.1 ๐ด โˆˆ โ„
axri.2 ๐ต โˆˆ โ„
Assertion
Ref Expression
remulcli (๐ด ยท ๐ต) โˆˆ โ„

Proof of Theorem remulcli
StepHypRef Expression
1 recni.1 . 2 ๐ด โˆˆ โ„
2 axri.2 . 2 ๐ต โˆˆ โ„
3 remulcl 11143 . 2 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
41, 2, 3mp2an 691 1 (๐ด ยท ๐ต) โˆˆ โ„
Colors of variables: wff setvar class
Syntax hints:   โˆˆ wcel 2107  (class class class)co 7362  โ„cr 11057   ยท cmul 11063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11121
This theorem depends on definitions:  df-bi 206  df-an 398
This theorem is referenced by:  ledivp1i  12087  ltdivp1i  12088  addltmul  12396  nn0lele2xi  12475  10re  12644  numltc  12651  nn0opthlem2  14176  faclbnd4lem1  14200  ef01bndlem  16073  cos2bnd  16077  sin4lt0  16084  dvdslelem  16198  divalglem1  16283  divalglem6  16287  sincosq3sgn  25873  sincosq4sgn  25874  sincos4thpi  25886  cos02pilt1  25898  cosq34lt1  25899  cos0pilt1  25904  efif1olem1  25914  efif1olem2  25915  efif1olem4  25917  efif1o  25918  efifo  25919  ang180lem1  26175  ang180lem2  26176  log2ublem1  26312  log2ublem2  26313  bpos1lem  26646  bposlem7  26654  bposlem8  26655  bposlem9  26656  chebbnd1lem3  26835  chebbnd1  26836  chto1ub  26840  siilem1  29835  normlem6  30099  normlem7  30100  norm-ii-i  30121  bcsiALT  30163  nmopadjlem  31073  nmopcoi  31079  bdopcoi  31082  nmopcoadji  31085  unierri  31088  dpmul4  31812  hgt750lem  33304  hgt750lem2  33305  hgt750leme  33311  problem5  34297  circum  34302  iexpire  34347  taupi  35823  sin2h  36097  tan2h  36099  sumnnodd  43945  sinaover2ne0  44183  stirlinglem11  44399  dirkerper  44411  dirkercncflem2  44419  dirkercncflem4  44421  fourierdlem24  44446  fourierdlem43  44465  fourierdlem44  44466  fourierdlem68  44489  fourierdlem94  44515  fourierdlem111  44532  fourierdlem113  44534  sqwvfoura  44543  sqwvfourb  44544  fourierswlem  44545  fouriersw  44546  lighneallem4a  45874  tgoldbach  46083
  Copyright terms: Public domain W3C validator