---

Step * of Lemma three-cubes-lemma

No Annotations
∀d,e:ℤ.
  (∃a,b:ℤ. ((((a * a) + ((b * b) - a * b)) = e ∈ ℤ) ∧ ((a + b) = d ∈ ℤ))
  ⇐⇒ ∃n:ℕ. (((4 * e) - d * d) = (3 * n * n) ∈ ℤ))
BY
{ (Intros THEN RepeatFor 2 ((D 0 THENA Auto)) THEN ExRepD) }

1
1. d : ℤ
2. e : ℤ
3. a : ℤ
4. b : ℤ
5. ((a * a) + ((b * b) - a * b)) = e ∈ ℤ
6. (a + b) = d ∈ ℤ
⊢ ∃n:ℕ. (((4 * e) - d * d) = (3 * n * n) ∈ ℤ)

2
1. d : ℤ
2. e : ℤ
3. n : ℕ
4. ((4 * e) - d * d) = (3 * n * n) ∈ ℤ
⊢ ∃a,b:ℤ. ((((a * a) + ((b * b) - a * b)) = e ∈ ℤ) ∧ ((a + b) = d ∈ ℤ))

---

Latex:

---

Latex:
No  Annotations
\mforall{}d,e:\mBbbZ{}.
    (\mexists{}a,b:\mBbbZ{}.  ((((a  *  a)  +  ((b  *  b)  -  a  *  b))  =  e)  \mwedge{}  ((a  +  b)  =  d))
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (((4  *  e)  -  d  *  d)  =  (3  *  n  *  n)))


By

---

Latex:
(Intros  THEN  RepeatFor  2  ((D  0  THENA  Auto))  THEN  ExRepD)

---

Home Index