Skip to main content

Challenge 5: 5²ⁿ - 2³ⁿ is divisible by 17

Also available in:

Español

Prove in Lean 4 that 5²ⁿ - 2³ⁿ is divisible by 17 for every natural number n.

To do so, complete the following Lean 4 theory:

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

variable (n : ℕ)

open Nat

example : 17 ∣ 5^(2 * n) - 2^(3 * n) := by
  sorry

1. Proofs in natural language

Proof 1 in natural language (NL1)

Considering that \begin{array}{ll} 5^{2n} - 2^{3n} &= (5^2)^n - (2^3)^n \\ &= 25^n - 8^n \end{array} What we have to prove is that, for every natural number \(n\), \[ 17 \mid 25^n - 8^n \] We prove it by induction.

Base case (\(n = 0\)): \begin{array}{ll} 25^n - 8^n &= 25^0 - 8^0 \\ &= 0 \end{array} which is divisible by 17.

Inductive step: Suppose that \[ 17 \mid 25^n - 8^n \tag{IH} \] and, therefore, there exists a \(k\) such that \[ 25^n - 8^n = 17k \tag{1} \] We have to prove that \[ 17 \mid 25^{n+1} - 8^{n+1} \] Hence, \begin{array}{lll} 25^{n+1} - 8^{n+1} &= 25 \times 25^n − 8 \times 8^n \\ &= (17+8) \times 25^n − 8 \times 8^n \\ &= 17 \times 25^n + 8 \times 25^n − 8 \times 8^n \\ &= 17 \times 25^n + 8 \times (25^n − 8^n) \\ &= 17 \times 25^n + 8 \times 17k &\text{[by (1)]} \\ &= 17 \times (25^n + 8k) \end{array} Therefore, \[ 17 \mid 25^{n+1} - 8^{n+1} \]

Proof 2 in natural language (NL2)

By induction on \(n\).

Base case (\(n = 0\)) \[ 5^{2 \times 0} - 2^{3 \times 0} = 0 \] which is divisible by 17.

Inductive step: Suppose that \[ 17 \mid 5^{2n} - 2^{3n} \] and we have to prove that \[ 17 \mid 5^{2n+1} − 2^{3n+1} \] From the IH, there exists a \(k\) such that \[ 5^{2n} - 2^{3n} = 17k \tag{1} \] Hence, \begin{array}{ll} 5^{2n+1} − 2^{3n+1} &= 5^{2n} \times 5^2 − 2^{3n} \times 2^3 \\ &= (17k + 2^{3n}) \times 5^2 − 2^{3n} \times 2^3 &\text{[by (1)]} \\ &= 17k \times 25 + 25 \times 2^{3n} − 8 \times 2^{3n} \\ &= 17 \times (25k) + (25 - 8) \times 2^{3n} \\ &= 17 \times (25k + 2^{3n}) \end{array} Therefore, \[ 17 \mid 5^{2n+1} − 2^{3n+1} \]

Proof 3 in natural language (NL3)

Using modular arithmetic \begin{array}{ll} 5^{2n} - 2^{3n} &= 25^n − 8^n \\ &\equiv 8^n − 8^n \pmod{17} \\ &\equiv 0 \pmod{17} \end{array}

Proof 4 in natural language (NL4)

We have that \[ 5^{2n} - 2^{3n} = 25^n − 8^n \] which is divisible by \(25 - 8\) (since \(x^n - y^n\) is divisible by \(x - y\)). Therefore, \(5^{2n} - 2^{3n}\) is divisible by 17.

2. Proofs in Lean 4

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

variable (n : ℕ)

open Nat

-- Proof 1 (based on NL1)
-- ======================

namespace Proof1

lemma L1 : (17 * 25^n + 8 * 25^n) - 8 * 8^n =
           17 * 25^n + (8 * 25^n - 8 * 8^n) :=
by
  apply Nat.add_sub_assoc
  -- ⊢ 8 * 8 ^ n ≤ 8 * 25 ^ n
  bound

