lean_workbook_plus_48040

Proved

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

Observe that $\frac{2^{56}}{5^{24}} = 1.024^8 = 1.048576^4 < 1.05^4 = 1.1025^2 < 1.11^2 = 1.2321 < 1.25 = \frac{5}{2^2}$ , so $5^{25} > 2^{58}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48040 :
  (5:ℝ)^25 > 2^58   :=  by sorry

Source