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

Theorem remulcli 10246
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 10213 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 710 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  (class class class)co 6813  cr 10127   · cmul 10133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10191
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  ledivp1i  11141  ltdivp1i  11142  addltmul  11460  nn0lele2xi  11540  numltc  11720  decleOLD  11735  nn0opthlem2  13250  faclbnd4lem1  13274  ef01bndlem  15113  cos2bnd  15117  sin4lt0  15124  dvdslelem  15233  divalglem1  15319  divalglem6  15323  sincosq3sgn  24451  sincosq4sgn  24452  sincos4thpi  24464  efif1olem1  24487  efif1olem2  24488  efif1olem4  24490  efif1o  24491  efifo  24492  ang180lem1  24738  ang180lem2  24739  log2ublem1  24872  log2ublem2  24873  bpos1lem  25206  bposlem7  25214  bposlem8  25215  bposlem9  25216  chebbnd1lem3  25359  chebbnd1  25360  chto1ub  25364  siilem1  28015  normlem6  28281  normlem7  28282  norm-ii-i  28303  bcsiALT  28345  nmopadjlem  29257  nmopcoi  29263  bdopcoi  29266  nmopcoadji  29269  unierri  29272  dpmul4  29931  hgt750lem  31038  hgt750lem2  31039  hgt750leme  31045  problem5  31870  circum  31875  iexpire  31928  taupi  33480  sin2h  33712  tan2h  33714  sumnnodd  40365  sinaover2ne0  40582  stirlinglem11  40804  dirkerper  40816  dirkercncflem2  40824  dirkercncflem4  40826  fourierdlem24  40851  fourierdlem43  40870  fourierdlem44  40871  fourierdlem68  40894  fourierdlem94  40920  fourierdlem111  40937  fourierdlem113  40939  sqwvfoura  40948  sqwvfourb  40949  fourierswlem  40950  fouriersw  40951  lighneallem4a  42035  tgoldbach  42215  tgoldbachOLD  42222
  Copyright terms: Public domain W3C validator