Sum of three cubes

An integer n : ℤ can be written as a sum of three cubes (of integers) if and only if n is not 4 or 5 mod 9.

References:

• Wikipedia
• mathoverflow/100324 asked by user David Feldman

def SumOfThreeCubes.IsSumOfThreeCubes (n : ℤ) : Prop

The predicate that n : ℤ is a sum of three (integer) cubes.

Equations

• SumOfThreeCubes.IsSumOfThreeCubes n = ∃ (x : ℤ) (y : ℤ) (z : ℤ), n = x ^ 3 + y ^ 3 + z ^ 3

theorem SumOfThreeCubes.isSumOfThreeCubes_2 : IsSumOfThreeCubes 2

theorem SumOfThreeCubes.isSumOfThreeCubes_33 : IsSumOfThreeCubes 33

theorem SumOfThreeCubes.mod_9_of_isSumOfThreeCubes (n : ℤ) (hn : IsSumOfThreeCubes n) : ¬(n ≡ 4 [ZMOD 9] ∨ n ≡ 5 [ZMOD 9])

theorem SumOfThreeCubes.isSumOfThreeCubes_iff_mod_9 : (∀ (n : ℤ), IsSumOfThreeCubes n ↔ ¬(n ≡ 4 [ZMOD 9] ∨ n ≡ 5 [ZMOD 9])) ↔ sorry

An integer n : ℤ can be written as a sum of three cubes (of integers) if and only if n is not 4 or 5 mod 9.