Theorem: FltRegular.p_dvd_c_of_ab_of_anegc (FltRegular/MayAssume/Lemmas.lean)

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
h : a ^ p + b ^ p = c ^ p
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
⊢ ↑p ∣ c
Tactic:
letI : Fact p.Prime := ⟨hpri⟩
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
h : a ^ p + b ^ p = c ^ p
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
⊢ ↑p ∣ c

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
h : a ^ p + b ^ p = c ^ p
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
⊢ ↑p ∣ c
Tactic:
replace h := congr_arg (fun n : ℤ => (n : ZMod p)) h
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : (fun n => ↑n) (a ^ p + b ^ p) = (fun n => ↑n) (c ^ p)
⊢ ↑p ∣ c

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : (fun n => ↑n) (a ^ p + b ^ p) = (fun n => ↑n) (c ^ p)
⊢ ↑p ∣ c
Tactic:
simp only [Int.natCast_pow, Int.cast_add, Int.cast_pow, ZMod.pow_card] at h
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
⊢ ↑p ∣ c

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
⊢ ↑p ∣ c
Tactic:
simp only [← ZMod.intCast_eq_intCast_iff, Int.cast_neg] at hbc hab
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c
Tactic:
rw [hab, hbc, ← sub_eq_zero, ← sub_eq_add_neg, ← Int.cast_neg, ← Int.cast_sub,
  ← Int.cast_sub] at h
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑(-c - c - c) = 0
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑(-c - c - c) = 0
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c
Tactic:
ring_nf at h
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑(-(c * 3)) = 0
⊢ ↑p ∣ c

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑(-(c * 3)) = 0
⊢ ↑p ∣ c
Tactic:
simp only [Int.cast_neg, Int.cast_mul, Int.cast_one, Int.cast_ofNat, neg_eq_zero,
  mul_eq_zero] at h
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑p ∣ c

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑p ∣ c
Tactic:
rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑c = 0

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑c = 0
Tactic:
refine' Or.resolve_right h fun h3 => _
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : 3 = 0
⊢ False

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : 3 = 0
⊢ False
Tactic:
rw [show (3 : ZMod p) = ((3 : ℕ) : ZMod p) by simp, ZMod.natCast_zmod_eq_zero_iff_dvd,
  Nat.dvd_prime Nat.prime_three] at h3
State after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : p = 1 ∨ p = 3
⊢ False

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : p = 1 ∨ p = 3
⊢ False
Tactic:
cases' h3 with H₁ H₂
State after:
case inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₁ : p = 1
⊢ False

case inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₂ : p = 3
⊢ False

State before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : 3 = 0
⊢ 3 = ↑3
Tactic:
simp
State after:
no goals

State before:
case inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₁ : p = 1
⊢ False
Tactic:
exact hpri.ne_one H₁
State after:
no goals

State before:
case inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₂ : p = 3
⊢ False
Tactic:
exact hp H₂
State after:
no goals