lean_workbook_plus_12513
Provedwhich is obvious by Bernoulli.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12513 : (5 : ℝ)^(51) ≥ 2^(118) ↔ (1 - 3 / 128)^(17) ≥ 1 / 2 := by sorry
Source
which is obvious by Bernoulli.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_12513 : (5 : ℝ)^(51) ≥ 2^(118) ↔ (1 - 3 / 128)^(17) ≥ 1 / 2 := by sorry