lean_workbook_plus_77486
ProvedShow that with no use of logarithm, elementarily as possible.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77486 : (4:ℝ)^(80) > 2 * (3:ℝ)^(100) := by sorry
Source
Show that with no use of logarithm, elementarily as possible.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_77486 : (4:ℝ)^(80) > 2 * (3:ℝ)^(100) := by sorry