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

Theorem remulcli 10650
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 10615 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 691 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  (class class class)co 7139  cr 10529   · cmul 10535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10593
This theorem depends on definitions:  df-bi 210  df-an 400
This theorem is referenced by:  ledivp1i  11558  ltdivp1i  11559  addltmul  11865  nn0lele2xi  11944  10re  12109  numltc  12116  nn0opthlem2  13629  faclbnd4lem1  13653  ef01bndlem  15533  cos2bnd  15537  sin4lt0  15544  dvdslelem  15655  divalglem1  15739  divalglem6  15743  sincosq3sgn  25097  sincosq4sgn  25098  sincos4thpi  25110  cos02pilt1  25122  cosq34lt1  25123  cos0pilt1  25128  efif1olem1  25138  efif1olem2  25139  efif1olem4  25141  efif1o  25142  efifo  25143  ang180lem1  25399  ang180lem2  25400  log2ublem1  25536  log2ublem2  25537  bpos1lem  25870  bposlem7  25878  bposlem8  25879  bposlem9  25880  chebbnd1lem3  26059  chebbnd1  26060  chto1ub  26064  siilem1  28638  normlem6  28902  normlem7  28903  norm-ii-i  28924  bcsiALT  28966  nmopadjlem  29876  nmopcoi  29882  bdopcoi  29885  nmopcoadji  29888  unierri  29891  dpmul4  30620  hgt750lem  32036  hgt750lem2  32037  hgt750leme  32043  problem5  33026  circum  33031  iexpire  33081  taupi  34738  sin2h  35046  tan2h  35048  3lexlogpow5ineq1  39340  sumnnodd  42269  sinaover2ne0  42507  stirlinglem11  42723  dirkerper  42735  dirkercncflem2  42743  dirkercncflem4  42745  fourierdlem24  42770  fourierdlem43  42789  fourierdlem44  42790  fourierdlem68  42813  fourierdlem94  42839  fourierdlem111  42856  fourierdlem113  42858  sqwvfoura  42867  sqwvfourb  42868  fourierswlem  42869  fouriersw  42870  lighneallem4a  44123  tgoldbach  44332
  Copyright terms: Public domain W3C validator