Theorem: flt_regular (FltRegular/FltRegular.lean)

State before:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
⊢ FermatLastTheoremFor p
Tactic:
apply fermatLastTheoremFor_iff_int.mpr
State after:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
⊢ FermatLastTheoremWith ℤ p

State before:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
⊢ FermatLastTheoremWith ℤ p
Tactic:
intro a b c ha hb hc e
State after:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
⊢ False

State before:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
⊢ False
Tactic:
have hprod := mul_ne_zero (mul_ne_zero ha hb) hc
State after:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
⊢ False

State before:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
⊢ False
Tactic:
obtain ⟨e', hgcd, hprod'⟩ := MayAssume.coprime e hprod
State after:
case intro.intro
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
⊢ False

State before:
case intro.intro
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
⊢ False
Tactic:
let d := ({a, b, c} : Finset ℤ).gcd id
State after:
case intro.intro
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
⊢ False

State before:
case intro.intro
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
⊢ False
Tactic:
by_cases case : ↑p ∣ (a / d) * (b / d) * (c / d)
State after:
case pos
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ↑p ∣ a / d * (b / d) * (c / d)
⊢ False

case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False

State before:
case pos
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ↑p ∣ a / d * (b / d) * (c / d)
⊢ False

case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Tactic:
exact caseII hreg hodd hprod' hgcd case e'
State after:
case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False

State before:
case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Tactic:
exact caseI hreg case e'
State after:
no goals