F. Austria 2016 Problem 6

Let $a, b, c$ be integers such that $$\frac{ab}{c} + \frac{ac}{b} + \frac{bc}{a}$$ is an integer. Prove that each of the numbers $$\frac{ab}{c}, \frac{ac}{b}, \frac{bc}{a}$$ is an integer.

<small>Note: the template was updated after the contest.</small>

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.29.0.

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Rat.Init

theorem solution (a b c : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0)
    (h : ∃ n : ℤ, n = (a * b) / (c : ℚ) + (a * c) / b + (b * c) / a) :
    (∃ m : ℤ, m = (a * b) / (c : ℚ)) ∧
    (∃ k : ℤ, k = (a * c) / (b : ℚ)) ∧
    (∃ l : ℤ, l = (b * c) / (a : ℚ)) := sorry

Submit Solution

Login to submit a solution.

Recent Submissions