lean_workbook_plus_38747
ProvedLet such that . Prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38747 (x : ℝ) (hx : x^5 - x^3 + x - 17 = 0) : 4 < x^3 ∧ x^3 < 17 := by sorry
Source
Let such that . Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38747 (x : ℝ) (hx : x^5 - x^3 + x - 17 = 0) : 4 < x^3 ∧ x^3 < 17 := by sorry