lemma L2 : 17 ∣ 25^n - 8^n :=
by
  induction n with
  | zero =>
    -- ⊢ 17 ∣ 25 ^ 0 - 8 ^ 0
    simp
  | succ n HI =>
    -- n : ℕ
    -- HI : 17 ∣ 25 ^ n - 8 ^ n
    -- ⊢ 17 ∣ 25 ^ (n + 1) - 8 ^ (n + 1)
    obtain ⟨k, hk⟩ := HI
    -- k : ℕ
    -- hk : 25 ^ n - 8 ^ n = 17 * k
    use 25^n + 8*k
    -- ⊢ 25 ^ (n + 1) - 8 ^ (n + 1) = 17 * (25 ^ n + 8 * k)
    calc 25 ^ (n + 1) - 8 ^ (n + 1)
     _ = 25 * 25^n - 8 * 8^n              := by grind
     _ = (17+8) * 25^n - 8 * 8^n          := by grind
     _ = (17 * 25^n + 8 * 25^n) - 8 * 8^n := by grind
     _ = 17 * 25^n + (8 * 25^n - 8 * 8^n) := L1 n
     _ = 17 * 25^n + 8 * (25^n - 8^n)     := by grind
     _ = 17 * 25^n + 8 * 17*k             := by grind
     _ = 17 * (25^n + 8 * k)              := by grind
     _ = 17 * (25 ^ n + 8 * k)            := by grind

example : 17 ∣ 5^(2 * n) - 2^(3 * n) :=
by
  have h1 : 5^(2 * n) - 2^(3 * n) = 25^n - 8^n :=
    by calc 5^(2 * n) - 2^(3 * n)
          = (5^2)^n - (2^3)^n     := by simp only [pow_mul]
        _ = 25^n - 8^n            := by norm_num
  rw [h1]
  -- ⊢ 17 ∣ 25 ^ n - 8 ^ n
  exact L2 n

end Proof1

-- Proof 2 (explicit version of Proof 1)
-- =====================================

namespace Proof2

lemma L1 : (17 * 25^n + 8 * 25^n) - 8 * 8^n =
           17 * 25^n + (8 * 25^n - 8 * 8^n) :=
by
  apply Nat.add_sub_assoc
  -- ⊢ 8 * 8 ^ n ≤ 8 * 25 ^ n
  bound

example : 25 ^ (n + 1) = 25^n * 25 := by simp only [Nat.pow_add_one]

lemma L2 : 17 ∣ 25^n - 8^n :=
by
  induction n with
  | zero =>
    -- ⊢ 17 ∣ 25 ^ 0 - 8 ^ 0
    simp
  | succ n HI =>
    -- n : ℕ
    -- HI : 17 ∣ 25 ^ n - 8 ^ n
    -- ⊢ 17 ∣ 25 ^ (n + 1) - 8 ^ (n + 1)
    obtain ⟨k, hk⟩ := HI
    -- k : ℕ
    -- hk : 25 ^ n - 8 ^ n = 17 * k
    use 25^n + 8*k
    -- ⊢ 25 ^ (n + 1) - 8 ^ (n + 1) = 17 * (25 ^ n + 8 * k)
    calc 25 ^ (n + 1) - 8 ^ (n + 1)
     _ = 25^n * 25 - 8^n * 8              := by simp only [Nat.pow_add_one]
     _ = 25 * 25^n - 8 * 8^n              := by simp only [mul_comm]
     _ = (17+8) * 25^n - 8 * 8^n          := by norm_num
     _ = (17 * 25^n + 8 * 25^n) - 8 * 8^n := by simp only [right_distrib]
     _ = 17 * 25^n + (8 * 25^n - 8 * 8^n) := L1 n
     _ = 17 * 25^n + 8 * (25^n - 8^n)     := by simp only [Nat.mul_sub]
     _ = 17 * 25^n + 8 * (17 * k)         := by rw [hk]
     _ = 17 * (25^n + 8 * k)              := by simp +arith

example : 17 ∣ 5^(2 * n) - 2^(3 * n) :=
by
  have h1 : 5^(2 * n) - 2^(3 * n) = 25^n - 8^n :=
    by calc 5^(2 * n) - 2^(3 * n)
          = (5^2)^n - (2^3)^n     := by simp only [pow_mul]
        _ = 25^n - 8^n            := by norm_num
  rw [h1]
  -- ⊢ 17 ∣ 25 ^ n - 8 ^ n
  exact L2 n

end Proof2

-- Proof 3 (based on NL2)
-- ======================

namespace Proof3

lemma L1 : 2^(3*n) ≤ 5^(2*n) := by
  have h : 2^3 ≤ 5^2 := by norm_num
  calc 2^(3*n)
       = (2^3)^n := pow_mul 2 3 n
     _ ≤ (5^2)^n := Nat.pow_le_pow_left h n
     _ = 5^(2*n) := (pow_mul 5 2 n).symm

