---

Step * 1 2 1 1 1 1 of Lemma integral-from-Taylor


1. a : ℝ
2. b : ℝ
3. x : ℝ
4. v : ℝ
5. k : ℕ
⊢ b_∫-x v * t - a^k dt = (v * (x - a^k + 1 - b - a^k + 1/r(k + 1)))
BY
{ ((RWO  "integral-rmul-const" 0 THENA Auto) THEN BLemma `rmul_functionality` THEN Auto) }

1
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. v : ℝ
5. k : ℕ
⊢ b_∫-x t - a^k dt = (x - a^k + 1 - b - a^k + 1/r(k + 1))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  x  :  \mBbbR{}
4.  v  :  \mBbbR{}
5.  k  :  \mBbbN{}
\mvdash{}  b\_\mint{}\msupminus{}x  v  *  t  -  a\^{}k  dt  =  (v  *  (x  -  a\^{}k  +  1  -  b  -  a\^{}k  +  1/r(k  +  1)))


By

---

Latex:
((RWO    "integral-rmul-const"  0  THENA  Auto)  THEN  BLemma  `rmul\_functionality`  THEN  Auto)

---

Home Index