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

Theorem remulcli 9906
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 9873 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 703 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1975  (class class class)co 6523  cr 9787   · cmul 9793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9851
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  ledivp1i  10794  ltdivp1i  10795  addltmul  11111  nn0lele2xi  11191  numltc  11356  decleOLD  11371  nn0opthlem2  12869  faclbnd4lem1  12893  ef01bndlem  14695  cos2bnd  14699  sin4lt0  14706  dvdslelem  14811  divalglem1  14897  divalglem6  14901  sincosq3sgn  23969  sincosq4sgn  23970  sincos4thpi  23982  efif1olem1  24005  efif1olem2  24006  efif1olem4  24008  efif1o  24009  efifo  24010  ang180lem1  24252  ang180lem2  24253  log2ublem1  24386  log2ublem2  24387  bpos1lem  24720  bposlem7  24728  bposlem8  24729  bposlem9  24730  chebbnd1lem3  24873  chebbnd1  24874  chto1ub  24878  siilem1  26892  normlem6  27158  normlem7  27159  norm-ii-i  27180  bcsiALT  27222  nmopadjlem  28134  nmopcoi  28140  bdopcoi  28143  nmopcoadji  28146  unierri  28149  problem5  30619  circum  30624  iexpire  30676  taupi  32145  sin2h  32368  tan2h  32370  sumnnodd  38497  sinaover2ne0  38551  stirlinglem11  38777  dirkerper  38789  dirkercncflem2  38797  dirkercncflem4  38799  fourierdlem24  38824  fourierdlem43  38843  fourierdlem44  38844  fourierdlem68  38867  fourierdlem94  38893  fourierdlem111  38910  fourierdlem113  38912  sqwvfoura  38921  sqwvfourb  38922  fourierswlem  38923  fouriersw  38924  lighneallem4a  39864  tgoldbach  40033  tgoldbachOLD  40040
  Copyright terms: Public domain W3C validator