Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1983P2

module

public import Mathlib.Tactic
public import Mathlib.Analysis.MeanInequalitiesPow

public section


/-!
# USA Mathematical Olympiad 1983, Problem 2

Prove that the zeros of

\[x^5+ax^4+bx^3+cx^2+dx+e=0\]

cannot all be real if $2a^2<5b$.
-/

namespace Usa1983P2
open Polynomial

theorem usa1983_p2 (a b c d e : ℝ)(x : Fin 5 → ℝ):
    2*a^2 < 5*b → ¬(((X - C (x 0)) * (X - C (x 1)) * (X - C (x 2)) * (X - C (x 3)) * (X - C (x 4))
    = X^5 + C a * X^4 + C b * X^3 + C c * X^2 + C d * X + C e)) := sorry

end Usa1983P2

File author(s): Pacmanboss256

This problem has a complete formalized solution.