---

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 2 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))
11. rmaximum(0;0;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]) ≤ d
12. 2 ≤ ||L2||
⊢ rmaximum(0;||L2|| - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]) ≤ d
BY
{ ((InstHyp [⌜0⌝] (-3)⋅ THENA Auto) THEN (RWO "-1" 0 THENA Auto)) }

1
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))
11. rmaximum(0;0;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]) ≤ d
12. 2 ≤ ||L2||
13. rmaximum(0;||L2|| - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1])
= rmax(rmaximum(0;0;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]);rmaximum(0 + 1;||L2|| 
  - 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]))
⊢ rmax(rmaximum(0;0;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1]);rmaximum(0 + 1;||L2|| 
- 1;i.L1 @ L2[(i + (||L1|| - 2) + 1) + 1] - L1 @ L2[i + (||L1|| - 2) + 1])) ≤ 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))
11.  rmaximum(0;0;i.L1  @  L2[(i  +  (||L1||  -  2)  +  1)  +  1]  -  L1  @  L2[i  +  (||L1||  -  2)  +  1])  \mleq{}  d
12.  2  \mleq{}  ||L2||
\mvdash{}  rmaximum(0;||L2||  -  1;i.L1  @  L2[(i  +  (||L1||  -  2)  +  1)  +  1]  -  L1  @  L2[i  +  (||L1||  -  2)  +  1])  \mleq{}  d


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index