---

Step * of Lemma Euler-four-square-identity

∀[a1,b1,c1,d1,a,b,c,d:ℤ].
  ((((a1 * a1) + (b1 * b1) + (c1 * c1) + (d1 * d1)) * ((a * a) + (b * b) + (c * c) + (d * d)))
  = ((((a1 * a) + ((-b1) * b) + ((-c1) * c) + ((-d1) * d)) * ((a1 * a) + ((-b1) * b) + ((-c1) * c) + ((-d1) * d)))
    + (((a1 * b) + (b1 * a) + (c1 * d) + ((-d1) * c)) * ((a1 * b) + (b1 * a) + (c1 * d) + ((-d1) * c)))
    + (((a1 * c) + (c1 * a) + (d1 * b) + ((-b1) * d)) * ((a1 * c) + (c1 * a) + (d1 * b) + ((-b1) * d)))
    + (((a1 * d) + (d1 * a) + (b1 * c) + ((-c1) * b)) * ((a1 * d) + (d1 * a) + (b1 * c) + ((-c1) * b))))
  ∈ ℤ)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[a1,b1,c1,d1,a,b,c,d:\mBbbZ{}].
    ((((a1  *  a1)  +  (b1  *  b1)  +  (c1  *  c1)  +  (d1  *  d1))  *  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d)))
    =  ((((a1  *  a)  +  ((-b1)  *  b)  +  ((-c1)  *  c)  +  ((-d1)  *  d))
          *  ((a1  *  a)  +  ((-b1)  *  b)  +  ((-c1)  *  c)  +  ((-d1)  *  d)))
        +  (((a1  *  b)  +  (b1  *  a)  +  (c1  *  d)  +  ((-d1)  *  c))
            *  ((a1  *  b)  +  (b1  *  a)  +  (c1  *  d)  +  ((-d1)  *  c)))
        +  (((a1  *  c)  +  (c1  *  a)  +  (d1  *  b)  +  ((-b1)  *  d))
            *  ((a1  *  c)  +  (c1  *  a)  +  (d1  *  b)  +  ((-b1)  *  d)))
        +  (((a1  *  d)  +  (d1  *  a)  +  (b1  *  c)  +  ((-c1)  *  b))
            *  ((a1  *  d)  +  (d1  *  a)  +  (b1  *  c)  +  ((-c1)  *  b)))))


By

---

Latex:
Auto

---

Home Index