x_ne_zero — Mathlib

English

If d ≥ 0, then every Pell solution has a.x ≠ 0.

Русский

Если d ≥ 0, то у каждого решения Пелля x ≠ 0.

LaTeX

$$$$ 0 \le d \Rightarrow \forall a \in Pell.Solution_1(d), a.x \neq 0. $$$$

Lean4

/-- A solution has `x ≠ 0`. -/
theorem x_ne_zero (h₀ : 0 ≤ d) (a : Solution₁ d) : a.x ≠ 0 :=
  by
  intro hx
  have h : 0 ≤ d * a.y ^ 2 := mul_nonneg h₀ (sq_nonneg _)
  rw [a.prop_y, hx, sq, zero_mul, zero_sub] at h
  exact not_le.mpr (neg_one_lt_zero : (-1 : ℤ) < 0) h

Похожие утверждения