x_zpow_pos — Mathlib

English

If a is a Pell solution with x > 0, then for every integer exponent n, the x-coordinate of a^n is positive.

Русский

Если у решения Пелля x > 0, то для любого целочисленного показателя n x-координата a^n положительна.

LaTeX

$$$\forall a\in \mathrm{Solution}_1(d),\; a_x>0 \rightarrow \forall n\in \mathbb{Z},\; (a^n)_x > 0$$$

Lean4

/-- If `(x, y)` is a solution with `x` positive, then all its powers have positive `x`. -/
theorem x_zpow_pos {a : Solution₁ d} (hax : 0 < a.x) (n : ℤ) : 0 < (a ^ n).x := by
  cases n with
  | ofNat n =>
    rw [Int.ofNat_eq_coe, zpow_natCast]
    exact x_pow_pos hax n
  | negSucc n =>
    rw [zpow_negSucc]
    exact x_pow_pos hax (n + 1)

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