---

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

.....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))])} 
BY
{ (DVar `f' THEN (InstLemma `rmin3-rmax3-subinterval` [⌜I⌝;⌜a⌝;⌜y⌝;⌜x⌝]⋅ THENA Auto) THEN MemTypeCD THEN Auto) }

1
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))

---

Latex:

---

Latex:
.....wf..... 
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{}  f  \mmember{}  \{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))])\} 


By

---

Latex:
(DVar  `f'
  THEN  (InstLemma  `rmin3-rmax3-subinterval`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index