---

Step * of Lemma summand-qle-sum

∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ].  ∀[i:{a..b-}]. (E[i] ≤ Σa ≤ j < b. E[j]) supposing ∀j:{a..b-}. (0 ≤ E[j])
BY
{ (Auto
   THEN (InstLemma `qsum-delta` [⌜a⌝;⌜b⌝;⌜E⌝;⌜i⌝]⋅ THENA Auto)
   THEN SplitOnHypITE -1 
   THEN Auto
   THEN Try ((D -1 THEN Complete (Auto'⋅)))
   THEN (RevHypSubst' -3 0 THENA Auto)
   THEN BLemma `qsum-qle`
   THEN Auto) }

1
1. a : ℤ
2. b : ℤ
3. E : {a..b-} ⟶ ℚ
4. ∀j:{a..b-}. (0 ≤ E[j])
5. i : {a..b-}
6. Σa ≤ j < b. E[j] * delta(i;j) = E[i] ∈ ℚ
7. a ≤ i
8. i < b
9. j : ℤ
10. a ≤ j
11. j < b
⊢ (E[j] * delta(i;j)) ≤ E[j]

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[E:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].
    \mforall{}[i:\{a..b\msupminus{}\}].  (E[i]  \mleq{}  \mSigma{}a  \mleq{}  j  <  b.  E[j])  supposing  \mforall{}j:\{a..b\msupminus{}\}.  (0  \mleq{}  E[j])


By

---

Latex:
(Auto
  THEN  (InstLemma  `qsum-delta`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SplitOnHypITE  -1 
  THEN  Auto
  THEN  Try  ((D  -1  THEN  Complete  (Auto'\mcdot{})))
  THEN  (RevHypSubst'  -3  0  THENA  Auto)
  THEN  BLemma  `qsum-qle`
  THEN  Auto)

---

Home Index