theory prob10 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin
lemma for_a:
fixes a b :: real and c m n :: int
assumes "0 < a" and "0 < b" and "1 / a + 1 / b = 1"
assumes "c <= m * a" and "m * a < c + 1"
assumes "c <= n * b" and "n * b < c + 1"
shows "c = m * a"
proof (rule ccontr)
assume "c ≠ m * a"
hence "c * (1 / a) < m ∧ m < (c + 1) * (1 / a) ∧
c * (1 / b) <= n ∧ n < (c + 1) * (1 / b)"
using assms by (simp add: field_simps)
hence "c * (1 / a + 1 / b) < m + n ∧ m + n < (c + 1) * (1 / a + 1 / b)"
by (simp add: algebra_simps)
hence "c < m + n ∧ m + n < c + 1"
using assms by simp
thus "False"
by auto
qed
theorem prob10:
fixes a b :: real and m n :: int
assumes "0 < a" and "0 < b" and "1 / a + 1 / b = 1"
assumes "¬(a ∈ Rats)" and "¬(b ∈ Rats)"
assumes "m ≠ 0 ∨ n ≠ 0"
shows "floor (m * a) ≠ floor (n * b)" (is "¬ ?P")
proof
assume ?P
then obtain c where "(c::int) <= m * a ∧ m * a < c + 1 ∧ c <= n * b ∧ n * b < c + 1"
using real_of_int_floor_add_one_gt real_of_int_floor_le by metis
with for_a assms have "c = m * a ∧ c = n * b"
by auto
with assms have "a = c / m ∨ b = c / n"
by auto
hence "a ∈ Rats ∨ b ∈ Rats"
using real_eq_of_int by auto
thus False
using assms by auto
qed
end
