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

Theorem remulcli 10508
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 10473 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 688 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2081  (class class class)co 7021  cr 10387   · cmul 10393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10451
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  ledivp1i  11418  ltdivp1i  11419  addltmul  11726  nn0lele2xi  11805  10re  11971  numltc  11978  nn0opthlem2  13484  faclbnd4lem1  13508  ef01bndlem  15375  cos2bnd  15379  sin4lt0  15386  dvdslelem  15497  divalglem1  15583  divalglem6  15587  sincosq3sgn  24774  sincosq4sgn  24775  sincos4thpi  24787  efif1olem1  24812  efif1olem2  24813  efif1olem4  24815  efif1o  24816  efifo  24817  ang180lem1  25073  ang180lem2  25074  log2ublem1  25211  log2ublem2  25212  bpos1lem  25545  bposlem7  25553  bposlem8  25554  bposlem9  25555  chebbnd1lem3  25734  chebbnd1  25735  chto1ub  25739  siilem1  28324  normlem6  28588  normlem7  28589  norm-ii-i  28610  bcsiALT  28652  nmopadjlem  29562  nmopcoi  29568  bdopcoi  29571  nmopcoadji  29574  unierri  29577  dpmul4  30279  hgt750lem  31544  hgt750lem2  31545  hgt750leme  31551  problem5  32526  circum  32531  iexpire  32581  taupi  34160  sin2h  34438  tan2h  34440  sumnnodd  41478  sinaover2ne0  41716  stirlinglem11  41937  dirkerper  41949  dirkercncflem2  41957  dirkercncflem4  41959  fourierdlem24  41984  fourierdlem43  42003  fourierdlem44  42004  fourierdlem68  42027  fourierdlem94  42053  fourierdlem111  42070  fourierdlem113  42072  sqwvfoura  42081  sqwvfourb  42082  fourierswlem  42083  fouriersw  42084  lighneallem4a  43281  tgoldbach  43490
  Copyright terms: Public domain W3C validator