---

Step * 3 of Lemma four-squares

.....antecedent..... 
∀n,m:ℕ+.
  ((∃a,b,c,d:ℤ. (n = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ))
  ⇒ (∃a,b,c,d:ℤ. (m = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ))
  ⇒ (∃a,b,c,d:ℤ. ((n * m) = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)))
BY
{ ((UnivCD THENA Auto) THEN ExRepD) }

1
1. n : ℕ+
2. m : ℕ+
3. a1 : ℤ
4. b1 : ℤ
5. c1 : ℤ
6. d1 : ℤ
7. n = ((a1 * a1) + (b1 * b1) + (c1 * c1) + (d1 * d1)) ∈ ℤ
8. a : ℤ
9. b : ℤ
10. c : ℤ
11. d : ℤ
12. m = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ
⊢ ∃a,b,c,d:ℤ. ((n * m) = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)

---

Latex:

---

Latex:
.....antecedent..... 
\mforall{}n,m:\mBbbN{}\msupplus{}.
    ((\mexists{}a,b,c,d:\mBbbZ{}.  (n  =  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d))))
    {}\mRightarrow{}  (\mexists{}a,b,c,d:\mBbbZ{}.  (m  =  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d))))
    {}\mRightarrow{}  (\mexists{}a,b,c,d:\mBbbZ{}.  ((n  *  m)  =  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d)))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  ExRepD)

---

Home Index