---

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


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))
BY
{ (InstLemma `ftc-total-integral` [⌜λ2t.t - a^k⌝;⌜λ2t.(t - a^k + 1/r(k + 1))⌝;⌜b⌝;⌜x⌝]⋅ THENA Auto) }

1
.....antecedent..... 
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. v : ℝ
5. k : ℕ
⊢ d((x - a^k + 1/r(k + 1)))/dx = λx.x - a^k on (-∞, ∞)

2
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. v : ℝ
5. k : ℕ
6. b_∫-x t - a^k dt = ((x - a^k + 1/r(k + 1)) - (b - a^k + 1/r(k + 1)))
⊢ 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  t  -  a\^{}k  dt  =  (x  -  a\^{}k  +  1  -  b  -  a\^{}k  +  1/r(k  +  1))


By

---

Latex:
(InstLemma  `ftc-total-integral`  [\mkleeneopen{}\mlambda{}\msubtwo{}t.t  -  a\^{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t.(t  -  a\^{}k  +  1/r(k  +  1))\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index