Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ ∃ X Y Z, X ≠ 0 ∧ Y ≠ 0 ∧ Z ≠ 0 ∧ 2 * v = X ^ 3 ∧ u - v = Y ^ 3 ∧ u + v = Z ^ 3
Tactic:
apply Int.cube_of_coprime
Proof state after:
case ha
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ 2 * v ≠ 0

case hb
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ u - v ≠ 0

case hc
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ u + v ≠ 0

case hcoprimeab
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ IsCoprime (2 * v) (u - v)

case hcoprimeac
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ IsCoprime (2 * v) (u + v)

case hcoprimebc
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ IsCoprime (u - v) (u + v)

case hs
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ 2 * v * (u - v) * (u + v) = ?s ^ 3

case s
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : Int.gcd (2 * (3 * s)) ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
⊢ ℤ