---

Step * of Lemma test-ring-req

∀v,v1,v2,v3,v4,v5,v6,v7,v8,v9:ℝ.
  ((((((v6 * v3) + (v2 * v5) + (v4 * v7)) - (v7 * v2) + (v3 * v4) + (v5 * v6))
    * (((v6 * v9) + (v8 * v1) + (v * v7)) - (v7 * v8) + (v9 * v) + (v1 * v6)))
  + ((((v * v7) + (v6 * v5) + (v4 * v1)) - (v1 * v6) + (v7 * v4) + (v5 * v))
    * (((v6 * v9) + (v8 * v3) + (v2 * v7)) - (v7 * v8) + (v9 * v2) + (v3 * v6)))
  + ((((v * v3) + (v2 * v7) + (v6 * v1)) - (v1 * v2) + (v3 * v6) + (v7 * v))
    * (((v6 * v9) + (v8 * v5) + (v4 * v7)) - (v7 * v8) + (v9 * v4) + (v5 * v6))))
  = r0)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}v,v1,v2,v3,v4,v5,v6,v7,v8,v9:\mBbbR{}.
    ((((((v6  *  v3)  +  (v2  *  v5)  +  (v4  *  v7))  -  (v7  *  v2)  +  (v3  *  v4)  +  (v5  *  v6))
        *  (((v6  *  v9)  +  (v8  *  v1)  +  (v  *  v7))  -  (v7  *  v8)  +  (v9  *  v)  +  (v1  *  v6)))
    +  ((((v  *  v7)  +  (v6  *  v5)  +  (v4  *  v1))  -  (v1  *  v6)  +  (v7  *  v4)  +  (v5  *  v))
        *  (((v6  *  v9)  +  (v8  *  v3)  +  (v2  *  v7))  -  (v7  *  v8)  +  (v9  *  v2)  +  (v3  *  v6)))
    +  ((((v  *  v3)  +  (v2  *  v7)  +  (v6  *  v1))  -  (v1  *  v2)  +  (v3  *  v6)  +  (v7  *  v))
        *  (((v6  *  v9)  +  (v8  *  v5)  +  (v4  *  v7))  -  (v7  *  v8)  +  (v9  *  v4)  +  (v5  *  v6))))
    =  r0)


By

---

Latex:
Auto

---

Home Index