---

Step * 1 of Lemma rcos-reduce4


1. x : ℝ
2. ((x)/2)/2 = (x)/4
3. y : ℝ
4. (x)/4 = y ∈ ℝ
⊢ (rcos(y)^2 - rsin(y)^2^2 - 2 * rsin(y) * rcos(y)^2) = (r1 - 8 * rsin(y)^2 * rcos(y)^2)
BY
{ ((InstLemma `rsin-rcos-pythag` [⌜y⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜rcos(y)⌝;⌜rsin(y)⌝]⋅
   THEN (RWW "int-rmul-req rnexp2" 0 THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. v : ℝ
2. v1 : ℝ
3. ((v1 * v1) + (v * v)) = r1
⊢ ((((v * v) - v1 * v1) * ((v * v) - v1 * v1)) - (r(2) * v1 * v) * r(2) * v1 * v) = (r1 - r(8) * (v1 * v1) * v * v)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  ((x)/2)/2  =  (x)/4
3.  y  :  \mBbbR{}
4.  (x)/4  =  y
\mvdash{}  (rcos(y)\^{}2  -  rsin(y)\^{}2\^{}2  -  2  *  rsin(y)  *  rcos(y)\^{}2)  =  (r1  -  8  *  rsin(y)\^{}2  *  rcos(y)\^{}2)


By

---

Latex:
((InstLemma  `rsin-rcos-pythag`  [\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}rcos(y)\mkleeneclose{};\mkleeneopen{}rsin(y)\mkleeneclose{}]\mcdot{}
  THEN  (RWW  "int-rmul-req  rnexp2"  0  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index