Lean-Workbook Plus 71756: Logarithmic inequality

Proved

WorkbookRestored.plus_71756

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

lean-workbookrestored-importssource-checked

For a positive natural number $n$ , if $\log_{10}(12n)>\log_{10}75$ , then $n>6$ .

Source: Lean-Workbook row lean_workbook_plus_71756 (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.Base
open Real

Formal statement

theorem WorkbookRestored.plus_71756  (n : ℕ)
  (h₀ : 0 < n)
  (h₁ : Real.logb 10 (12 * n) > Real.logb 10 75) :
  n > 6   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_71756; immutable original Prove2Me node 2a63ced2-015a-4cd9-932d-8342aa8d90cc

View graph