---

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


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

---

Latex:

---

Latex:

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


By

---

Latex:
EAuto  2

---

Home Index