English
If x, y ∈ ℤ and x^2 = d y^2 with d nonsquare, then x = 0 and y = 0.
Русский
Если x^2 = d y^2 для целых x, y и d ненквадратное, тогда x = 0 и y = 0.
LaTeX
$$$$\forall d \in \mathbb{N},\; [\text{Nonsquare}(d)]\Rightarrow \forall x,y \in \mathbb{Z},\; x^2 = d y^2 \Rightarrow x=0 \land y=0.$$$$
Lean4
theorem divides_sq_eq_zero {x y} (h : x * x = d * y * y) : x = 0 ∧ y = 0 :=
let g := x.gcd y
Or.elim g.eq_zero_or_pos (fun H => ⟨Nat.eq_zero_of_gcd_eq_zero_left H, Nat.eq_zero_of_gcd_eq_zero_right H⟩)
fun gpos =>
False.elim <| by
let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime _ _
rw [hx, hy] at h
have : m * m = d * (n * n) := by
refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_
simpa [mul_comm, mul_left_comm, mul_assoc] using h
have co2 :=
let co1 := co.mul_right co
co1.mul_left co1
exact
Nonsquare.ns d m
(Nat.dvd_antisymm (by rw [this]; apply dvd_mul_right) <| co2.dvd_of_dvd_mul_right <| by simp [this])
