---

Step * 1 1 of Lemma integral-additive-lemma


1. m : ℝ
2. M : ℝ
3. m ≤ M
4. f : {f:[m, M] ⟶ℝ| ifun(f;[m, M])} 
5. a : {x:ℝ| x ∈ [m, M]} 
6. b : {x:ℝ| x ∈ [m, M]} 
7. λx.f[x] ∈ {f:[m, M] ⟶ℝ| ifun(f;[m, M])} 
8. m ≤ rmin(a;b)
9. rmin(a;b) ≤ M
10. ∫ f[x] dx on [m, b] = (∫ f[x] dx on [m, rmin(a;b)] + ∫ f[x] dx on [rmin(a;b), b])
11. ∫ f[x] dx on [m, a] = (∫ f[x] dx on [m, rmin(a;b)] + ∫ f[x] dx on [rmin(a;b), a])
⊢ (∫ f[x] dx on [rmin(a;b), b] - ∫ f[x] dx on [rmin(a;b), a]) = (∫ f[x] dx on [m, b] - ∫ f[x] dx on [m, a])
BY
{ (RWO "-1 -2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  m  :  \mBbbR{}
2.  M  :  \mBbbR{}
3.  m  \mleq{}  M
4.  f  :  \{f:[m,  M]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[m,  M])\} 
5.  a  :  \{x:\mBbbR{}|  x  \mmember{}  [m,  M]\} 
6.  b  :  \{x:\mBbbR{}|  x  \mmember{}  [m,  M]\} 
7.  \mlambda{}x.f[x]  \mmember{}  \{f:[m,  M]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[m,  M])\} 
8.  m  \mleq{}  rmin(a;b)
9.  rmin(a;b)  \mleq{}  M
10.  \mint{}  f[x]  dx  on  [m,  b]  =  (\mint{}  f[x]  dx  on  [m,  rmin(a;b)]  +  \mint{}  f[x]  dx  on  [rmin(a;b),  b])
11.  \mint{}  f[x]  dx  on  [m,  a]  =  (\mint{}  f[x]  dx  on  [m,  rmin(a;b)]  +  \mint{}  f[x]  dx  on  [rmin(a;b),  a])
\mvdash{}  (\mint{}  f[x]  dx  on  [rmin(a;b),  b]  -  \mint{}  f[x]  dx  on  [rmin(a;b),  a])
=  (\mint{}  f[x]  dx  on  [m,  b]  -  \mint{}  f[x]  dx  on  [m,  a])


By

---

Latex:
(RWO  "-1  -2"  0  THEN  Auto)

---

Home Index