---

Step * 1 3 1 of Lemma harmonic-series-diverges

.....assertion..... 
1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
4. k ≤ (2^k - 1)
⊢ (Σ{(r1/r(i + 1)) | 0≤i≤2^(k + 1) - 1} - Σ{(r1/r(i + 1)) | 0≤i≤2^k - 1}) = Σ{(r1/r(i + 1)) | 2^k≤i≤2^(k + 1) - 1}
BY
{ (InstLemma `rsum-split` [⌜0⌝;⌜2^(k + 1) - 1⌝;⌜λ2i.(r1/r(i + 1))⌝;⌜2^k - 1⌝]⋅ THEN Auto THEN Auto) }

1
.....antecedent..... 
1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
4. k ≤ (2^k - 1)
⊢ (2^k - 1) ≤ (2^(k + 1) - 1)

2
1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
4. k ≤ (2^k - 1)
5. Σ{(r1/r(i + 1)) | 0≤i≤2^(k + 1) - 1}
= (Σ{(r1/r(i + 1)) | 0≤i≤2^k - 1} + Σ{(r1/r(i + 1)) | (2^k - 1) + 1≤i≤2^(k + 1) - 1})
⊢ (Σ{(r1/r(i + 1)) | 0≤i≤2^(k + 1) - 1} - Σ{(r1/r(i + 1)) | 0≤i≤2^k - 1}) = Σ{(r1/r(i + 1)) | 2^k≤i≤2^(k + 1) - 1}

---

Latex:

---

Latex:
.....assertion..... 
1.  r0  <  (r1/r(2))
2.  k  :  \mBbbN{}
3.  k  \mleq{}  (2\^{}(k  +  1)  -  1)
4.  k  \mleq{}  (2\^{}k  -  1)
\mvdash{}  (\mSigma{}\{(r1/r(i  +  1))  |  0\mleq{}i\mleq{}2\^{}(k  +  1)  -  1\}  -  \mSigma{}\{(r1/r(i  +  1))  |  0\mleq{}i\mleq{}2\^{}k  -  1\})
=  \mSigma{}\{(r1/r(i  +  1))  |  2\^{}k\mleq{}i\mleq{}2\^{}(k  +  1)  -  1\}


By

---

Latex:
(InstLemma  `rsum-split`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}2\^{}(k  +  1)  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.(r1/r(i  +  1))\mkleeneclose{};\mkleeneopen{}2\^{}k  -  1\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Auto)

---

Home Index