x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
⊢ False
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
⊢ Int.gcd y z = 1
by_contra H
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ False
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
⊢ False
obtain ⟨p, hp, hpy, hpz⟩ := Nat.Prime.not_coprime_iff_dvd.mp H
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ p ∣ 1
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ False
apply hp.not_dvd_one
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ p ∣ Int.gcd x y
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ p ∣ 1
rw [← hc]
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ ↑p ∣ x ^ 2
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ p ∣ Int.gcd x y
apply Nat.dvd_gcd (Int.Prime.dvd_natAbs_of_coe_dvd_sq hp _ _) hpy
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ ↑p ∣ z * z - y * y
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ ↑p ∣ x ^ 2
rw [sq, eq_sub_of_add_eq h]
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : ↑p ∣ y
hpz : ↑p ∣ z
⊢ ↑p ∣ z * z - y * y
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ Int.natAbs y
hpz : p ∣ Int.natAbs z
⊢ ↑p ∣ z * z - y * y
rw [← Int.coe_nat_dvd_left] at hpy hpz
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
H : ¬Int.gcd y z = 1
p : ℕ
hp : Nat.Prime p
hpy : ↑p ∣ y
hpz : ↑p ∣ z
⊢ ↑p ∣ z * z - y * y
exact dvd_sub (hpz.mul_right _) (hpy.mul_right _)