---

Step * of Lemma uhg-identity1

∀[t1,t2,t3,t4:ℝ].
  ((((((r1 + (t1 * t2)) * (t3 + t4)) - (r1 + (t3 * t4)) * (t1 + t2))
  * (((r1 + (t1 * t3)) * (t2 + t4)) - (r1 + (t2 * t4)) * (t1 + t3)))
  + ((r(2) * ((t3 * t4) - t1 * t2)) * r(2) * ((t2 * t4) - t1 * t3)))
  = ((((r1 - t1 * t2) * (t3 + t4)) - (r1 - t3 * t4) * (t1 + t2))
    * (((r1 - t1 * t3) * (t2 + t4)) - (r1 - t2 * t4) * (t1 + t3))))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[t1,t2,t3,t4:\mBbbR{}].
    ((((((r1  +  (t1  *  t2))  *  (t3  +  t4))  -  (r1  +  (t3  *  t4))  *  (t1  +  t2))
    *  (((r1  +  (t1  *  t3))  *  (t2  +  t4))  -  (r1  +  (t2  *  t4))  *  (t1  +  t3)))
    +  ((r(2)  *  ((t3  *  t4)  -  t1  *  t2))  *  r(2)  *  ((t2  *  t4)  -  t1  *  t3)))
    =  ((((r1  -  t1  *  t2)  *  (t3  +  t4))  -  (r1  -  t3  *  t4)  *  (t1  +  t2))
        *  (((r1  -  t1  *  t3)  *  (t2  +  t4))  -  (r1  -  t2  *  t4)  *  (t1  +  t3))))


By

---

Latex:
Auto

---

Home Index