Step
*
of Lemma
rcp-Jacobi
∀[a,b,c:ℝ^3]. req-vec(3;(a x (b x c)) + (b x (c x a)) + (c x (a x b));λi.r0)
BY
{ (Auto THEN D 0 THEN RepUR ``rcp real-vec-mul real-vec-add`` 0 THEN Try (IntSegCases (-1)) THEN Reduce 0 THEN Auto) }
Latex:
Latex:
\mforall{}[a,b,c:\mBbbR{}\^{}3]. req-vec(3;(a x (b x c)) + (b x (c x a)) + (c x (a x b));\mlambda{}i.r0)
By
Latex:
(Auto
THEN D 0
THEN RepUR ``rcp real-vec-mul real-vec-add`` 0
THEN Try (IntSegCases (-1))
THEN Reduce 0
THEN Auto)
Home
Index