Prove2Me

Factoring a difference of reciprocal sums

Proved
WorkbookSource.problem_40020

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let x1>x2>0x_1 > x_2>0 , then f(x1)−f(x2)=x1−x2+1x1−1x2=(x1−x2)(x1x2−1)x1x2f(x_1)-f(x_2)=x_1-x_2+\dfrac{1}{x_1}-\dfrac{1}{x_2}=\dfrac{(x_1-x_2)(x_1x_2-1)}{x_1x_2}

Source: InternLM Lean-Workbook, record lean_workbook_40020 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_40020  (x1 x2 : ℝ)
  (f : ℝ → ℝ)
  (h₀ : 0 < x1 ∧ 0 < x2)
  (h₁ : x1 > x2)
  (h₂ : f x1 - f x2 = x1 - x2 + (1 / x1 - 1 / x2)) :
  f x1 - f x2 = (x1 - x2) * (x1 * x2 - 1) / (x1 * x2)  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_40020; Apache-2.0

View graph