---

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


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
{ ((BLemma `qle_weakening_eq_qorder` THEN Auto) THEN EqCD THEN Auto) }

1
.....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] ∈ ℚ

---

Latex:

---

Latex:

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]|  \mleq{}  |\mSigma{}0  \mleq{}  j  <  b  -  a.  E[a  +  j]|


By

---

Latex:
((BLemma  `qle\_weakening\_eq\_qorder`  THEN  Auto)  THEN  EqCD  THEN  Auto)

---

Home Index