---

Step * 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
⊢ |a_∫-y f[t] dt - a_∫-x f[t] dt - f[x] * (y - x)| = |x_∫-y f[t] - f[x] dt|
BY
{ (((FLemma `rmin-rmax-subinterval` [-2;-1] THENA Auto)
    THEN (Assert a ∈ I BY
                (DVar `a' THEN Unhide THEN Auto))
    THEN (FLemma `rmin-rmax-subinterval` [-1;-4] THENA Auto)
    THEN (FLemma `rmin-rmax-subinterval` [-2;-4] THENA Auto)
    THEN (Assert ∀u,v:ℝ.  ([u, v] ⊆ I  ⇒ ifun(f;[u, v])) BY
                (Auto
                 THEN D 0
                 THEN Reduce 0
                 THEN Auto
                 THEN DVar `f'
                 THEN (Unhide THENA Auto)
                 THEN BackThruSomeHyp
                 THEN Auto))
    THEN (Assert a_∫-y f[t] dt ∈ ℝ BY
                Auto)
    THEN (Assert a_∫-x f[t] dt ∈ ℝ BY
                Auto)
    THEN (Assert x_∫-y f[t] dt ∈ ℝ BY
                Auto)
    THEN (Assert x_∫-y f[t] - f[x] dt ∈ ℝ BY
                (Auto THEN nRAdd ⌜f x⌝ 0⋅ THEN Auto)))
   THEN (InstLemma `integral-additive` [⌜a⌝;⌜y⌝;⌜x⌝]⋅ THENA Auto)
   ) }

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

---

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
\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:
(((FLemma  `rmin-rmax-subinterval`  [-2;-1]  THENA  Auto)
    THEN  (Assert  a  \mmember{}  I  BY
                            (DVar  `a'  THEN  Unhide  THEN  Auto))
    THEN  (FLemma  `rmin-rmax-subinterval`  [-1;-4]  THENA  Auto)
    THEN  (FLemma  `rmin-rmax-subinterval`  [-2;-4]  THENA  Auto)
    THEN  (Assert  \mforall{}u,v:\mBbbR{}.    ([u,  v]  \msubseteq{}  I    {}\mRightarrow{}  ifun(f;[u,  v]))  BY
                            (Auto
                              THEN  D  0
                              THEN  Reduce  0
                              THEN  Auto
                              THEN  DVar  `f'
                              THEN  (Unhide  THENA  Auto)
                              THEN  BackThruSomeHyp
                              THEN  Auto))
    THEN  (Assert  a\_\mint{}\msupminus{}y  f[t]  dt  \mmember{}  \mBbbR{}  BY
                            Auto)
    THEN  (Assert  a\_\mint{}\msupminus{}x  f[t]  dt  \mmember{}  \mBbbR{}  BY
                            Auto)
    THEN  (Assert  x\_\mint{}\msupminus{}y  f[t]  dt  \mmember{}  \mBbbR{}  BY
                            Auto)
    THEN  (Assert  x\_\mint{}\msupminus{}y  f[t]  -  f[x]  dt  \mmember{}  \mBbbR{}  BY
                            (Auto  THEN  nRAdd  \mkleeneopen{}f  x\mkleeneclose{}  0\mcdot{}  THEN  Auto)))
  THEN  (InstLemma  `integral-additive`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index