---

Step * of Lemma rng_minus_sum

∀[r:Rng]. ∀[a,b:ℤ].
  ∀[F:{a..b-} ⟶ |r|]. ((-r (Σ(r) a ≤ i < b. F[i])) = (Σ(r) a ≤ i < b. -r F[i]) ∈ |r|) supposing a ≤ b
BY
{ (((Auto THEN InstLemma `rng_times_sum_l` [⌜r⌝;⌜a⌝;⌜b⌝;⌜F⌝;⌜-r 1⌝]⋅) THENA Auto) THEN NthHypEq (-1) THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. r : Rng
2. a : ℤ
3. b : ℤ
4. a ≤ b
5. F : {a..b-} ⟶ |r|
6. ((-r 1) * (Σ(r) a ≤ j < b. F[j])) = (Σ(r) a ≤ j < b. (-r 1) * F[j]) ∈ |r|
⊢ (-r (Σ(r) a ≤ i < b. F[i])) = ((-r 1) * (Σ(r) a ≤ j < b. F[j])) ∈ |r|

2
.....subterm..... T:t
3:n
1. r : Rng
2. a : ℤ
3. b : ℤ
4. a ≤ b
5. F : {a..b-} ⟶ |r|
6. ((-r 1) * (Σ(r) a ≤ j < b. F[j])) = (Σ(r) a ≤ j < b. (-r 1) * F[j]) ∈ |r|
⊢ (Σ(r) a ≤ i < b. -r F[i]) = (Σ(r) a ≤ j < b. (-r 1) * F[j]) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:\mBbbZ{}].
    \mforall{}[F:\{a..b\msupminus{}\}  {}\mrightarrow{}  |r|].  ((-r  (\mSigma{}(r)  a  \mleq{}  i  <  b.  F[i]))  =  (\mSigma{}(r)  a  \mleq{}  i  <  b.  -r  F[i]))  supposing  a  \mleq{}  b


By

---

Latex:
(((Auto  THEN  InstLemma  `rng\_times\_sum\_l`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}-r  1\mkleeneclose{}]\mcdot{})  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCDA)

---

Home Index