---

Step * 2 1 of Lemma Riemann-integral-additive


1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. c : ℝ
5. a ≤ c
6. c ≤ b
7. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
8. ∫ f[x] dx on [a, c] ∈ ℝ
9. ∫ f[x] dx on [c, b] ∈ ℝ
10. m : ℕ+
⊢ |∫ f[x] dx on [a, b] - ∫ f[x] dx on [a, c] + ∫ f[x] dx on [c, b]| ≤ (r1/r(m))
BY
{ ((Assert ifun(f;[a, b]) BY
          (DVar `f' THEN Unhide THEN Auto))
   THEN (Assert ifun(f;[a, c]) BY
               (RepeatFor 2 (ParallelLast) THEN Reduce -1 THEN Reduce 0 THEN RepeatFor 2 (ParallelLast) THEN Auto))
   THEN (Assert ifun(f;[c, b]) BY
               (Thin (-1)
                THEN RepeatFor 2 (ParallelLast)
                THEN Reduce -1
                THEN Reduce 0
                THEN RepeatFor 2 (ParallelLast)
                THEN Auto))) }

1
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. c : ℝ
5. a ≤ c
6. c ≤ b
7. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
8. ∫ f[x] dx on [a, c] ∈ ℝ
9. ∫ f[x] dx on [c, b] ∈ ℝ
10. m : ℕ+
11. ifun(f;[a, b])
12. ifun(f;[a, c])
13. ifun(f;[c, b])
⊢ |∫ f[x] dx on [a, b] - ∫ f[x] dx on [a, c] + ∫ f[x] dx on [c, b]| ≤ (r1/r(m))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  \mleq{}  b\} 
3.  f  :  \{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\} 
4.  c  :  \mBbbR{}
5.  a  \mleq{}  c
6.  c  \mleq{}  b
7.  \mlambda{}x.f[x]  \mmember{}  \{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\} 
8.  \mint{}  f[x]  dx  on  [a,  c]  \mmember{}  \mBbbR{}
9.  \mint{}  f[x]  dx  on  [c,  b]  \mmember{}  \mBbbR{}
10.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  |\mint{}  f[x]  dx  on  [a,  b]  -  \mint{}  f[x]  dx  on  [a,  c]  +  \mint{}  f[x]  dx  on  [c,  b]|  \mleq{}  (r1/r(m))


By

---

Latex:
((Assert  ifun(f;[a,  b])  BY
                (DVar  `f'  THEN  Unhide  THEN  Auto))
  THEN  (Assert  ifun(f;[a,  c])  BY
                          (RepeatFor  2  (ParallelLast)
                            THEN  Reduce  -1
                            THEN  Reduce  0
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  Auto))
  THEN  (Assert  ifun(f;[c,  b])  BY
                          (Thin  (-1)
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  Reduce  -1
                            THEN  Reduce  0
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  Auto)))

---

Home Index