IMO 2024 Q2

Determine all pairs $(a,b)$ of positive integers for which there exist positive integers $g$ and $N$ such that [ \gcd(a^n + b, b^n + a) = g ] holds for all integers $n \ge N$.

We consider the sequence modulo ab+1; if the exponent is -1 modulo φ(ab+1), the terms are zero modulo ab+1, so ab+1 divides g, and all sufficiently large terms, so all terms, from which we conclude that a=b=1.

def Imo2024Q2.Condition (a : ℕ) (b : ℕ) : Prop

The condition of the problem.

Equations

• Imo2024Q2.Condition a b = (0 < a ∧ 0 < b ∧ ∃ (g : ℕ) (N : ℕ), 0 < g ∧ 0 < N ∧ ∀ (n : ℕ), N ≤ n → (a ^ n + b).gcd (b ^ n + a) = g)

theorem Imo2024Q2.dvd_pow_iff_of_dvd_sub {a : ℕ} {b : ℕ} {d : ℕ} {n : ℕ} {z : ℤ} (ha : a.Coprime d) (hd : ↑d.totient ∣ ↑n - z) : d ∣ a ^ n + b ↔ ↑(ZMod.unitOfCoprime a ha ^ z) + ↑b = 0

theorem Imo2024Q2.Condition.a_pos {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : 0 < a

theorem Imo2024Q2.Condition.b_pos {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : 0 < b

noncomputable def Imo2024Q2.Condition.g {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ℕ

The value of g in the problem (determined by a and b).

Equations

• h.g = ⋯.choose

theorem Imo2024Q2.Condition.g_spec {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ∃ (N : ℕ), 0 < h.g ∧ 0 < N ∧ ∀ (n : ℕ), N ≤ n → (a ^ n + b).gcd (b ^ n + a) = h.g

noncomputable def Imo2024Q2.Condition.N {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ℕ

The value of N in the problem (any sufficiently large value).

Equations

• h.N = ⋯.choose

theorem Imo2024Q2.Condition.N_spec {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : 0 < h.g ∧ 0 < h.N ∧ ∀ (n : ℕ), h.N ≤ n → (a ^ n + b).gcd (b ^ n + a) = h.g

theorem Imo2024Q2.Condition.g_pos {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : 0 < h.g

theorem Imo2024Q2.Condition.N_pos {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : 0 < h.N

theorem Imo2024Q2.Condition.gcd_eq_g {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) {n : ℕ} (hn : h.N ≤ n) : (a ^ n + b).gcd (b ^ n + a) = h.g

theorem Imo2024Q2.Condition.symm {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : Imo2024Q2.Condition b a

theorem Imo2024Q2.Condition.dvd_g_of_le_N_of_dvd {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) {n : ℕ} (hn : h.N ≤ n) {d : ℕ} (hab : d ∣ a ^ n + b) (hba : d ∣ b ^ n + a) : d ∣ h.g

theorem Imo2024Q2.Condition.a_coprime_ab_add_one {a : ℕ} {b : ℕ} : a.Coprime (a * b + 1)

noncomputable def Imo2024Q2.Condition.large_n {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ℕ

A sufficiently large value of n, congruent to -1 mod φ (a * b + 1).

Equations

• h.large_n = (max h.N ⋯.N + 1) * (a * b + 1).totient - 1

theorem Imo2024Q2.Condition.symm_large_n {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ⋯.large_n = h.large_n

theorem Imo2024Q2.Condition.N_le_large_n {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : h.N ≤ h.large_n

theorem Imo2024Q2.Condition.dvd_large_n_sub_neg_one {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ↑(a * b + 1).totient ∣ ↑h.large_n - -1

noncomputable def Imo2024Q2.Condition.large_n_0 {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ℕ

A sufficiently large value of n, congruent to 0 mod φ (a * b + 1).

Equations

• h.large_n_0 = max h.N ⋯.N * (a * b + 1).totient

theorem Imo2024Q2.Condition.symm_large_n_0 {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ⋯.large_n_0 = h.large_n_0

theorem Imo2024Q2.Condition.N_le_large_n_0 {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : h.N ≤ h.large_n_0

theorem Imo2024Q2.Condition.dvd_large_n_0_sub_zero {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : ↑(a * b + 1).totient ∣ ↑h.large_n_0 - 0

theorem Imo2024Q2.Condition.ab_add_one_dvd_a_pow_large_n_add_b {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : a * b + 1 ∣ a ^ h.large_n + b

theorem Imo2024Q2.Condition.ab_add_one_dvd_b_pow_large_n_add_a {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : a * b + 1 ∣ b ^ h.large_n + a

theorem Imo2024Q2.Condition.ab_add_one_dvd_g {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : a * b + 1 ∣ h.g

theorem Imo2024Q2.Condition.ab_add_one_dvd_a_pow_large_n_0_add_b {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : a * b + 1 ∣ a ^ h.large_n_0 + b

theorem Imo2024Q2.Condition.ab_add_one_dvd_b_add_one {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : a * b + 1 ∣ b + 1

theorem Imo2024Q2.Condition.a_eq_one {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : a = 1

theorem Imo2024Q2.Condition.b_eq_one {a : ℕ} {b : ℕ} (h : Imo2024Q2.Condition a b) : b = 1

def Imo2024Q2.solutionSet : Set (ℕ × ℕ)

This is to be determined by the solver of the original problem.

Equations

• Imo2024Q2.solutionSet = {(1, 1)}

theorem Imo2024Q2.result (a : ℕ) (b : ℕ) : Imo2024Q2.Condition a b ↔ (a, b) ∈ Imo2024Q2.solutionSet