Factorial arithmetic identity #62454
ProvedWorkbookCorrected.plus_62454arithmeticcorrectedelementaryworkbook
The elementary natural-number / rational identity
holds by direct arithmetic evaluation.
Formalization Note: This corrects Lean-Workbook record lean_workbook_plus_62454, 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_62454 (Apache-2.0).
Preamble
import Mathlib.Data.Nat.Factorial.Basic import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_62454 : 77 ^ 10 ≥ 2 ^ 10 * ((Nat.factorial 10)) ^ 2 := by sorry
Source