---

Step * 1 1 1 1 of Lemma derivative-of-integral


1. I : Interval
2. a : {a:ℝ| a ∈ I} 
3. f : {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))} 
4. k : ℕ+
5. n : ℕ+
6. icompact(i-approx(I;n))
7. iproper(i-approx(I;n))
8. x : ℝ
9. y : ℝ
10. x ∈ I
11. y ∈ I
12. [rmin(x;y), rmax(x;y)] ⊆ I 
13. a ∈ I
14. [rmin(a;x), rmax(a;x)] ⊆ I 
15. [rmin(a;y), rmax(a;y)] ⊆ I 
16. ∀u,v:ℝ.  ([u, v] ⊆ I  ⇒ ifun(f;[u, v]))
17. a_∫-y f[t] dt ∈ ℝ
18. a_∫-x f[t] dt ∈ ℝ
19. x_∫-y f[t] dt ∈ ℝ
20. x_∫-y f[t] - f[x] dt ∈ ℝ
21. ∀[f:{f:[rmin(a;rmin(y;x)), rmax(a;rmax(y;x))] ⟶ℝ| ifun(f;[rmin(a;rmin(y;x)), rmax(a;rmax(y;x))])} ]
      (a_∫-y f[x] dx = (a_∫-x f[x] dx + x_∫-y f[x] dx))
⊢ |a_∫-y f[t] dt - a_∫-x f[t] dt - f[x] * (y - x)| = |x_∫-y f[t] - f[x] dt|
BY
{ (InstHyp [⌜f⌝] (-1)⋅ THENM Thin (-2)) }

1
.....wf..... 
1. I : Interval
2. a : {a:ℝ| a ∈ I} 
3. f : {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))} 
4. k : ℕ+
5. n : ℕ+
6. icompact(i-approx(I;n))
7. iproper(i-approx(I;n))
8. x : ℝ
9. y : ℝ
10. x ∈ I
11. y ∈ I
12. [rmin(x;y), rmax(x;y)] ⊆ I 
13. a ∈ I
14. [rmin(a;x), rmax(a;x)] ⊆ I 
15. [rmin(a;y), rmax(a;y)] ⊆ I 
16. ∀u,v:ℝ.  ([u, v] ⊆ I  ⇒ ifun(f;[u, v]))
17. a_∫-y f[t] dt ∈ ℝ
18. a_∫-x f[t] dt ∈ ℝ
19. x_∫-y f[t] dt ∈ ℝ
20. x_∫-y f[t] - f[x] dt ∈ ℝ
21. ∀[f:{f:[rmin(a;rmin(y;x)), rmax(a;rmax(y;x))] ⟶ℝ| ifun(f;[rmin(a;rmin(y;x)), rmax(a;rmax(y;x))])} ]
      (a_∫-y f[x] dx = (a_∫-x f[x] dx + x_∫-y f[x] dx))
⊢ f ∈ {f:[rmin(a;rmin(y;x)), rmax(a;rmax(y;x))] ⟶ℝ| ifun(f;[rmin(a;rmin(y;x)), rmax(a;rmax(y;x))])} 

2
1. I : Interval
2. a : {a:ℝ| a ∈ I} 
3. f : {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))} 
4. k : ℕ+
5. n : ℕ+
6. icompact(i-approx(I;n))
7. iproper(i-approx(I;n))
8. x : ℝ
9. y : ℝ
10. x ∈ I
11. y ∈ I
12. [rmin(x;y), rmax(x;y)] ⊆ I 
13. a ∈ I
14. [rmin(a;x), rmax(a;x)] ⊆ I 
15. [rmin(a;y), rmax(a;y)] ⊆ I 
16. ∀u,v:ℝ.  ([u, v] ⊆ I  ⇒ ifun(f;[u, v]))
17. a_∫-y f[t] dt ∈ ℝ
18. a_∫-x f[t] dt ∈ ℝ
19. x_∫-y f[t] dt ∈ ℝ
20. x_∫-y f[t] - f[x] dt ∈ ℝ
21. a_∫-y f[x] dx = (a_∫-x f[x] dx + x_∫-y f[x] dx)
⊢ |a_∫-y f[t] dt - a_∫-x f[t] dt - f[x] * (y - x)| = |x_∫-y f[t] - f[x] dt|

---

Latex:

---

Latex:

1.  I  :  Interval
2.  a  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
3.  f  :  \{f:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))\} 
4.  k  :  \mBbbN{}\msupplus{}
5.  n  :  \mBbbN{}\msupplus{}
6.  icompact(i-approx(I;n))
7.  iproper(i-approx(I;n))
8.  x  :  \mBbbR{}
9.  y  :  \mBbbR{}
10.  x  \mmember{}  I
11.  y  \mmember{}  I
12.  [rmin(x;y),  rmax(x;y)]  \msubseteq{}  I 
13.  a  \mmember{}  I
14.  [rmin(a;x),  rmax(a;x)]  \msubseteq{}  I 
15.  [rmin(a;y),  rmax(a;y)]  \msubseteq{}  I 
16.  \mforall{}u,v:\mBbbR{}.    ([u,  v]  \msubseteq{}  I    {}\mRightarrow{}  ifun(f;[u,  v]))
17.  a\_\mint{}\msupminus{}y  f[t]  dt  \mmember{}  \mBbbR{}
18.  a\_\mint{}\msupminus{}x  f[t]  dt  \mmember{}  \mBbbR{}
19.  x\_\mint{}\msupminus{}y  f[t]  dt  \mmember{}  \mBbbR{}
20.  x\_\mint{}\msupminus{}y  f[t]  -  f[x]  dt  \mmember{}  \mBbbR{}
21.  \mforall{}[f:\{f:[rmin(a;rmin(y;x)),  rmax(a;rmax(y;x))]  {}\mrightarrow{}\mBbbR{}| 
                  ifun(f;[rmin(a;rmin(y;x)),  rmax(a;rmax(y;x))])\}  ]
            (a\_\mint{}\msupminus{}y  f[x]  dx  =  (a\_\mint{}\msupminus{}x  f[x]  dx  +  x\_\mint{}\msupminus{}y  f[x]  dx))
\mvdash{}  |a\_\mint{}\msupminus{}y  f[t]  dt  -  a\_\mint{}\msupminus{}x  f[t]  dt  -  f[x]  *  (y  -  x)|  =  |x\_\mint{}\msupminus{}y  f[t]  -  f[x]  dt|


By

---

Latex:
(InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-1)\mcdot{}  THENM  Thin  (-2))

---

Home Index