example : 17 ∣ 5^(2 * n) - 2^(3 * n) :=
by
  induction n with
  | zero =>
    -- ⊢ 17 ∣ 5 ^ (2 * 0) - 2 ^ (3 * 0)
    simp
  | succ n HI =>
    -- n : ℕ
    -- HI : 17 ∣ 5 ^ (2 * n) - 2 ^ (3 * n)
    -- ⊢ 17 ∣ 5 ^ (2 * (n + 1)) - 2 ^ (3 * (n + 1))
    obtain ⟨k, hk⟩ := HI
    -- k : ℕ
    -- hk : 5^(2*n)-2^(3*n) = 17*k
    use 25 * k + 2 ^ (3 * n)
    -- ⊢ 5^(2*(n+1))-2^(3*(n+1)) = 17*(25*k+2^(3*n))
    calc 5^(2*(n+1))-2^(3*(n+1))
         = 5^(2*n)*5^2-2^(3*n)*2^3         := by grind
       _ = (17*k+2^(3*n))*5^2-2^(3*n)*2^3  := by grind [L1]
       _ = 17*k*25+25*2^(3*n)-8*2^(3*n)    := by grind
       _ = 17*(25*k)+(25-8)*2^(3*n)        := by grind
       _ = 17*(25*k+2^(3*n))               := by grind

end Proof3

-- Proof 4 (explicit version of Proof 3)
-- =====================================

namespace Proof4

lemma L1 : 2^(3*n) ≤ 5^(2*n) := by
  have h : 2^3 ≤ 5^2 := by norm_num
  calc 2^(3*n)
       = (2^3)^n := pow_mul 2 3 n
     _ ≤ (5^2)^n := Nat.pow_le_pow_left h n
     _ = 5^(2*n) := (pow_mul 5 2 n).symm

lemma L2
  (hk : 5 ^ (2 * n) - 2 ^ (3 * n) = 17 * k)
  : 5 ^ (2 * n) = 17 * k + 2 ^ (3 * n) :=
(Nat.sub_eq_iff_eq_add (L1 n)).mp hk

example : 17 ∣ 5^(2 * n) - 2^(3 * n) :=
by
  induction n with
  | zero =>
    -- ⊢ 17 ∣ 5 ^ (2 * 0) - 2 ^ (3 * 0)
    simp
  | succ n HI =>
    -- n : ℕ
    -- HI : 17 ∣ 5 ^ (2 * n) - 2 ^ (3 * n)
    -- ⊢ 17 ∣ 5 ^ (2 * (n + 1)) - 2 ^ (3 * (n + 1))
    obtain ⟨k, hk⟩ := HI
    -- k : ℕ
    -- hk : 5^(2*n)-2^(3*n) = 17*k
    use 25 * k + 2 ^ (3 * n)
    -- ⊢ 5^(2*(n+1))-2^(3*(n+1)) = 17*(25*k+2^(3*n))
    calc 5^(2*(n+1))-2^(3*(n+1))
         = 5^(2*n+2)-2^(3*n+3)             := by simp +arith only
       _ = 5^(2*n)*5^2-2^(3*n)*2^3         := by noncomm_ring
       _ = (17*k+2^(3*n))*5^2-2^(3*n)*2^3  := by simp [hk, L2]
       _ = 17*k*25+25*2^(3*n)-8*2^(3*n)    := by omega
       _ = 17*(25*k)+(25-8)*2^(3*n)        := by omega
       _ = 17*(25*k+2^(3*n))               := by ring

end Proof4

-- Proof 5 (based on NL3)
-- ======================

namespace Proof5

example : 17 ∣ 5^(2*n) - 2^(3*n) :=
by
  have h1 : 25 ≡ 8 [MOD 17] := by decide
  apply modEq_zero_iff_dvd.mp
  -- ⊢ 5 ^ (2 * n) - 2 ^ (3 * n) ≡ 0 [MOD 17]
  calc 5^(2*n) - 2^(3*n)
       = 25^n - 8^n         := by simp [pow_mul]
     _ ≡ 8^n - 8^n [MOD 17] := by apply ModEq.sub_right
                                  · -- ⊢ 8 ^ n ≤ 25 ^ n
                                    bound
                                  · -- ⊢ 8 ^ n ≤ 8 ^ n
                                    gcongr
                                  exact (ModEq.pow n h1)
     _ = 0                  := by simp
     _ ≡ 0 [MOD 17]         := ModEq.refl 0

end Proof5

-- Proof 6 (based on NL4)
-- ======================

namespace Proof6

example : 17 ∣ (5 ^ (2 * n) - 2 ^ (3 * n)) :=
by
  rw [pow_mul, pow_mul]
  -- ⊢ 17 ∣ (5 ^ 2) ^ n - (2 ^ 3) ^ n
  exact Nat.sub_dvd_pow_sub_pow 25 8 n

