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

Theorem remulcli 10312
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 10276 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 683 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  (class class class)co 6844  cr 10190   · cmul 10196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10254
This theorem depends on definitions:  df-bi 198  df-an 385
This theorem is referenced by:  ledivp1i  11205  ltdivp1i  11206  addltmul  11516  nn0lele2xi  11597  10re  11762  numltc  11770  nn0opthlem2  13263  faclbnd4lem1  13287  ef01bndlem  15199  cos2bnd  15203  sin4lt0  15210  dvdslelem  15319  divalglem1  15402  divalglem6  15406  sincosq3sgn  24547  sincosq4sgn  24548  sincos4thpi  24560  efif1olem1  24583  efif1olem2  24584  efif1olem4  24586  efif1o  24587  efifo  24588  ang180lem1  24833  ang180lem2  24834  log2ublem1  24967  log2ublem2  24968  bpos1lem  25301  bposlem7  25309  bposlem8  25310  bposlem9  25311  chebbnd1lem3  25454  chebbnd1  25455  chto1ub  25459  siilem1  28165  normlem6  28431  normlem7  28432  norm-ii-i  28453  bcsiALT  28495  nmopadjlem  29407  nmopcoi  29413  bdopcoi  29416  nmopcoadji  29419  unierri  29422  dpmul4  30072  hgt750lem  31183  hgt750lem2  31184  hgt750leme  31190  problem5  32012  circum  32017  iexpire  32069  taupi  33606  sin2h  33826  tan2h  33828  sumnnodd  40503  sinaover2ne0  40720  stirlinglem11  40941  dirkerper  40953  dirkercncflem2  40961  dirkercncflem4  40963  fourierdlem24  40988  fourierdlem43  41007  fourierdlem44  41008  fourierdlem68  41031  fourierdlem94  41057  fourierdlem111  41074  fourierdlem113  41076  sqwvfoura  41085  sqwvfourb  41086  fourierswlem  41087  fouriersw  41088  lighneallem4a  42204  tgoldbach  42384
  Copyright terms: Public domain W3C validator