---

Step * of Lemma 33-is-sum-of-three-cubes-implies

∃d,n:ℕ
 ((∃c:ℤ. ((((2 * d) * ((d * d) + (3 * n * n))) - 33) = (c * c * c) ∈ ℤ))
 ∨ (∃c:ℤ. (((((2 * d) + 1) * (((d * (d + 1)) + (3 * n * (n + 1))) + 1)) - 33) = (c * c * c) ∈ ℤ)))
BY
{ (InstLemma `sum-of-three-cubes-iff` [⌜33⌝]⋅
   THEN Auto
   THEN (RWO "assert-is_power" (1) THENA Auto)
   THEN D 1
   THEN Auto
   THEN (RepeatFor 4 (ParallelLast) THEN HypSubst'  (-1) 0)
   THEN Computation
   THEN Auto) }

---

Latex:

---

Latex:
\mexists{}d,n:\mBbbN{}
  ((\mexists{}c:\mBbbZ{}.  ((((2  *  d)  *  ((d  *  d)  +  (3  *  n  *  n)))  -  33)  =  (c  *  c  *  c)))
  \mvee{}  (\mexists{}c:\mBbbZ{}.  (((((2  *  d)  +  1)  *  (((d  *  (d  +  1))  +  (3  *  n  *  (n  +  1)))  +  1))  -  33)  =  (c  *  c  *  c))))


By

---

Latex:
(InstLemma  `sum-of-three-cubes-iff`  [\mkleeneopen{}33\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (RWO  "assert-is\_power"  (1)  THENA  Auto)
  THEN  D  1
  THEN  Auto
  THEN  (RepeatFor  4  (ParallelLast)  THEN  HypSubst'    (-1)  0)
  THEN  Computation
  THEN  Auto)

---

Home Index