lean_workbook_plus_38471

Proved

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

Well, $7^{6}= 117649 > 10^{5}$ , so $5 \cdot 7^{34}> 5 \cdot 7^{4}\cdot 10^{25}= 12005 \cdot 10^{25}> 1.2 \cdot 10^{29}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38471 : (5 * 7^34 : ℝ) > 1.2 * 10^29   :=  by sorry

Source