theory Problem imports Complex begin; theorem assumes "ALL (x::real) y. f(x + y) + f(x - y) = (2::real) * f x * g y" and "EX x. f(x) ~= 0" and "ALL x. abs(f x) <= 1" shows "ALL y. abs(g y) <= 1"; proof; fix y; have "~abs(g y) > 1"; proof; assume "1 < abs(g y)"; have "EX k. isLub UNIV {z. EX x. abs(f x) = z} k"; apply (rule reals_complete); apply auto; apply (rule_tac x = 1 in exI); apply (rule isUbI); apply (rule setleI); apply (insert prems, auto); done; then obtain k where b: "isLub UNIV {z. EX x. abs(f x) = z} k"; by auto; then have a: "ALL x. abs(f x) <= k"; apply clarify; apply (rule isLubD2); apply auto; done; have d: "k > 0"; proof -; obtain w where "f w ~= 0"; by (insert prems, auto); then have "abs(f w) > 0"; by arith; also have "k >= abs(f w)"; by (insert a, auto); finally; show ?thesis;.; qed; have "ALL x. abs(g y) * abs(f x) <= k"; proof; fix x; show "abs(g y) * abs(f x) <= k"; proof -; 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 have "... <= 2 * k"; apply (insert a); apply (frule_tac x = "x + y" in spec); apply (frule_tac x = "x - y" in spec); apply arith; done; finally have "2 * abs(g y) * abs(f x) <= 2 * k";.; thus ?thesis; by (auto simp add: mult_commute); qed; qed; then have "ALL x. abs(f x) <= k / abs (g y)"; apply (intro allI); apply (subst pos_le_divide_eq); apply (insert prems, arith); apply (subst mult_commute, auto); done; hence "isUb UNIV {z. EX x. abs(f x) = z} (k / abs(g y))"; apply (unfold isUb_def, auto); apply (rule setleI); apply auto; done; moreover have "~isUb UNIV {z. EX x. abs(f x) = z} (k / abs(g y))"; apply (rule less_isLub_not_isUb); prefer 2; apply (subgoal_tac "k / abs(g y) < k"); apply assumption; apply (rule mult_imp_div_pos_less); apply (insert prems, arith); apply (subgoal_tac "k * 1 < k * abs(g y)"); apply force; apply (rule real_mult_less_mono2); apply auto; apply (rule d); done; ultimately show False; by auto; qed; thus "abs(g y) <= 1"; by auto; qed;