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