---

Step * 2 1 1 1 1 2 1 2 2 1 1 1 2 1 1 1 1 1 1 1 1 2 1 1 1 1 1 1 1 1 of Lemma Riemann-integral-additive


1. c : ℝ
2. d : {d:ℝ| r0 < d} 
3. L1 : ℝ List
4. L2 : ℝ List
5. 2 ≤ ||L2||
6. 2 ≤ ||L1||
7. last(L1) = c ∈ ℝ
8. rmaximum(0;||L1|| - 2;i.L1[i + 1] - L1[i]) ≤ d
9. rmaximum(0;||L2|| - 1;i.[c / L2][i + 1] - [c / L2][i]) ≤ d
10. ∀[k:ℤ]
      (rmaximum(0;||L2|| - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1])
         = rmax(rmaximum(0;k;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]);rmaximum(k
           + 1;||L2|| - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]))) supposing 
         (k < ||L2|| - 1 and 
         (0 ≤ k))
⊢ (L1 @ L2[||L1||] - L1 @ L2[||L1|| - 1]) ≤ d
BY
{ Subst' L1 @ L2[||L1|| - 1] ~ last(L1) 0 }

1
.....equality..... 
1. c : ℝ
2. d : {d:ℝ| r0 < d} 
3. L1 : ℝ List
4. L2 : ℝ List
5. 2 ≤ ||L2||
6. 2 ≤ ||L1||
7. last(L1) = c ∈ ℝ
8. rmaximum(0;||L1|| - 2;i.L1[i + 1] - L1[i]) ≤ d
9. rmaximum(0;||L2|| - 1;i.[c / L2][i + 1] - [c / L2][i]) ≤ d
10. ∀[k:ℤ]
      (rmaximum(0;||L2|| - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1])
         = rmax(rmaximum(0;k;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]);rmaximum(k
           + 1;||L2|| - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]))) supposing 
         (k < ||L2|| - 1 and 
         (0 ≤ k))
⊢ L1 @ L2[||L1|| - 1] ~ last(L1)

2
1. c : ℝ
2. d : {d:ℝ| r0 < d} 
3. L1 : ℝ List
4. L2 : ℝ List
5. 2 ≤ ||L2||
6. 2 ≤ ||L1||
7. last(L1) = c ∈ ℝ
8. rmaximum(0;||L1|| - 2;i.L1[i + 1] - L1[i]) ≤ d
9. rmaximum(0;||L2|| - 1;i.[c / L2][i + 1] - [c / L2][i]) ≤ d
10. ∀[k:ℤ]
      (rmaximum(0;||L2|| - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1])
         = rmax(rmaximum(0;k;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]);rmaximum(k
           + 1;||L2|| - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]))) supposing 
         (k < ||L2|| - 1 and 
         (0 ≤ k))
⊢ (L1 @ L2[||L1||] - last(L1)) ≤ d

---

Latex:

---

Latex:

1.  c  :  \mBbbR{}
2.  d  :  \{d:\mBbbR{}|  r0  <  d\} 
3.  L1  :  \mBbbR{}  List
4.  L2  :  \mBbbR{}  List
5.  2  \mleq{}  ||L2||
6.  2  \mleq{}  ||L1||
7.  last(L1)  =  c
8.  rmaximum(0;||L1||  -  2;i.L1[i  +  1]  -  L1[i])  \mleq{}  d
9.  rmaximum(0;||L2||  -  1;i.[c  /  L2][i  +  1]  -  [c  /  L2][i])  \mleq{}  d
10.  \mforall{}[k:\mBbbZ{}]
            (rmaximum(0;||L2||  -  1;i.L1  @  L2[(i  +  (||L1||  -  2)  +  1)  +  1]  -  L1  @  L2[i  +  (||L1||  -  2)  +  1])
                  =  rmax(rmaximum(0;k;i.L1  @  L2[(i  +  (||L1||  -  2)  +  1)  +  1]  -  L1  @  L2[i
                      +  (||L1||  -  2)
                      +  1]);rmaximum(k  +  1;||L2||  -  1;i.L1  @  L2[(i  +  (||L1||  -  2)  +  1)  +  1]  -  L1  @  L2[i
                      +  (||L1||  -  2)
                      +  1])))  supposing 
                  (k  <  ||L2||  -  1  and 
                  (0  \mleq{}  k))
\mvdash{}  (L1  @  L2[||L1||]  -  L1  @  L2[||L1||  -  1])  \mleq{}  d


By

---

Latex:
Subst'  L1  @  L2[||L1||  -  1]  \msim{}  last(L1)  0

---

Home Index