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?
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 |
|---|---|---|---|
| 312 | Otabek_Aynazarov | 2026-03-01T05:08 | Forbidden axiom |
| 223 | FelixMP | Long time ago | PASSED |
| 182 | Kitsune | Long time ago | PASSED |