---

Step * of Lemma ftc-example2

∀a,b:ℝ.
  (a_∫-b t^3 * cosine(t) dt
  = ((((b^3 - r(6) * b) * sine(b)) - (a^3 - r(6) * a) * sine(a))
    + ((((r(3) * b^2) - r(6)) * cosine(b)) - ((r(3) * a^2) - r(6)) * cosine(a))))
BY
{ (Auto THEN RW (SweepDnC IntegralEvalC) 0⋅ THEN Auto THEN Try ((MemTypeCD THEN Reduce 0 THEN Auto))) }

1
.....rewrite subgoal..... 
1. a : ℝ
2. b : ℝ
⊢ d(t^3 - 1)/dt = λt.if (3 - 1 =z 0) then r0 else r(3 - 1) * t^3 - 1 - 1 fi  on (-∞, ∞)

2
.....antecedent..... 
1. a : ℝ
2. b : ℝ
⊢ d(((r(3) * r(3 - 1) * t^1) * -(sine(t))) - ((r(3) * r(3 - 1) * r1 * t^0) * -(-(cosine(t)))) - ((r(3)
* r(3 - 1)
* r1
* r0)
* -(-(sine(t)))) - r0)/dt = λt.(r(3) * if (3 - 1 =z 0) then r0 else r(3 - 1) * t^3 - 1 - 1 fi )
* -(cosine(t)) on (-∞, ∞)

3
1. a : ℝ
2. b : ℝ
⊢ ((b^3 * sine(b)) - ((r(3) * b^2) * -(cosine(b))) - ((r(3) * r(2) * b^1) * -(sine(b))) - ((r(3) * r(2) * r1 * b^0)
* -(-(cosine(b)))) - ((r(3) * r(2) * r1 * r0) * -(-(sine(b)))) - r0 - (a^3 * sine(a)) - ((r(3) * a^2) * -(cosine(a))) 
- ((r(3) * r(2) * a^1) * -(sine(a))) - ((r(3) * r(2) * r1 * a^0) * -(-(cosine(a)))) - ((r(3) * r(2) * r1 * r0)
* -(-(sine(a)))) - r0)
= ((((b^3 - r(6) * b) * sine(b)) - (a^3 - r(6) * a) * sine(a))
  + ((((r(3) * b^2) - r(6)) * cosine(b)) - ((r(3) * a^2) - r(6)) * cosine(a)))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    (a\_\mint{}\msupminus{}b  t\^{}3  *  cosine(t)  dt
    =  ((((b\^{}3  -  r(6)  *  b)  *  sine(b))  -  (a\^{}3  -  r(6)  *  a)  *  sine(a))
        +  ((((r(3)  *  b\^{}2)  -  r(6))  *  cosine(b))  -  ((r(3)  *  a\^{}2)  -  r(6))  *  cosine(a))))


By

---

Latex:
(Auto  THEN  RW  (SweepDnC  IntegralEvalC)  0\mcdot{}  THEN  Auto  THEN  Try  ((MemTypeCD  THEN  Reduce  0  THEN  Auto)))

---

Home Index