Prove2Me

lean_workbook_plus_54477

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Denote L=xnyn+xn+1yn+1−2L = x_ny_n + x_{n+1}y_{n+1} - 2. We can derive the following:\n\nxn+1−xn=−L(yn+yn+1)x_{n+1} - x_n = -L(y_n + y_{n+1})\n\nyn+1−yn=−L(xn+xn+1)y_{n+1} - y_n = -L(x_n + x_{n+1})\n\nxn+12−xn2=yn+12−yn2  ⟹  xn+12−yn+12=xn2−yn2=...=x02−y02<0  ⟹  ∣xn∣<∣yn∣x_{n+1}^2 - x_n^2 = y_{n+1}^2 - y_n^2 \implies x_{n+1}^2 - y_{n+1}^2 = x_n^2 - y_n^2 = ... = x_0^2 - y_0^2 < 0 \implies |x_n| < |y_n| for all nn.\n\nxn+1yn+1−xnyn=(xn+1−xn)yn+1+(yn+1−yn)xn=−L(yn+yn+1)yn+1−L(xn+xn+1)xnx_{n+1}y_{n+1} - x_ny_n = (x_{n+1} - x_n)y_{n+1} + (y_{n+1} - y_n)x_n = -L(y_n + y_{n+1})y_{n+1} - L(x_n + x_{n+1})x_n\n\nxn+1yn+1−xnyn=(yn+1−yn)xn+1+(xn+1−xn)yn=−L(xn+xn+1)xn+1−L(yn+yn+1)ynx_{n+1}y_{n+1} - x_ny_n = (y_{n+1} - y_n)x_{n+1} + (x_{n+1} - x_n)y_n = -L(x_n + x_{n+1})x_{n+1} - L(y_n + y_{n+1})y_n\n\nAdding these two and dividing by 2, we get:\n\nxn+1yn+1−xnyn=−L2((xn+xn+1)2+(yn+yn+1)2)x_{n+1}y_{n+1} - x_ny_n = -\frac{L}{2}((x_n + x_{n+1})^2 + (y_n + y_{n+1})^2)\n\n(xn+1yn+1−1)2−(xnyn−1)2=(xn+1yn+1−xnyn)(xnyn+xn+1yn+1−2)=−L22((xn+xn+1)2+(yn+yn+1)2)≤0(x_{n+1}y_{n+1} - 1)^2 - (x_ny_n - 1)^2 = (x_{n+1}y_{n+1} - x_ny_n)(x_ny_n + x_{n+1}y_{n+1} - 2) = -\frac{L^2}{2}((x_n + x_{n+1})^2 + (y_n + y_{n+1})^2) \leq 0\n\n  ⟹  (xnyn−1)2≤(x0y0−1)2=20062\implies (x_ny_n - 1)^2 \leq (x_0y_0 - 1)^2 = 2006^2\n\n∣xnyn∣≤2007  ⟹  ∣xn∣≤2007|x_ny_n| \leq 2007 \implies |x_n| \leq \sqrt{2007}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54477  (x y : ℕ → ℝ)
  (h₀ : ∀ n, x (n + 2) - x (n + 1) = -(y (n + 1) + y n))
  (h₁ : ∀ n, y (n + 2) - y (n + 1) = -(x (n + 1) + x n))
  (h₂ : ∀ n, x (n + 1) * y (n + 1) - x n * y n = -((x n + x (n + 1))^2 + (y n + y (n + 1))^2))
  (h₃ : 0 < x 0)
  (h₄ : 0 < y 0)
  (h₅ : x 0 * y 0 = 2006^2 + 1)
  : ∀ n, |x n| ≤ √2007 ∧ |x n * y n| ≤ 2007   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph