Subtracting two from a real exponent

Proved

WorkbookRestored.plus_2048

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

lean-workbookrestored-importssource-checked

With $r=\log_2 5$ ,

2^{r-2}=\frac{2^r}{2^2}.

Formalization Note This restores source entry lean_workbook_plus_2048 from the Apache-2.0 Lean-Workbook dataset. The mathematical proposition is unchanged; targeted imports and namespace openings supply the constants missing from the original Prove2Me node 708b5936-4988-4b07-bd45-2ec77a455817. This is a separate corrected node because formal statements and preambles are immutable.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Tactic
open Real

Formal statement

theorem WorkbookRestored.plus_2048 : (2:ℝ)^(Real.logb 2 5 - 2) = (2:ℝ)^(Real.logb 2 5) / (2:ℝ)^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_2048; original Prove2Me theorem ID 708b5936-4988-4b07-bd45-2ec77a455817; Apache-2.0.

View graph