Step
*
3
1
of Lemma
ftc-example2
1. a : ℝ
2. b : ℝ
3. v : ℝ
4. v1 : ℝ
5. v2 : ℝ
6. v3 : ℝ
⊢ ((b^3 * v3) - ((r(3) * b^2) * -(v1)) - ((r(6) * b) * -(v3)) - (r(6) * -(-(v1))) - r0 - r0 - (a^3 * v2) - ((r(3) * a^2)
* -(v)) - ((r(6) * a) * -(v2)) - (r(6) * -(-(v))) - r0 - r0)
= ((((b^3 - r(6) * b) * v3) - (a^3 - r(6) * a) * v2) + ((((r(3) * b^2) - r(6)) * v1) - ((r(3) * a^2) - r(6)) * v))
BY
{ Auto }
Latex:
Latex:
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  v  :  \mBbbR{}
4.  v1  :  \mBbbR{}
5.  v2  :  \mBbbR{}
6.  v3  :  \mBbbR{}
\mvdash{}  ((b\^{}3  *  v3)  -  ((r(3)  *  b\^{}2)  *  -(v1))  -  ((r(6)  *  b)  *  -(v3))  -  (r(6)  *  -(-(v1)))  -  r0  -  r0  -  (a\^{}3
*  v2)  -  ((r(3)  *  a\^{}2)  *  -(v))  -  ((r(6)  *  a)  *  -(v2))  -  (r(6)  *  -(-(v)))  -  r0  -  r0)
=  ((((b\^{}3  -  r(6)  *  b)  *  v3)  -  (a\^{}3  -  r(6)  *  a)  *  v2)
    +  ((((r(3)  *  b\^{}2)  -  r(6))  *  v1)  -  ((r(3)  *  a\^{}2)  -  r(6))  *  v))
By
Latex:
Auto
Home
Index