---

Step * 2 1 1 1 of Lemma qabs-qsum-qle

.....subterm..... T:t
1:n
1. ∀n:ℕ. ∀[E:ℕn ⟶ ℚ]. ∀[x:ℚ].  |Σ0 ≤ j < n. E[j]| ≤ (n * x) supposing ∀j:ℕn. (|E[j]| ≤ x)
2. a : ℤ
3. b : ℤ
4. E : {a..b-} ⟶ ℚ
5. x : ℚ
6. a ≤ b
7. ∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (|E[j]| ≤ x))
8. |Σ0 ≤ j < b - a. E[a + j]| ≤ ((b - a) * x)
⊢ Σa ≤ j < b. E[j] = Σ0 ≤ j < b - a. E[a + j] ∈ ℚ
BY
{ (InstLemma `sum_shift_q` [⌜a⌝;⌜b⌝;⌜E⌝;⌜-a⌝]⋅ THENA Auto) }

1
1. ∀n:ℕ. ∀[E:ℕn ⟶ ℚ]. ∀[x:ℚ].  |Σ0 ≤ j < n. E[j]| ≤ (n * x) supposing ∀j:ℕn. (|E[j]| ≤ x)
2. a : ℤ
3. b : ℤ
4. E : {a..b-} ⟶ ℚ
5. x : ℚ
6. a ≤ b
7. ∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (|E[j]| ≤ x))
8. |Σ0 ≤ j < b - a. E[a + j]| ≤ ((b - a) * x)
9. Σa ≤ j < b. E[j] = Σa + (-a) ≤ j < b + (-a). E[j - -a] ∈ ℚ
⊢ Σa ≤ j < b. E[j] = Σ0 ≤ j < b - a. E[a + j] ∈ ℚ

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  \mforall{}n:\mBbbN{}.  \mforall{}[E:\mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[x:\mBbbQ{}].    |\mSigma{}0  \mleq{}  j  <  n.  E[j]|  \mleq{}  (n  *  x)  supposing  \mforall{}j:\mBbbN{}n.  (|E[j]|  \mleq{}  x)
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
5.  x  :  \mBbbQ{}
6.  a  \mleq{}  b
7.  \mforall{}j:\mBbbZ{}.  ((a  \mleq{}  j)  {}\mRightarrow{}  j  <  b  {}\mRightarrow{}  (|E[j]|  \mleq{}  x))
8.  |\mSigma{}0  \mleq{}  j  <  b  -  a.  E[a  +  j]|  \mleq{}  ((b  -  a)  *  x)
\mvdash{}  \mSigma{}a  \mleq{}  j  <  b.  E[j]  =  \mSigma{}0  \mleq{}  j  <  b  -  a.  E[a  +  j]


By

---

Latex:
(InstLemma  `sum\_shift\_q`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}-a\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index