IMO 2024 P2
Google DeepMind IMO 2024
IMO 2024 P1IMO 2024 P2IMO 2024 P4IMO 2024 P6
IMO 2024 P2
Determine all pairs (a, b) of positive integers for which there exist positive integers g and N such that
\operatorname{gcd}(a^n + b, b^n + a) = g
holds for all integers n \ge N.
(Note that \operatorname{gcd}(x, y) denotes the greatest common divisor of integers x and y.)
Solution: a = 1 and b = 1
open scoped Nat
theorem imo_2024_p2 :
{(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, Nat.gcd (a ^ n + b) (b ^ n + a) = g}
= {(1, 1)} := by
⊢ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)}
induction(10)+2
zero⊢ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)}
succn✝:ℕa✝:{(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)}⊢ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)}
·
zero⊢ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)} use Set.eq_singleton_iff_unique_mem.2 ⟨?_,λb g=>by_contra$ g.2.2.rec λY S i=>S.rec λL D=>?_⟩
zero.refine_1⊢ (1, 1) ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}
zero.refine_2b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Y⊢ False
·
zero.refine_1⊢ (1, 1) ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} -- (1, 1) satisfies the condition with g = 2, N = 3.
exact⟨by
⊢ 0 < 1 left
All goals completed! 🐙,by
⊢ 0 < 1 left
All goals completed! 🐙,2,3,by
⊢ 0 < 2 ∧ 0 < 3 ∧ ∀ n ≥ 3, (1 ^ n + 1).gcd (1 ^ n + 1) = 2 simp_all
All goals completed! 🐙⟩
-- We claim that this is the only solution.
-- The agent wastes the next 16 lines proving then discarding a lemma.
have:b.1+b.2∣Y:=?_
zero.refine_2.refine_2b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 + b.2 ∣ Y⊢ False
zero.refine_2.refine_1b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Y⊢ b.1 + b.2 ∣ Y
·
zero.refine_2.refine_2b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 + b.2 ∣ Y⊢ False suffices: b.1= b.2
zero.refine_2.refine_2b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 + b.2 ∣ Ythis:b.1 = b.2⊢ False
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 + b.2 ∣ Y⊢ b.1 = b.2
·
zero.refine_2.refine_2b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 + b.2 ∣ Ythis:b.1 = b.2⊢ False norm_num[b.ext_iff,<-D.2.2 L,this]at*
zero.refine_2.refine_2b:ℕ × ℕY:ℕL:ℕg:0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → b.2 ^ n + b.2 = gS:(0 < b.2 ^ L ∨ 0 < b.2) ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → b.2 ^ n = b.2 ^ Li:¬b.2 = 1D:(0 < b.2 ^ L ∨ 0 < b.2) ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → b.2 ^ n = b.2 ^ Lthis✝:b.2 + b.2 ∣ b.2 ^ L + b.2this:True⊢ False
use(`pow_lt_pow` has been deprecated, use `pow_lt_pow_right` insteadpow_lt_pow (g.1.nat_succ_le.lt_of_ne' i) (by
b:ℕ × ℕY:ℕL:ℕg:0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → b.2 ^ n + b.2 = gS:(0 < b.2 ^ L ∨ 0 < b.2) ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → b.2 ^ n = b.2 ^ Li:¬b.2 = 1D:(0 < b.2 ^ L ∨ 0 < b.2) ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → b.2 ^ n = b.2 ^ Lthis✝:b.2 + b.2 ∣ b.2 ^ L + b.2this:True⊢ L < L.succ left
All goals completed! 🐙)).ne' (D.2.2 _ L.le_succ)
suffices:b.1+b.2∣b.fst^ (2 *L) +b.2 ∧(b).fst +(b).snd ∣ b.snd^ (2 *L)+b.1
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 + b.2 ∣ Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ b.1 = b.2
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 + b.2 ∣ Y⊢ b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1
·
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 + b.2 ∣ Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ b.1 = b.2 suffices:b.1^2%(b.1+b.2)=b.2^2%(b.1+b.snd)
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝¹:b.1 + b.2 ∣ Ythis✝:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1this:b.1 ^ 2 % (b.1 + b.2) = b.2 ^ 2 % (b.1 + b.2)⊢ b.1 = b.2
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 + b.2 ∣ Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ b.1 ^ 2 % (b.1 + b.2) = b.2 ^ 2 % (b.1 + b.2)
·
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝¹:b.1 + b.2 ∣ Ythis✝:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1this:b.1 ^ 2 % (b.1 + b.2) = b.2 ^ 2 % (b.1 + b.2)⊢ b.1 = b.2 norm_num[Nat.add_mod,pow_mul,this,Nat.dvd_iff_mod_eq_zero,Nat.pow_mod]at*
thisb:ℕ × ℕY:ℕi:¬b = (1, 1)L:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:0 < Y ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YD:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝¹:Y % (b.1 + b.2) = 0this✝:(((b.2 % (b.1 + b.2) % (b.1 + b.2)) ^ 2 % (b.1 + b.2) % (b.1 + b.2)) ^ L % (b.1 + b.2) % (b.1 + b.2) +
b.2 % (b.1 + b.2) % (b.1 + b.2)) %
(b.1 + b.2) =
0 ∧
(((b.2 % (b.1 + b.2) % (b.1 + b.2)) ^ 2 % (b.1 + b.2) % (b.1 + b.2)) ^ L % (b.1 + b.2) % (b.1 + b.2) +
b.1 % (b.1 + b.2) % (b.1 + b.2)) %
(b.1 + b.2) =
0this:True⊢ b.1 = b.2
norm_num[add_comm,b.ext_iff,sq _,←Nat.pow_mod,←Nat.dvd_iff_mod_eq_zero]at*
thisb:ℕ × ℕY:ℕL:ℕi:b.1 = 1 → ¬b.2 = 1g:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = gS:0 < Y ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = YD:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = Ythis✝¹:b.1 + b.2 ∣ Ythis✝:b.1 + b.2 ∣ b.2 + (b.2 * b.2) ^ L ∧ b.1 + b.2 ∣ b.1 + (b.2 * b.2) ^ Lthis:True⊢ b.1 = b.2
zify at*
thisb:ℕ × ℕY:ℕL:ℕthis✝¹:Truei:↑b.1 = 1 → ¬↑b.2 = 1g:0 < ↑b.1 ∧ 0 < ↑b.2 ∧ ∃ g, 0 < ↑g ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑gS:0 < ↑Y ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YD:0 < ↑Y ∧ 0 < ↑L ∧ ∀ (n : ℕ), ↑L ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑Ythis✝:↑b.1 + ↑b.2 ∣ ↑Ythis:↑b.1 + ↑b.2 ∣ ↑b.2 + (↑b.2 * ↑b.2) ^ L ∧ ↑b.1 + ↑b.2 ∣ ↑b.1 + (↑b.2 * ↑b.2) ^ L⊢ ↑b.1 = ↑b.2
cases this.1.sub this.2with|_ Z=>
this.introb:ℕ × ℕY:ℕL:ℕthis✝¹:Truei:↑b.1 = 1 → ¬↑b.2 = 1g:0 < ↑b.1 ∧ 0 < ↑b.2 ∧ ∃ g, 0 < ↑g ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑gS:0 < ↑Y ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YD:0 < ↑Y ∧ 0 < ↑L ∧ ∀ (n : ℕ), ↑L ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑Ythis✝:↑b.1 + ↑b.2 ∣ ↑Ythis:↑b.1 + ↑b.2 ∣ ↑b.2 + (↑b.2 * ↑b.2) ^ L ∧ ↑b.1 + ↑b.2 ∣ ↑b.1 + (↑b.2 * ↑b.2) ^ LZ:ℤh✝:↑b.2 + (↑b.2 * ↑b.2) ^ L - (↑b.1 + (↑b.2 * ↑b.2) ^ L) = (↑b.1 + ↑b.2) * Z⊢ ↑b.1 = ↑b.2 nlinarith [ (by
b:ℕ × ℕY:ℕL:ℕthis✝¹:Truei:↑b.1 = 1 → ¬↑b.2 = 1g:0 < ↑b.1 ∧ 0 < ↑b.2 ∧ ∃ g, 0 < ↑g ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑gS:0 < ↑Y ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YD:0 < ↑Y ∧ 0 < ↑L ∧ ∀ (n : ℕ), ↑L ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑Ythis✝:↑b.1 + ↑b.2 ∣ ↑Ythis:↑b.1 + ↑b.2 ∣ ↑b.2 + (↑b.2 * ↑b.2) ^ L ∧ ↑b.1 + ↑b.2 ∣ ↑b.1 + (↑b.2 * ↑b.2) ^ LZ:ℤh✝:↑b.2 + (↑b.2 * ↑b.2) ^ L - (↑b.1 + (↑b.2 * ↑b.2) ^ L) = (↑b.1 + ↑b.2) * Z⊢ Z = 0 (nlinarith
All goals completed! 🐙): Z=0 )]
apply@Nat.modEq_of_dvd
this.ab:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 + b.2 ∣ Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ ↑(b.1 + b.2) ∣ ↑(b.2 ^ 2) - ↑(b.1 ^ 2)
use(b.snd)-b.fst , (by
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 + b.2 ∣ Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ ↑b.2 ^ 2 - ↑b.1 ^ 2 = (↑b.1 + ↑b.2) * (↑b.2 - ↑b.1)·
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 + b.2 ∣ Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ ↑b.2 ^ 2 - ↑b.1 ^ 2 = (↑b.1 + ↑b.2) * (↑b.2 - ↑b.1)ring
All goals completed! 🐙: ( (b.snd) : ℤ)^2-b.fst^2=(b.fst+(b).2) * _)
norm_num[(2).le_mul_of_pos_left,Nat.gcd_dvd,← D.2.2 (2 *L), this.trans, (D.right.1 :_)]
All goals completed! 🐙
suffices:b.1+b.2∣b.1^(2*L)+b.2 ∧b.1+b.2 ∣b.snd^ (2 *L) +b.1
zero.refine_2.refine_1b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ b.1 + b.2 ∣ Y
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Y⊢ b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1
·
zero.refine_2.refine_1b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ b.1 + b.2 ∣ Y exact D.2.2 (2 *(L )) (le_mul_of_one_le_left' (by
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 + b.2 ∣ b.1 ^ (2 * L) + b.2 ∧ b.1 + b.2 ∣ b.2 ^ (2 * L) + b.1⊢ 1 ≤ 2 decide
All goals completed! 🐙 ) )▸dvd_gcd (this.left) (this).2
exfalso
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Y⊢ False
-- First, assume ab + 1 | g.
suffices:b.1*b.2+1∣Y
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 * b.2 + 1 ∣ Y⊢ False
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Y⊢ b.1 * b.2 + 1 ∣ Y
·
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 * b.2 + 1 ∣ Y⊢ False suffices:b.1^φ (b.1*b.2+1)%(b.1*b.2+1)=1%(b.1*b.2+1) ∧b.2^ φ (b.1* b.snd+1)%((b).1 * ↑(b.snd)+1)= 1% (b.1*b.snd + 1)
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ False
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 * b.2 + 1 ∣ Y⊢ b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)
·
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ False /- Then ab + 1 | a ^ (Nφ(ab + 1)) + b and
ab + 1 | b ^ (Nφ(ab + 1)) + a. -/
absurd D.2.2 (φ (b.1*b.2+1)*L) (by
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ φ (b.1 * b.2 + 1) * L ≥ L nlinarith [((b.fst *b.2+1).totient_pos).2 ↑ Fin.size_pos']
All goals completed! 🐙)
apply mt (.▸Nat.gcd_dvd _ _)
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ ¬(Y ∣ b.1 ^ (φ (b.1 * b.2 + 1) * L) + b.2 ∧ Y ∣ b.2 ^ (φ (b.1 * b.2 + 1) * L) + b.1)
useλH=>absurd (‹_∣Y›.trans H.1) (λv=>absurd (‹_∣Y›.trans H.2) ? _)
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)H:Y ∣ b.1 ^ (φ (b.1 * b.2 + 1) * L) + b.2 ∧ Y ∣ b.2 ^ (φ (b.1 * b.2 + 1) * L) + b.1v:b.1 * b.2 + 1 ∣ b.1 ^ (φ (b.1 * b.2 + 1) * L) + b.2⊢ ¬b.1 * b.2 + 1 ∣ b.2 ^ (φ (b.1 * b.2 + 1) * L) + b.1
norm_num[pow_mul,b.ext_iff,(1).mod_eq_of_lt,g.symm,this,Nat.add_mod,Nat.dvd_iff_mod_eq_zero,Nat.pow_mod]at(i)v⊢
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YL:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis✝:b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)H:Y ∣ b.1 ^ (φ (b.1 * b.2 + 1) * L) + b.2 ∧ Y ∣ b.2 ^ (φ (b.1 * b.2 + 1) * L) + b.1i:b.1 = 1 → ¬b.2 = 1v:(1 % (b.1 * b.2 + 1) + b.2 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) % (b.1 * b.2 + 1) = 0⊢ ¬(1 % (b.1 * b.2 + 1) + b.1 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) % (b.1 * b.2 + 1) = 0
/- By Euler's Theorem, a ^ (Nφ(ab + 1)) ≡ 1 (mod ab + 1),
so ab + 1 | b + 1 and ab + 1 | a + 1. -/
norm_num[add_comm,pow_mul,<-Nat.dvd_iff_mod_eq_zero]at*
thisb:ℕ × ℕY:ℕL:ℕthis✝:b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)i:b.1 = 1 → ¬b.2 = 1g:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = gS:0 < Y ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = YD:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = YH:Y ∣ b.2 + (b.1 ^ φ (b.1 * b.2 + 1)) ^ L ∧ Y ∣ b.1 + (b.2 ^ φ (b.1 * b.2 + 1)) ^ Lv:b.1 * b.2 + 1 ∣ b.2 + 1⊢ ¬b.1 * b.2 + 1 ∣ b.1 + 1
contrapose! i
thisb:ℕ × ℕY:ℕL:ℕthis✝:b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)g:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = gS:0 < Y ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = YD:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n) = YH:Y ∣ b.2 + (b.1 ^ φ (b.1 * b.2 + 1)) ^ L ∧ Y ∣ b.1 + (b.2 ^ φ (b.1 * b.2 + 1)) ^ Lv:b.1 * b.2 + 1 ∣ b.2 + 1i:b.1 * b.2 + 1 ∣ b.1 + 1⊢ b.1 = 1 ∧ b.2 = 1
zify at*
thisb:ℕ × ℕY:ℕL:ℕthis✝:↑b.1 * ↑b.2 + 1 ∣ ↑Ythis:↑b.1 ^ φ (b.1 * b.2 + 1) % (↑b.1 * ↑b.2 + 1) = 1 % (↑b.1 * ↑b.2 + 1) ∧
↑b.2 ^ φ (b.1 * b.2 + 1) % (↑b.1 * ↑b.2 + 1) = 1 % (↑b.1 * ↑b.2 + 1)g:0 < ↑b.1 ∧ 0 < ↑b.2 ∧ ∃ g, 0 < ↑g ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑gS:0 < ↑Y ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YD:0 < ↑Y ∧ 0 < ↑L ∧ ∀ (n : ℕ), ↑L ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YH:↑Y ∣ ↑b.2 + (↑b.1 ^ φ (b.1 * b.2 + 1)) ^ L ∧ ↑Y ∣ ↑b.1 + (↑b.2 ^ φ (b.1 * b.2 + 1)) ^ Lv:↑b.1 * ↑b.2 + 1 ∣ ↑b.2 + 1i:↑b.1 * ↑b.2 + 1 ∣ ↑b.1 + 1⊢ ↑b.1 = 1 ∧ ↑b.2 = 1
/- Thus ab + 1 ≤ b + 1 and ab + 1 ≤ a + 1 which requires
a = b = 1 as desired. -/
repeat use by
b:ℕ × ℕY:ℕL:ℕthis✝:↑b.1 * ↑b.2 + 1 ∣ ↑Ythis:↑b.1 ^ φ (b.1 * b.2 + 1) % (↑b.1 * ↑b.2 + 1) = 1 % (↑b.1 * ↑b.2 + 1) ∧
↑b.2 ^ φ (b.1 * b.2 + 1) % (↑b.1 * ↑b.2 + 1) = 1 % (↑b.1 * ↑b.2 + 1)g:0 < ↑b.1 ∧ 0 < ↑b.2 ∧ ∃ g, 0 < ↑g ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑gS:0 < ↑Y ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YD:0 < ↑Y ∧ 0 < ↑L ∧ ∀ (n : ℕ), ↑L ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YH:↑Y ∣ ↑b.2 + (↑b.1 ^ φ (b.1 * b.2 + 1)) ^ L ∧ ↑Y ∣ ↑b.1 + (↑b.2 ^ φ (b.1 * b.2 + 1)) ^ Lv:↑b.1 * ↑b.2 + 1 ∣ ↑b.2 + 1i:↑b.1 * ↑b.2 + 1 ∣ ↑b.1 + 1⊢ ↑b.2 = 1 nlinarith[Int.le_of_dvd (by
b:ℕ × ℕY:ℕL:ℕthis✝:↑b.1 * ↑b.2 + 1 ∣ ↑Ythis:↑b.1 ^ φ (b.1 * b.2 + 1) % (↑b.1 * ↑b.2 + 1) = 1 % (↑b.1 * ↑b.2 + 1) ∧
↑b.2 ^ φ (b.1 * b.2 + 1) % (↑b.1 * ↑b.2 + 1) = 1 % (↑b.1 * ↑b.2 + 1)g:0 < ↑b.1 ∧ 0 < ↑b.2 ∧ ∃ g, 0 < ↑g ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑gS:0 < ↑Y ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YD:0 < ↑Y ∧ 0 < ↑L ∧ ∀ (n : ℕ), ↑L ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YH:↑Y ∣ ↑b.2 + (↑b.1 ^ φ (b.1 * b.2 + 1)) ^ L ∧ ↑Y ∣ ↑b.1 + (↑b.2 ^ φ (b.1 * b.2 + 1)) ^ Lv:↑b.1 * ↑b.2 + 1 ∣ ↑b.2 + 1i:↑b.1 * ↑b.2 + 1 ∣ ↑b.1 + 1⊢ 0 < ↑b.2 + 1 linarith
All goals completed! 🐙) v,Int.le_of_dvd (by
b:ℕ × ℕY:ℕL:ℕthis✝:↑b.1 * ↑b.2 + 1 ∣ ↑Ythis:↑b.1 ^ φ (b.1 * b.2 + 1) % (↑b.1 * ↑b.2 + 1) = 1 % (↑b.1 * ↑b.2 + 1) ∧
↑b.2 ^ φ (b.1 * b.2 + 1) % (↑b.1 * ↑b.2 + 1) = 1 % (↑b.1 * ↑b.2 + 1)g:0 < ↑b.1 ∧ 0 < ↑b.2 ∧ ∃ g, 0 < ↑g ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑gS:0 < ↑Y ∧ ∃ x, 0 < ↑x ∧ ∀ (n : ℕ), ↑x ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YD:0 < ↑Y ∧ 0 < ↑L ∧ ∀ (n : ℕ), ↑L ≤ ↑n → ↑((b.2 + b.1 ^ n).gcd (b.1 + b.2 ^ n)) = ↑YH:↑Y ∣ ↑b.2 + (↑b.1 ^ φ (b.1 * b.2 + 1)) ^ L ∧ ↑Y ∣ ↑b.1 + (↑b.2 ^ φ (b.1 * b.2 + 1)) ^ Lv:↑b.1 * ↑b.2 + 1 ∣ ↑b.2 + 1i:↑b.1 * ↑b.2 + 1 ∣ ↑b.1 + 1⊢ 0 < ↑b.1 + 1 linarith
All goals completed! 🐙) i]
repeat use↑(Nat.ModEq.pow_totient (by
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Ythis:b.1 * b.2 + 1 ∣ Y⊢ b.2.Coprime (b.1 * b.2 + 1) norm_num
All goals completed! 🐙))
-- Now, we proceed to show that indeed ab + 1 | g.
by_contra! H
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Y⊢ False
suffices:b.1^φ (b.1*b.2+1)%(b.1*b.2+1)=1%(b.1*b.2+1) ∧b.2^φ (b.1*b.2+1)%(b.1*b.2+1)=1%( b.fst * ↑ (b.snd)+1)
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ False
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Y⊢ b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)
·
thisb:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ False simp_all
thisb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ False
/- It suffices to show that
ab + 1 | a^(φ(ab + 1)(N + 1) - 1) + b and
ab + 1 | b^(φ(ab + 1)(N + 1) - 1) + a. -/
suffices:b.1*b.2+1∣b.1^(φ (b.1*b.2+1)*(L+1)-1)+b.2 ∧b.1*b.2+1∣b.2^(φ (b.1* b.2+1)* (L+1)-1)+(b.fst)
thisb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Ythis✝:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)this:b.1 * b.2 + 1 ∣ b.1 ^ (φ (b.1 * b.2 + 1) * (L + 1) - 1) + b.2 ∧
b.1 * b.2 + 1 ∣ b.2 ^ (φ (b.1 * b.2 + 1) * (L + 1) - 1) + b.1⊢ False
thisb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ b.1 * b.2 + 1 ∣ b.1 ^ (φ (b.1 * b.2 + 1) * (L + 1) - 1) + b.2 ∧
b.1 * b.2 + 1 ∣ b.2 ^ (φ (b.1 * b.2 + 1) * (L + 1) - 1) + b.1
·
thisb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Ythis✝:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)this:b.1 * b.2 + 1 ∣ b.1 ^ (φ (b.1 * b.2 + 1) * (L + 1) - 1) + b.2 ∧
b.1 * b.2 + 1 ∣ b.2 ^ (φ (b.1 * b.2 + 1) * (L + 1) - 1) + b.1⊢ False use H$ D.2.2 (φ _ *(L+1)-1) (L.le_sub_of_add_le (by
b:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Ythis✝:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)this:b.1 * b.2 + 1 ∣ b.1 ^ (φ (b.1 * b.2 + 1) * (L + 1) - 1) + b.2 ∧
b.1 * b.2 + 1 ∣ b.2 ^ (φ (b.1 * b.2 + 1) * (L + 1) - 1) + b.1⊢ L + 1 ≤ φ (b.1 * b.2 + 1) * (L + 1) nlinarith[((b.1* b.2+1).totient_pos).2 Nat.succ_pos']
All goals completed! 🐙))▸(((Nat.dvd_gcd) ( this).1)) this.right
cases unused variable `B`
note: this linter can be disabled with `set_option linter.unusedVariables false`B:Nat.exists_eq_add_of_lt$ ((b.1*b.2+1).totient_pos).2 (by
b:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Ythis:b.1 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1) ∧
b.2 ^ φ (b.1 * b.2 + 1) % (b.1 * b.2 + 1) = 1 % (b.1 * b.2 + 1)⊢ 0 < b.1 * b.2 + 1 continuity
All goals completed! 🐙)
norm_num[*, g, ‹φ _ = _›, mul_add,Nat.pow_mod,(1).mod_eq_of_lt,pow_add,Nat.add_mod,pow_mul,Nat.dvd_iff_mod_eq_zero,Nat.mul_mod] at this⊢
this.introb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1B:⋯ = ⋯this:(b.1 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) ^ w✝ % (b.1 * b.2 + 1) % (b.1 * b.2 + 1) *
(b.1 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) %
(b.1 * b.2 + 1) =
1 ∧
(b.2 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) ^ w✝ % (b.1 * b.2 + 1) % (b.1 * b.2 + 1) *
(b.2 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) %
(b.1 * b.2 + 1) =
1⊢ (((b.1 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) ^ w✝ % (b.1 * b.2 + 1) % (b.1 * b.2 + 1) *
(b.1 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) %
(b.1 * b.2 + 1) %
(b.1 * b.2 + 1)) ^
L %
(b.1 * b.2 + 1) %
(b.1 * b.2 + 1) *
((b.1 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) ^ w✝ % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) %
(b.1 * b.2 + 1) %
(b.1 * b.2 + 1) +
b.2 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) %
(b.1 * b.2 + 1) =
0 ∧
(((b.2 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) ^ w✝ % (b.1 * b.2 + 1) % (b.1 * b.2 + 1) *
(b.2 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) %
(b.1 * b.2 + 1) %
(b.1 * b.2 + 1)) ^
L %
(b.1 * b.2 + 1) %
(b.1 * b.2 + 1) *
((b.2 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) ^ w✝ % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) %
(b.1 * b.2 + 1) %
(b.1 * b.2 + 1) +
b.1 % (b.1 * b.2 + 1) % (b.1 * b.2 + 1)) %
(b.1 * b.2 + 1) =
0
simp_all
this.introb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1⊢ ((1 % (b.1 * b.2 + 1)) ^ L * (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2) % (b.1 * b.2 + 1) = 0 ∧
((1 % (b.1 * b.2 + 1)) ^ L * (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1) % (b.1 * b.2 + 1) = 0
/- Since a, b are coprime to ab + 1, it suffices to show that
ab + 1 | a(a^(φ(ab + 1)(N + 1) - 1) + b) and
ab + 1 | b(b^(φ(ab + 1)(N + 1) - 1) + a). -/
suffices:b.1*b.2+1∣b.1*( (b.1%((b).1 * ( b.snd) + 1) : _)^‹Nat› +b.snd) ∧(b.fst * ↑(b.snd) + 1)∣(b).snd*( (b.snd%((b).fst * b.snd + 1))^ ‹Nat›+b.fst)
this.introb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this✝:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1this:b.1 * b.2 + 1 ∣ b.1 * ((b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2) ∧ b.1 * b.2 + 1 ∣ b.2 * ((b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1)⊢ ((1 % (b.1 * b.2 + 1)) ^ L * (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2) % (b.1 * b.2 + 1) = 0 ∧
((1 % (b.1 * b.2 + 1)) ^ L * (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1) % (b.1 * b.2 + 1) = 0
thisb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1⊢ b.1 * b.2 + 1 ∣ b.1 * ((b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2) ∧ b.1 * b.2 + 1 ∣ b.2 * ((b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1)
·
this.introb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this✝:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1this:b.1 * b.2 + 1 ∣ b.1 * ((b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2) ∧ b.1 * b.2 + 1 ∣ b.2 * ((b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1)⊢ ((1 % (b.1 * b.2 + 1)) ^ L * (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2) % (b.1 * b.2 + 1) = 0 ∧
((1 % (b.1 * b.2 + 1)) ^ L * (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1) % (b.1 * b.2 + 1) = 0 norm_num[<-Nat.dvd_iff_mod_eq_zero,g,(1).mod_eq_of_lt,Nat.dvd_mul] at this⊢
this.introb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this✝:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1this:(∃ y, y ∣ b.1 ∧ ∃ x, x ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 ∧ y * x = b.1 * b.2 + 1) ∧
∃ y, y ∣ b.2 ∧ ∃ x, x ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1 ∧ y * x = b.1 * b.2 + 1⊢ b.1 * b.2 + 1 ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 ∧ b.1 * b.2 + 1 ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1
exists@?_
this.intro.refine_1b:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this✝:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1this:(∃ y, y ∣ b.1 ∧ ∃ x, x ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 ∧ y * x = b.1 * b.2 + 1) ∧
∃ y, y ∣ b.2 ∧ ∃ x, x ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1 ∧ y * x = b.1 * b.2 + 1⊢ b.1 * b.2 + 1 ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2
this.intro.refine_2b:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this✝:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1this:(∃ y, y ∣ b.1 ∧ ∃ x, x ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 ∧ y * x = b.1 * b.2 + 1) ∧
∃ y, y ∣ b.2 ∧ ∃ x, x ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1 ∧ y * x = b.1 * b.2 + 1⊢ b.1 * b.2 + 1 ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1
·
this.intro.refine_1b:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this✝:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1this:(∃ y, y ∣ b.1 ∧ ∃ x, x ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 ∧ y * x = b.1 * b.2 + 1) ∧
∃ y, y ∣ b.2 ∧ ∃ x, x ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1 ∧ y * x = b.1 * b.2 + 1⊢ b.1 * b.2 + 1 ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 cases this.1 with|_ Q r=>
this.intro.refine_1.introb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this✝:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1this:(∃ y, y ∣ b.1 ∧ ∃ x, x ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 ∧ y * x = b.1 * b.2 + 1) ∧
∃ y, y ∣ b.2 ∧ ∃ x, x ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1 ∧ y * x = b.1 * b.2 + 1Q:ℕr:Q ∣ b.1 ∧ ∃ x, x ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 ∧ Q * x = b.1 * b.2 + 1⊢ b.1 * b.2 + 1 ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2simp_all[(Q.dvd_gcd r.1 ⟨_,.symm r.right.choose_spec.2⟩).antisymm]
All goals completed! 🐙
cases@this.2with|_ F X=>
this.intro.refine_2.introb:ℕ × ℕY:ℕL:ℕg:0 < b.1 ∧ 0 < b.2 ∧ ∃ g, 0 < g ∧ ∃ x, 0 < x ∧ ∀ (n : ℕ), x ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = gS:∃ N, 0 < N ∧ ∀ (n : ℕ), N ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)D:0 < Y ∧ 0 < L ∧ ∀ (n : ℕ), L ≤ n → (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Yw✝:ℕh✝:φ (b.1 * b.2 + 1) = 0 + w✝ + 1this✝:(b.1 % (b.1 * b.2 + 1)) ^ w✝ * b.1 % (b.1 * b.2 + 1) = 1 ∧ (b.2 % (b.1 * b.2 + 1)) ^ w✝ * b.2 % (b.1 * b.2 + 1) = 1this:(∃ y, y ∣ b.1 ∧ ∃ x, x ∣ (b.1 % (b.1 * b.2 + 1)) ^ w✝ + b.2 ∧ y * x = b.1 * b.2 + 1) ∧
∃ y, y ∣ b.2 ∧ ∃ x, x ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1 ∧ y * x = b.1 * b.2 + 1F:ℕX:F ∣ b.2 ∧ ∃ x, x ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1 ∧ F * x = b.1 * b.2 + 1⊢ b.1 * b.2 + 1 ∣ (b.2 % (b.1 * b.2 + 1)) ^ w✝ + b.1simp_all[(F.dvd_gcd X.1 ⟨_,symm X.2.choose_spec.2⟩).antisymm]
All goals completed! 🐙
/- This follows from Euler's Theorem:
a(a^(φ(ab + 1)(N + 1) - 1) + b)
≡ a^(φ(ab + 1)(N + 1)) + ab
≡ 1 + ab
≡ 0 (mod ab + 1)
and similarly for b(b^(φ(ab + 1)(N + 1) - 1) + a). -/
simp_all[mul_comm, mul_add,add_comm,Nat.add_mod,Nat.dvd_iff_mod_eq_zero]
All goals completed! 🐙
repeat use(Nat.ModEq.pow_totient (by
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Y⊢ b.2.Coprime (b.1 * b.2 + 1) .
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Y⊢ b.2.Coprime (b.1 * b.2 + 1) .
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Y⊢ b.2.Coprime (b.1 * b.2 + 1) .
b:ℕ × ℕg:b ∈ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g}Y:ℕS:∃ N, 0 < Y ∧ 0 < N ∧ ∀ n ≥ N, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = Yi:¬b = (1, 1)L:ℕD:0 < Y ∧ 0 < L ∧ ∀ n ≥ L, (b.1 ^ n + b.2).gcd (b.2 ^ n + b.1) = YH:¬b.1 * b.2 + 1 ∣ Y⊢ b.2.Coprime (b.1 * b.2 + 1)norm_num
All goals completed! 🐙) )
congr 26
All goals completed! 🐙
The following command shows which axioms the proof relies upon:
'imo_2024_p2' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms imo_2024_p2
'imo_2024_p2' depends on axioms: [propext, Classical.choice, Quot.sound]
These are the standard built in axioms.