-- Note: In the previous proof the induction is hidden in
-- [Nat.sub_dvd_pow_sub_pow](https://1pt.co/34pbu) which uses
-- [pow_le_pow_left](https://1pt.co/ydx7a) which is proved by
-- induction.

end Proof6

-- Proof 7 (simplification of Proof 6)
-- ===================================

namespace Proof7

example (n : ℕ) : 17 ∣ 5 ^ (2 * n) - 2 ^ (3 * n) :=
by
  simpa [pow_mul] using Nat.sub_dvd_pow_sub_pow 25 8 n

end Proof7

-- Proof 10
-- ========

namespace Proof8

variable (k : ℕ)

lemma L1 : 2 ^ (3 * k) ≤ 5 ^ (2 * k) := by
  rw [pow_mul, pow_mul]
  -- ⊢ (2 ^ 3) ^ k ≤ (5 ^ 2) ^ k
  gcongr 1
  -- ⊢ 2 ^ 3 ≤ 5 ^ 2
  norm_num

lemma L2 :
    5 ^ (2 * (k + 1)) - 2 ^ (3 * (k + 1)) =
    17 * 5 ^ (2 * k) + 8 * (5 ^ (2 * k) - 2 ^ (3 * k)) :=
by
  zify [L1 k, L1 (k + 1)]
  -- ⊢ 5^(2*(k+1))-2^(3*(k+1)) = 17*5^(2*k)+8*(5^(2*k)-2^(3*k))
  ring

example : 17 ∣ 5 ^ (2 * n) - 2 ^ (3 * n) := by
  induction n with
  | zero =>
    -- ⊢ 17 ∣ 5 ^ (2 * 0) - 2 ^ (3 * 0)
    simp
  | succ k ih =>
    -- n k k : ℕ
    -- ih : 17 ∣ 5 ^ (2 * k) - 2 ^ (3 * k)
    -- ⊢ 17 ∣ 5 ^ (2 * (k + 1)) - 2 ^ (3 * (k + 1))
    rw [L2 k]
    -- ⊢ 17 ∣ 17*5^(2*k)+8*(5^(2*k)-2^(3*k))
    exact Dvd.dvd.add (Dvd.intro _ rfl) (Dvd.dvd.mul_left ih 8)

end Proof8

-- Lemmas used
-- ===========

variable (a b c m k : ℕ)
#check (Dvd.dvd.add : m ∣ n → m ∣ k → m ∣ n + k)
#check (Dvd.dvd.mul_left : m ∣ n → ∀ k, m ∣ k * n)
#check (Dvd.intro k : m * k = n → m ∣ n)
#check (ModEq.pow m : a ≡ b [MOD n] → a ^ m ≡ b ^ m [MOD n])
#check (ModEq.refl a : a ≡ a [MOD n])
#check (ModEq.sub_right : a ≤ b → a ≤ c → b ≡ c [MOD n] → b - a ≡ c - a [MOD n])
#check (Nat.add_sub_assoc : k ≤ m → ∀ n, n + m - k = n + (m - k))
#check (Nat.mul_sub n m k : n * (m - k) = n * m - n * k)
#check (Nat.mul_sub_left_distrib n m k : n * (m - k) = n * m - n * k)
#check (Nat.pow_add_one n m : n ^ (m + 1) = n ^ m * n)
#check (Nat.pow_le_pow_left : n ≤ m → ∀ k, n ^ k ≤ m ^ k)
#check (Nat.sub_dvd_pow_sub_pow m k n : m - k ∣ m ^ n - k ^ n)
#check (Nat.sub_eq_iff_eq_add : b ≤ a → (a - b = c ↔ a = c + b))
#check (add_zero a : a + 0 = a)
#check (dvd_add : m ∣ n → m ∣ k → m ∣ n + k)
#check (dvd_mul_of_dvd_right : m ∣ n → ∀ k, m ∣ k * n)
#check (dvd_mul_right m n : m ∣ m * n)
#check (modEq_zero_iff_dvd : m ≡ 0 [MOD n] ↔ n ∣ m)
#check (mul_add a b c : a * (b + c) = a * b + a * c)
#check (mul_comm n m : n * m = m * n)
#check (mul_le_mul_left k : n ≤ m → k * n ≤ k * m)
#check (pow_add a m n : a ^ (m + n) = a ^ m * a ^ n)
#check (pow_mul m n k : m ^ (n * k) = (m ^ n) ^ k)
#check (right_distrib n m k : (n + m) * k = n * k + m * k)

You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.

3. Collaborative solutions

Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:

  • Write your proof in live.lean-lang.org and check that it compiles without errors.
  • Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean
   -- your proof
```

Comments