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

Theorem remulcli 10014
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 9981 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 707 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  (class class class)co 6615  cr 9895   · cmul 9901
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9959
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  ledivp1i  10909  ltdivp1i  10910  addltmul  11228  nn0lele2xi  11308  numltc  11488  decleOLD  11503  nn0opthlem2  13012  faclbnd4lem1  13036  ef01bndlem  14858  cos2bnd  14862  sin4lt0  14869  dvdslelem  14974  divalglem1  15060  divalglem6  15064  sincosq3sgn  24190  sincosq4sgn  24191  sincos4thpi  24203  efif1olem1  24226  efif1olem2  24227  efif1olem4  24229  efif1o  24230  efifo  24231  ang180lem1  24473  ang180lem2  24474  log2ublem1  24607  log2ublem2  24608  bpos1lem  24941  bposlem7  24949  bposlem8  24950  bposlem9  24951  chebbnd1lem3  25094  chebbnd1  25095  chto1ub  25099  siilem1  27594  normlem6  27860  normlem7  27861  norm-ii-i  27882  bcsiALT  27924  nmopadjlem  28836  nmopcoi  28842  bdopcoi  28845  nmopcoadji  28848  unierri  28851  problem5  31324  circum  31329  iexpire  31382  taupi  32841  sin2h  33070  tan2h  33072  sumnnodd  39298  sinaover2ne0  39414  stirlinglem11  39638  dirkerper  39650  dirkercncflem2  39658  dirkercncflem4  39660  fourierdlem24  39685  fourierdlem43  39704  fourierdlem44  39705  fourierdlem68  39728  fourierdlem94  39754  fourierdlem111  39771  fourierdlem113  39773  sqwvfoura  39782  sqwvfourb  39783  fourierswlem  39784  fouriersw  39785  lighneallem4a  40854  tgoldbach  41023  tgoldbachOLD  41030
  Copyright terms: Public domain W3C validator