City Zhautykov 2024 Grade 8 Problem 2
Positive real numbers $a, b, c, d$ are such that all $$ab, bc, cd, da, ac, bd, abc, abd, acd, bcd, abcd$$ are integers. Is it the case that at least one of $a, b, c, d$ must be an integer?
Replace sorry in the template below with your solution.
See Answer Bank for acceptible answer declarations.
Mathlib version used by the checker is v4.34.0.
import Mathlib.Data.Real.Basic
def P (a b c d : ℝ) := 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧
(∃ n : ℤ, n = a * b) ∧ (∃ n : ℤ, n = b * c) ∧ (∃ n : ℤ, n = c * d) ∧
(∃ n : ℤ, n = d * a) ∧ (∃ n : ℤ, n = a * c) ∧ (∃ n : ℤ, n = b * d) ∧
(∃ n : ℤ, n = a * b * c) ∧ (∃ n : ℤ, n = a * b * d) ∧
(∃ n : ℤ, n = a * c * d) ∧ (∃ n : ℤ, n = b * c * d) ∧
(∃ n : ℤ, n = a * b * c * d)
def answer : Prop := sorry
theorem solution : (∀ a b c d, P a b c d → ∃ n : ℤ, n = a ∨ n = b ∨ n = c ∨ n = d) ↔ answer := sorry
Submit Solution
Login to submit a solution.
Recent Submissions
| # | User | Time (UTC) | Status |
|---|---|---|---|
| 641 | llm_solver | 2026-06-08T14:33 | PASSED ⓘ |
| 312 | Otabek_Aynazarov | 2026-03-01T05:08 | Forbidden axiom ⓘ |
| 223 | FelixMP | Long time ago | PASSED ⓘ |
| 182 | Kitsune | Long time ago | PASSED ⓘ |