x_pow_pos — Mathlib

English

If a is a Pell solution with x-coordinate positive, then every natural power a^n has x > 0.

Русский

Если решение Пелля имеет x > 0, то у всех натуральных степеней x остаётся положительным.

LaTeX

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

Lean4

/-- If `(x, y)` is a solution with `x` positive, then all its powers with natural exponents
have positive `x`. -/
theorem x_pow_pos {a : Solution₁ d} (hax : 0 < a.x) (n : ℕ) : 0 < (a ^ n).x := by
  induction n with
  | zero => simp only [pow_zero, x_one, zero_lt_one]
  | succ n ih => rw [pow_succ]; exact x_mul_pos ih hax

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