---

Step * of Lemma integral-rsum

∀[n,m:ℤ]. ∀[a,b:ℝ]. ∀[f:{f:{n..m + 1-} ⟶ [rmin(a;b), rmax(a;b)] ⟶ℝ| 
                         ∀i:{n..m + 1-}. ifun(λx.f[i;x];[rmin(a;b), rmax(a;b)])} ].
  (a_∫-b Σ{f[i;x] | n≤i≤m} dx = Σ{a_∫-b f[i;x] dx | n≤i≤m})
BY
{ Assert ⌜∀d:ℕ
            ∀[n:ℤ]. ∀[a,b:ℝ]. ∀[f:{f:{n..(n + d) + 1-} ⟶ [rmin(a;b), rmax(a;b)] ⟶ℝ| 
                                   ∀i:{n..(n + d) + 1-}. ifun(λx.f[i;x];[rmin(a;b), rmax(a;b)])} ].
              (a_∫-b Σ{f[i;x] | n≤i≤n + d} dx = Σ{a_∫-b f[i;x] dx | n≤i≤n + d})⌝⋅ }

1
.....assertion..... 
∀d:ℕ
  ∀[n:ℤ]. ∀[a,b:ℝ]. ∀[f:{f:{n..(n + d) + 1-} ⟶ [rmin(a;b), rmax(a;b)] ⟶ℝ| 
                         ∀i:{n..(n + d) + 1-}. ifun(λx.f[i;x];[rmin(a;b), rmax(a;b)])} ].
    (a_∫-b Σ{f[i;x] | n≤i≤n + d} dx = Σ{a_∫-b f[i;x] dx | n≤i≤n + d})

2
1. ∀d:ℕ
     ∀[n:ℤ]. ∀[a,b:ℝ]. ∀[f:{f:{n..(n + d) + 1-} ⟶ [rmin(a;b), rmax(a;b)] ⟶ℝ| 
                            ∀i:{n..(n + d) + 1-}. ifun(λx.f[i;x];[rmin(a;b), rmax(a;b)])} ].
       (a_∫-b Σ{f[i;x] | n≤i≤n + d} dx = Σ{a_∫-b f[i;x] dx | n≤i≤n + d})
⊢ ∀[n,m:ℤ]. ∀[a,b:ℝ]. ∀[f:{f:{n..m + 1-} ⟶ [rmin(a;b), rmax(a;b)] ⟶ℝ| 
                           ∀i:{n..m + 1-}. ifun(λx.f[i;x];[rmin(a;b), rmax(a;b)])} ].
    (a_∫-b Σ{f[i;x] | n≤i≤m} dx = Σ{a_∫-b f[i;x] dx | n≤i≤m})

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[a,b:\mBbbR{}].  \mforall{}[f:\{f:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  [rmin(a;b),  rmax(a;b)]  {}\mrightarrow{}\mBbbR{}| 
                                                  \mforall{}i:\{n..m  +  1\msupminus{}\}.  ifun(\mlambda{}x.f[i;x];[rmin(a;b),  rmax(a;b)])\}  ].
    (a\_\mint{}\msupminus{}b  \mSigma{}\{f[i;x]  |  n\mleq{}i\mleq{}m\}  dx  =  \mSigma{}\{a\_\mint{}\msupminus{}b  f[i;x]  dx  |  n\mleq{}i\mleq{}m\})


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}
                    \mforall{}[n:\mBbbZ{}].  \mforall{}[a,b:\mBbbR{}].  \mforall{}[f:\{f:\{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  [rmin(a;b),  rmax(a;b)]  {}\mrightarrow{}\mBbbR{}| 
                                                                  \mforall{}i:\{n..(n  +  d)  +  1\msupminus{}\}.  ifun(\mlambda{}x.f[i;x];[rmin(a;b),  rmax(a;b)])\}  ].
                        (a\_\mint{}\msupminus{}b  \mSigma{}\{f[i;x]  |  n\mleq{}i\mleq{}n  +  d\}  dx  =  \mSigma{}\{a\_\mint{}\msupminus{}b  f[i;x]  dx  |  n\mleq{}i\mleq{}n  +  d\})\mkleeneclose{}\mcdot{}

---

Home Index