Prove2Me

lean_workbook_plus_66332

Open

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

Write xln⁡a+ln⁡(1+1ax)xln⁡b+ln⁡(1+1bx)=ln⁡a+1xln⁡(1+1ax)ln⁡b+1xln⁡(1+1bx)\frac{x\ln a+\ln \left( 1+\frac{1}{{{a}^{x}}} \right)}{x\ln b+\ln \left( 1+\frac{1}{{{b}^{x}}} \right)}=\frac{\ln a+\frac{1}{x}\ln \left( 1+\frac{1}{{{a}^{x}}} \right)}{\ln b+\frac{1}{x}\ln \left( 1+\frac{1}{{{b}^{x}}} \right)}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66332  (x a b : ℝ)
  (h₀ : a > 0 ∧ b > 0)
  (h₁ : a ≠ 1 ∧ b ≠ 1)
  (h₂ : x ≠ 0) :
  (x * Real.log a + Real.log (1 + 1 / a^x)) / (x * Real.log b + Real.log (1 + 1 / b^x))
    = (Real.log a + 1 / x * Real.log (1 + 1 / a^x)) / (Real.log b + 1 / x * Real.log (1 + 1 / b^x))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph