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

Theorem remulcli 11234
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 11197 . 2 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
41, 2, 3mp2an 689 1 (๐ด ยท ๐ต) โˆˆ โ„
Colors of variables: wff setvar class
Syntax hints:   โˆˆ wcel 2098  (class class class)co 7405  โ„cr 11111   ยท cmul 11117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11175
This theorem depends on definitions:  df-bi 206  df-an 396
This theorem is referenced by:  ledivp1i  12143  ltdivp1i  12144  addltmul  12452  nn0lele2xi  12531  10re  12700  numltc  12707  nn0opthlem2  14234  faclbnd4lem1  14258  ef01bndlem  16134  cos2bnd  16138  sin4lt0  16145  dvdslelem  16259  divalglem1  16344  divalglem6  16348  sincosq3sgn  26390  sincosq4sgn  26391  sincos4thpi  26403  cos02pilt1  26415  cosq34lt1  26416  cos0pilt1  26421  efif1olem1  26431  efif1olem2  26432  efif1olem4  26434  efif1o  26435  efifo  26436  ang180lem1  26696  ang180lem2  26697  log2ublem1  26833  log2ublem2  26834  bpos1lem  27170  bposlem7  27178  bposlem8  27179  bposlem9  27180  chebbnd1lem3  27359  chebbnd1  27360  chto1ub  27364  siilem1  30613  normlem6  30877  normlem7  30878  norm-ii-i  30899  bcsiALT  30941  nmopadjlem  31851  nmopcoi  31857  bdopcoi  31860  nmopcoadji  31863  unierri  31866  dpmul4  32585  hgt750lem  34192  hgt750lem2  34193  hgt750leme  34199  problem5  35182  circum  35187  iexpire  35238  taupi  36711  sin2h  36991  tan2h  36993  sumnnodd  44918  sinaover2ne0  45156  stirlinglem11  45372  dirkerper  45384  dirkercncflem2  45392  dirkercncflem4  45394  fourierdlem24  45419  fourierdlem43  45438  fourierdlem44  45439  fourierdlem68  45462  fourierdlem94  45488  fourierdlem111  45505  fourierdlem113  45507  sqwvfoura  45516  sqwvfourb  45517  fourierswlem  45518  fouriersw  45519  lighneallem4a  46848  tgoldbach  47057
  Copyright terms: Public domain W3C validator