---

Step * of Lemma integral-additive-lemma

∀[m,M:ℝ].
  ∀[f:{f:[m, M] ⟶ℝ| ifun(f;[m, M])} ]. ∀[a,b:{x:ℝ| x ∈ [m, M]} ].
    (a_∫-b f[x] dx = (∫ f[x] dx on [m, b] - ∫ f[x] dx on [m, a])) 
  supposing m ≤ M
BY
{ (Intros
   THEN Unfold `integral` 0
   THEN (Assert λx.f[x] ∈ {f:[m, M] ⟶ℝ| ifun(f;[m, M])}  BY
               (Unhide THEN DVar `f' THEN MemTypeCD THEN Auto))
   THEN Unhide
   THEN Auto
   THEN Try ((BLemma `rmin_ub` THEN Auto))) }

1
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])} 
⊢ (∫ 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])

---

Latex:

---

Latex:
\mforall{}[m,M:\mBbbR{}].
    \mforall{}[f:\{f:[m,  M]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[m,  M])\}  ].  \mforall{}[a,b:\{x:\mBbbR{}|  x  \mmember{}  [m,  M]\}  ].
        (a\_\mint{}\msupminus{}b  f[x]  dx  =  (\mint{}  f[x]  dx  on  [m,  b]  -  \mint{}  f[x]  dx  on  [m,  a])) 
    supposing  m  \mleq{}  M


By

---

Latex:
(Intros
  THEN  Unfold  `integral`  0
  THEN  (Assert  \mlambda{}x.f[x]  \mmember{}  \{f:[m,  M]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[m,  M])\}    BY
                          (Unhide  THEN  DVar  `f'  THEN  MemTypeCD  THEN  Auto))
  THEN  Unhide
  THEN  Auto
  THEN  Try  ((BLemma  `rmin\_ub`  THEN  Auto)))

---

Home Index