Real logarithm identity #66568
ProvedWorkbookCorrected.plus_66568arithmeticcorrectedelementaryworkbook
The elementary natural-number / rational identity
holds by direct arithmetic evaluation.
Formalization Note: This corrects Lean-Workbook record lean_workbook_plus_66568, which omitted a compilable colon/type annotation and/or used a preamble of only Mathlib.Analysis.Complex.Basic.
Source: InternLM Lean-Workbook, record lean_workbook_plus_66568 (Apache-2.0).
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Analysis.SpecialFunctions.Log.Base import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Tactic.Ring import Mathlib.Tactic.FieldSimp import Mathlib.Tactic.Positivity import Mathlib.Tactic.Linarith import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_66568 : 1 / Real.logb 2 (1 / 7) + 1 / Real.logb 3 (1 / 7) + 1 / Real.logb 4 (1 / 7) + 1 / Real.logb 5 (1 / 7) + 1 / Real.logb 6 (1 / 7) - 1 / Real.logb 7 (1 / 7) - 1 / Real.logb 8 (1 / 7) - 1 / Real.logb 9 (1 / 7) - 1 / Real.logb 10 (1 / 7) = 1 := by sorry
Source