---

Step * of Lemma test-omega2

∀p0,p1,q0,q1,r0,r1,t0,t1:ℤ.
  ((((p0 * q1) + (q0 * r1) + (r0 * p1)) - (p1 * q0) + (q1 * r0) + (r1 * p0))
  = ((((t0 * q1) + (q0 * r1) + (r0 * t1)) - (t1 * q0) + (q1 * r0) + (r1 * t0))
    + (((p0 * t1) + (t0 * r1) + (r0 * p1)) - (p1 * t0) + (t1 * r0) + (r1 * p0))
    + (((p0 * q1) + (q0 * t1) + (t0 * p1)) - (p1 * q0) + (q1 * t0) + (t1 * p0)))
  ∈ ℤ)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}p0,p1,q0,q1,r0,r1,t0,t1:\mBbbZ{}.
    ((((p0  *  q1)  +  (q0  *  r1)  +  (r0  *  p1))  -  (p1  *  q0)  +  (q1  *  r0)  +  (r1  *  p0))
    =  ((((t0  *  q1)  +  (q0  *  r1)  +  (r0  *  t1))  -  (t1  *  q0)  +  (q1  *  r0)  +  (r1  *  t0))
        +  (((p0  *  t1)  +  (t0  *  r1)  +  (r0  *  p1))  -  (p1  *  t0)  +  (t1  *  r0)  +  (r1  *  p0))
        +  (((p0  *  q1)  +  (q0  *  t1)  +  (t0  *  p1))  -  (p1  *  q0)  +  (q1  *  t0)  +  (t1  *  p0))))


By

---

Latex:
Auto

---

Home Index