theory Problem

imports Complex

begin

theorem IMO:
   assumes "ALL (x::real) y. f(x + y) + f(x - y) = (2::real) * f x * g y"
   and "~ (ALL x. f(x) = 0)"
   and "ALL x. abs(f x) <= 1"
   shows "ALL y. abs(g y) <= 1"
proof (clarify, rule leI, clarify)
   obtain k where "isLub UNIV {z. EX x. abs(f x) = z} k"
     by (subgoal_tac "EX k. ?P k", force, insert prems,
         auto intro!: reals_complete isUbI setleI)
   hence "ALL x. abs(f x) <= k"
     by (intro allI, rule isLubD2, auto)
   fix y
   assume "abs(g y) > 1"
   have "ALL x. abs(f x) <= k / abs(g y)"
   proof
     fix x
     have "2 * abs(g y) * abs(f x) = abs(f(x + y) + f(x - y))"
       by (insert prems, auto simp add: abs_mult)
     also have "... <= abs(f(x + y)) + abs(f(x - y))"
       by (rule abs_triangle_ineq)
     also from `ALL x. abs(f x) <= k` have "... <=  k + k"
       by (intro add_mono, auto)
     finally have "2 * abs(g y) * abs(f x) <= 2 * k"
       by auto
     thus "abs(f x) <= k / abs(g y)"
       by (subst pos_le_divide_eq, insert prems,
         auto simp add: pos_le_divide_eq mult_commute)
   qed
   hence "isUb UNIV {z. EX x. abs(f x) = z} (k / abs(g y))"
     by (unfold isUb_def, auto intro: setleI)
   moreover note `isLub UNIV {z. EX x. abs(f x) = z} k`
   moreover have "k / abs(g y) < k"
   proof -
     have "k > 0"
     proof -
       from prems obtain w where "f w ~= 0"
         by auto
       moreover from `ALL x. abs(f x) <= k` have "k >= abs(f w)"
         by auto
       ultimately show ?thesis
         by auto
     qed
     thus "k / abs(g y) < k"
       by (insert prems, auto intro: mult_imp_div_pos_less
         simp add: mult_less_cancel_left1)
   qed
   ultimately show False
     by (auto simp add: setge_def isLub_def leastP_def)
qed

end