a b c : ℤ
h : Minimal a b c
⊢ Int.gcd a b = 1
a b c : ℤ
h : Minimal a b c
⊢ IsCoprime a b
apply Int.gcd_eq_one_iff_coprime.mp
a b c : ℤ
h : Minimal a b c
hab : ¬Int.gcd a b = 1
⊢ False
a b c : ℤ
h : Minimal a b c
⊢ Int.gcd a b = 1
by_contra hab
case intro.intro.intro
a b c : ℤ
h : Minimal a b c
hab : ¬Int.gcd a b = 1
p : ℕ
hp : Nat.Prime p
hpa : p ∣ Int.natAbs a
hpb : p ∣ Int.natAbs b
⊢ False
a b c : ℤ
h : Minimal a b c
hab : ¬Int.gcd a b = 1
⊢ False
obtain ⟨p, hp, hpa, hpb⟩ := Nat.Prime.not_coprime_iff_dvd.mp hab
case intro.intro.intro.intro
b c : ℤ
p : ℕ
hp : Nat.Prime p
hpb : p ∣ Int.natAbs b
a1 : ℤ
h : Minimal (↑p * a1) b c
hab : ¬Int.gcd (↑p * a1) b = 1
hpa : p ∣ Int.natAbs (↑p * a1)
⊢ False
case intro.intro.intro
a b c : ℤ
h : Minimal a b c
hab : ¬Int.gcd a b = 1
p : ℕ
hp : Nat.Prime p
hpa : p ∣ Int.natAbs a
hpb : p ∣ Int.natAbs b
⊢ False
obtain ⟨a1, rfl⟩ := Int.coe_nat_dvd_left.mpr hpa
case intro.intro.intro.intro.intro
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
⊢ False
case intro.intro.intro.intro
b c : ℤ
p : ℕ
hp : Nat.Prime p
hpb : p ∣ Int.natAbs b
a1 : ℤ
h : Minimal (↑p * a1) b c
hab : ¬Int.gcd (↑p * a1) b = 1
hpa : p ∣ Int.natAbs (↑p * a1)
⊢ False
obtain ⟨b1, rfl⟩ := Int.coe_nat_dvd_left.mpr hpb
case intro.intro.intro.intro.intro
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
hpc : ↑p ^ 2 ∣ c
⊢ False
case intro.intro.intro.intro.intro
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
⊢ False
have hpc : (p : ℤ) ^ 2 ∣ c := by
  rw [← Int.pow_dvd_pow_iff zero_lt_two, ← h.1.2.2]
  apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
  ring
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
⊢ False
case intro.intro.intro.intro.intro
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
hpc : ↑p ^ 2 ∣ c
⊢ False
obtain ⟨c1, rfl⟩ := hpc
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ False
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
⊢ False
have hf : Fermat42 a1 b1 c1 :=
  (Fermat42.mul (Int.coe_nat_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ Int.natAbs c1 < Int.natAbs (↑p ^ 2 * c1)
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ False
apply Nat.le_lt_antisymm (h.2 _ _ _ hf)
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 1 < p ^ 2

case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < Int.natAbs c1
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ Int.natAbs c1 < Int.natAbs (↑p ^ 2 * c1)
rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_ofNat]
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
⊢ (↑p ^ 2) ^ 2 ∣ (↑p * a1) ^ 4 + (↑p * b1) ^ 4
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
⊢ ↑p ^ 2 ∣ c
rw [← Int.pow_dvd_pow_iff zero_lt_two, ← h.1.2.2]
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
⊢ (↑p ^ 2) ^ 2 * (a1 ^ 4 + b1 ^ 4) = (↑p * a1) ^ 4 + (↑p * b1) ^ 4
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
⊢ (↑p ^ 2) ^ 2 ∣ (↑p * a1) ^ 4 + (↑p * b1) ^ 4
apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
no goals
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
⊢ (↑p ^ 2) ^ 2 * (a1 ^ 4 + b1 ^ 4) = (↑p * a1) ^ 4 + (↑p * b1) ^ 4
ring
no goals
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 1 < p ^ 2
exact Nat.one_lt_pow _ _ zero_lt_two (Nat.Prime.one_lt hp)
no goals
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ Int.natAbs (↑p * a1)
b1 : ℤ
hpb : p ∣ Int.natAbs (↑p * b1)
hab : ¬Int.gcd (↑p * a1) (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < Int.natAbs c1
exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))