y_ne_zero_of_one_lt_x — Mathlib

English

If a.x > 1, then a.y ≠ 0.

Русский

Если a.x > 1, то a.y ≠ 0.

LaTeX

$$$$ \forall a \in Pell.Solution_1(d),\; 1 < a.x \Rightarrow a.y \neq 0. $$$$

Lean4

/-- A solution with `x > 1` must have `y ≠ 0`. -/
theorem y_ne_zero_of_one_lt_x {a : Solution₁ d} (ha : 1 < a.x) : a.y ≠ 0 :=
  by
  intro hy
  have prop := a.prop
  rw [hy, sq (0 : ℤ), zero_mul, mul_zero, sub_zero] at prop
  exact lt_irrefl _ (((one_lt_sq_iff₀ <| zero_le_one.trans ha.le).mpr ha).trans_eq prop)

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