---

Step * 3 of Lemma ftc-example2


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)))
BY
{ (GenConclTerms  Auto [⌜cosine(a)⌝;⌜cosine(b)⌝;⌜sine(a)⌝;⌜sine(b)⌝]⋅
   THEN All Thin
   THEN Reduce 0
   THEN (RWW "rmul-zero rmul-zero-both.2 rnexp1 rmul-int rmul_assoc<" 0 THENA Auto)
   THEN Reduce 0) }

1
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))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
\mvdash{}  ((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)))


By

---

Latex:
(GenConclTerms    Auto  [\mkleeneopen{}cosine(a)\mkleeneclose{};\mkleeneopen{}cosine(b)\mkleeneclose{};\mkleeneopen{}sine(a)\mkleeneclose{};\mkleeneopen{}sine(b)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Reduce  0
  THEN  (RWW  "rmul-zero  rmul-zero-both.2  rnexp1  rmul-int  rmul\_assoc<"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index