Prove2Me

Lean-Workbook Plus 21774: Logarithmic inequality

Proved
WorkbookRestored.plus_21774

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

lean-workbookrestored-importssource-checked

If a,b,c>0a,b,c>0 and a,b,c≠1a,b,c\ne1, then (log⁡b/log⁡a)(log⁡c/log⁡b)=log⁡c/log⁡a(\log b/\log a)(\log c/\log b)=\log c/\log a.

Source: Lean-Workbook row lean_workbook_plus_21774 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
Formal statement
theorem WorkbookRestored.plus_21774 : ∀ a b c : ℝ, (a > 0 ∧ b > 0 ∧ c > 0 ∧ a ≠ 1 ∧ b ≠ 1 ∧ c ≠ 1) →  (Real.log b / Real.log a) * (Real.log c / Real.log b) = (Real.log c / Real.log a)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_21774; immutable original Prove2Me node affe610d-1fb8-4264-8924-9dc8f52fb962

View graph