Step
*
1
1
of Lemma
rsin-reduce4
1. v : ℝ
2. v1 : ℝ
3. ((v1 * v1) + (v * v)) = r1
⊢ (r(2) * (r(2) * v1 * v) * ((v * v) - v1 * v1)) = (r(4) * v * (v1 - r(2) * v1 * v1 * v1))
BY
{ (nRAdd ⌜-(r(4) * v * (v1 - r(2) * v1 * v1 * v1))⌝ 0⋅ THEN Auto) }
1
1. v : ℝ
2. v1 : ℝ
3. ((v1 * v1) + (v * v)) = r1
⊢ ((r(-4) * v * v1) + (r(4) * v * v * v * v1) + (r(4) * v * v1 * v1 * v1)) = r0
Latex:
Latex:
1. v : \mBbbR{}
2. v1 : \mBbbR{}
3. ((v1 * v1) + (v * v)) = r1
\mvdash{} (r(2) * (r(2) * v1 * v) * ((v * v) - v1 * v1)) = (r(4) * v * (v1 - r(2) * v1 * v1 * v1))
By
Latex:
(nRAdd \mkleeneopen{}-(r(4) * v * (v1 - r(2) * v1 * v1 * v1))\mkleeneclose{} 0\mcdot{} THEN Auto)
Home
Index