Prove2Me

A polynomial consequence of an exponential substitution

Proved
WorkbookRestored.plus_33555

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

Let a=2xa=2^x and b=3x.b=3^x. Rewriting the given equation as 1a+b2+1b+a2+1ab+1=12ab(a+b+1),\frac{1}{a+b^2}+\frac{1}{b+a^2}+\frac{1}{ab+1}=\frac{1}{2ab}(a+b+1), and clearing denominators we get a(b−1)(b−a)[(b+1)(b2+ab+a2)+a+b]+b(a−1)2[b3(a+1)+(a+b2)(a2+a+1)]=0.a(b-1)(b-a)[(b+1)(b^2+ab+a^2)+a+b]+b(a-1)^2[b^3(a+1)+(a+b^2)(a^2+a+1)]=0. The formal statement quantifies over all real x,a,bx,a,b satisfying the two substitutions and the displayed rational equation.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_33555 (Apache-2.0).

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
Formal statement
theorem WorkbookRestored.plus_33555  (x : ℝ)
  (a b : ℝ)
  (h₀ : a = 2^x)
  (h₁ : b = 3^x)
  (h₂ : 1 / (a + b^2) + 1 / (b + a^2) + 1 / (a * b + 1) = 1 / (2 * a * b) * (a + b + 1)) :
  a * (b - 1) * (b - a) * ((b + 1) * (b^2 + a * b + a^2) + a + b) + b * (a - 1)^2 * (b^3 * (a + 1) + (a + b^2) * (a^2 + a + 1)) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_33555; original Prove2Me node 8c9fa6f4-11ca-4983-a6f8-25c85dc5f20d; Apache-2.0

View graph