Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1984P6

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1984, Problem 6

Let a, b, c, and d be odd integers such that 0 < a < b < c < d and ad = bc.
Prove that if a + d = 2ᵏ and b + c = 2ᵐ for some integers k and m, then
a = 1.
-/

namespace Imo1984P6

theorem imo_1984_p6
    (a b c d k m : ℕ)
    (h₀ : 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d)
    (h₁ : Odd a ∧ Odd b ∧ Odd c ∧ Odd d)
    (h₂ : a < b ∧ b < c ∧ c < d)
    (h₃ : a * d = b * c)
    (h₄ : a + d = 2^k)
    (h₅ : b + c = 2^m) :
    a = 1 := sorry

end Imo1984P6

File author(s): Roozbeh Yousefzadeh

This problem has a complete formalized solution.

The solution was imported from IMO-Steps/imo_proofs/imo_1984_p6.lean.