---

Step * of Lemma four-squares

∀n:ℕ+. ∃a,b,c,d:ℤ. (n = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)
BY
{ ((InstLemma `nat-plus-ind-primes` [⌜λ2n.∃a,b,c,d:ℤ. (n = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)⌝]⋅ THENW Auto)
THENM Trivial
) }

1
.....antecedent..... 
∃a,b,c,d:ℤ. (1 = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)

2
.....antecedent..... 
∀p:Prime. ∃a,b,c,d:ℤ. (p = ((a * a) + (b * b) + (c * c) + (d * d)) ∈ ℤ)

3
.....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)) ∈ ℤ)))

---

Latex:

---

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


By

---

Latex:
((InstLemma  `nat-plus-ind-primes`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.\mexists{}a,b,c,d:\mBbbZ{}.  (n  =  ((a  *  a)  +  (b  *  b)  +  (c  *  c)  +  (d  *  d)))\mkleeneclose{}]\mcdot{}
    THENW  Auto
    )
THENM  Trivial
)

---

Home Index