Theorem: flt_three (Flt/Euler.lean)

State before:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Tactic:
induction' h : (a * b * c).natAbs using Nat.strong_induction_on with k' IH generalizing a b c
State after:
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3

State before:
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Tactic:
intro H
State after:
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
⊢ False

State before:
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
⊢ False
Tactic:
obtain ⟨x'', y'', z'', hxle, hyle, hzle, hcoprime⟩ := exists_coprime zero_lt_three ha hb hc H
State after:
case h.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
⊢ False

State before:
case h.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
⊢ False
Tactic:
obtain ⟨x', y', z', hx'pos, hy'pos, hz'pos, hsmaller, hsolution⟩ := descent x'' y'' z'' hcoprime
State after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ False

State before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ False
Tactic:
refine' IH (x' * y' * z').natAbs _ hx'pos hy'pos hz'pos rfl hsolution
State after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x' * y' * z') < k'

State before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x' * y' * z') < k'
Tactic:
apply lt_of_lt_of_le hsmaller
State after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x'' * y'' * z'') ≤ k'

State before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x'' * y'' * z'') ≤ k'
Tactic:
rw [← h]
State after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x'' * y'' * z'') ≤ Int.natAbs (a * b * c)

State before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x'' * y'' * z'') ≤ Int.natAbs (a * b * c)
Tactic:
simp only [Int.natAbs_mul]
State after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs x'' * Int.natAbs y'' * Int.natAbs z'' ≤ Int.natAbs a * Int.natAbs b * Int.natAbs c

State before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs x'' * Int.natAbs y'' * Int.natAbs z'' ≤ Int.natAbs a * Int.natAbs b * Int.natAbs c
Tactic:
exact Nat.mul_le_mul (Nat.mul_le_mul hxle hyle) hzle
State after:
no goals