Reto 5: 5²ⁿ - 2³ⁿ es divisible por 17
El reto de esta semana consiste en demostrar en Lean 4 ue, 5²ⁿ - 2³ⁿ es divisible por 17 para todo número natural n.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Nat.Basic import Mathlib.Tactic variable (n : ℕ) open Nat example : 17 ∣ 5^(2 * n) - 2^(3 * n) := by sorry
1. Demostración en lenguaje natural
1ª demostración en lenguaje natural (LN1)
Considerando que \begin{array}{ll} 5^{2n} - 2^{3n} &= (5^2)^n - (2^3)^n \\ &= 25^n - 8^n \end{array} Lo que tenemos que demostrar es que, para todo número natural \(n\), \[ 17 \mid 25^n - 8^n \] Lo haremos por inducción.
Caso base (\(n = 0\)): \begin{array}{ll} 25^n - 8^n &= 25^0 - 8^0 \\ &= 0 \end{array} que es divisble por 17.
Paso de inducción: Supongamos que \[ 17 \mid 25^n - 8^n \tag{HI} \] y, por tanto, existe un \(k\) tal que \[ 25^n - 8^n = 17k \tag{1} \] Tenemos que probar que \[ 17 \mid 25^{n+1} - 8^{n+1} \] Luego, \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{[por (1)]} \\ &= 17 \times (25^n + 8k) \end{array} Por tanto, \[ 17 \mid 25^{n+1} - 8^{n+1} \]
2ª demostración en lenguaje natural (LN2)
Por indución en \(n\).
Caso base (\(n = 0\)) \[ 5^{2 \times 0} - 2^{3 \times 0} = 0 \] que es divisble por 17.
Paso de inducción: Supongamos que \[ 17 \mid 5^{2n} - 2^{3n} \] y tenemos que probar que \[ 17 \mid 5^{2n+1} − 2^{3n+1} \] De la HI, se tiene que existe un \(k\) tal que \[ 5^{2n} - 2^{3n} = 17k \tag{1} \] Luego, \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{[por (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} Por tanto, \[ 17 \mid 5^{2n+1} − 2^{3n+1} \]
3ª demostración en lenguaje natural (LN3)
Usando aritmética modular \begin{array}{ll} 5^{2n} - 2^{3n} &= 25^n − 8^n \\ &\equiv 8^n − 8^n \pmod{17} \\ &\equiv 0 \pmod{17} \end{array}
4ª demostración en lenguaje natural (LN4)
Se tiene que \[ 5^{2n} - 2^{3n} = 25^n − 8^n \] que que es divisible por \(25 - 8\) (ya que \(x^n - y^n\) es divisible por \(x - y\)). Por tanto, \(5^{2n} - 2^{3n}\) es divisible por 17.
2. Demostraciones con Lean 4
import Mathlib.Data.Nat.Basic import Mathlib.Tactic variable (n : ℕ) open Nat -- 1ª demostración (basada en la LN1) -- ================================== namespace Demostracion1 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 Demostracion1 -- 2ª demostración (explicitación de la 1ª) -- ======================================== namespace Demostracion2 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 Demostracion2 -- 3ª demostración (basada en la LN2) -- ================================== namespace Demostracion3 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 Demostracion3 -- 4ª demostración (explicitación de la 3ª) -- ======================================== namespace Demostracion4 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 Demostracion4 -- 5ª demostración (basasa en la LN3) -- ================================== namespace Demostracion5 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 Demostracion5 -- 6ª demostración (hasada en la LN4) -- ================================== namespace Demostracion6 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 -- Nota: En la demostración anterior la inducción está oculta en -- [Nat.sub_dvd_pow_sub_pow](https://1pt.co/34pbu) que usa -- [pow_le_pow_left](https://1pt.co/ydx7a) que se demuestra por -- inducción. end Demostracion6 -- 7ª demostración (simplificación de la 6ª) -- =============== namespace Demostracion7 example (n : ℕ) : 17 ∣ 5 ^ (2 * n) - 2 ^ (3 * n) := by simpa [pow_mul] using Nat.sub_dvd_pow_sub_pow 25 8 n end Demostracion7 -- 8ª demostración con comentarios -- =============================== namespace Demostracion8 example (n : ℕ) : 17 ∣ 5 ^ (2 * n) - 2 ^ (3 * n) := by induction n with | zero => -- Caso base: 5^0 - 2^0 = 0, y 17 | 0. simp | succ k ih => -- 1. Preparar las potencias (usamos 'ring' para manejar la conmutatividad) have h_pow5 : 5 ^ (2 * (k + 1)) = 25 * 5 ^ (2 * k) := by rw [mul_add, pow_add] ring have h_pow2 : 2 ^ (3 * (k + 1)) = 8 * 2 ^ (3 * k) := by rw [mul_add, pow_add] ring rw [h_pow5, h_pow2] -- 2. Demostrar que 2^(3k) ≤ 5^(2k) para poder operar restas en Nat -- (8^k ≤ 25^k) have h_le : 2 ^ (3 * k) ≤ 5 ^ (2 * k) := by rw [pow_mul, pow_mul] -- Nombre corregido: Nat.pow_le_pow_left apply Nat.pow_le_pow_left (by norm_num) -- 3. Aplicar el truco de "sumar y restar" (Método Hirsch / 1ª Forma) -- Descomponemos 25 como (17 + 8) have h_split : 25 * 5 ^ (2 * k) = 17 * 5 ^ (2 * k) + 8 * 5 ^ (2 * k) := by ring rw [h_split] -- Asociamos los términos: 17*5^(2k) + (8*5^(2k) - 8*2^(3k)) -- Nat.add_sub_assoc requiere demostrar que el sustraendo es menor o igual rw [Nat.add_sub_assoc (mul_le_mul_left 8 h_le)] -- 4. Demostrar divisibilidad por partes apply dvd_add · -- Caso: 17 ∣ 17 * ... apply dvd_mul_right · -- Caso: 17 ∣ 8 * (5^(2k) - 2^(3k)) rw [← Nat.mul_sub_left_distrib] apply dvd_mul_of_dvd_right ih end Demostracion8 -- 9ª demostración (factorización de la 8ª) -- ======================================== namespace Demostracion9 example : 17 ∣ 5 ^ (2 * n) - 2 ^ (3 * n) := by induction n with | zero => -- ⊢ 17 ∣ 5 ^ (2 * 0) - 2 ^ (3 * 0) simp | succ k ih => -- k : ℕ -- ih : 17 ∣ 5 ^ (2 * k) - 2 ^ (3 * k) -- ⊢ 17 ∣ 5 ^ (2 * (k + 1)) - 2 ^ (3 * (k + 1)) have h_le : 2 ^ (3 * k) ≤ 5 ^ (2 * k) := by calc 2 ^ (3 * k) = (2 ^ 3) ^ k := pow_mul 2 3 k _ = 8 ^ k := add_zero (NatPow.pow (2 ^ 3) k) _ ≤ 25 ^ k := Nat.pow_le_pow_left (by norm_num) k _ = 5 ^ (2 * k) := (pow_mul 5 2 k).symm have h1 : 5 ^ (2 * (k + 1)) - 2 ^ (3 * (k + 1)) = 17 * 5 ^ (2 * k) + 8 * (5 ^ (2 * k) - 2 ^ (3 * k)) := calc 5 ^ (2 * (k + 1)) - 2 ^ (3 * (k + 1)) = 25 * 5 ^ (2 * k) - 8 * 2 ^ (3 * k) := by ring_nf _ = 17 * 5 ^ (2 * k) + 8 * (5 ^ (2 * k) - 2 ^ (3 * k)) := by grind rw [h1] -- ⊢ 17 ∣ 17 * 5 ^ (2 * k) + 8 * (5 ^ (2 * k) - 2 ^ (3 * k)) exact dvd_add (dvd_mul_right 17 _) (dvd_mul_of_dvd_right ih 8) end Demostracion9 -- 10ª demostración -- ================ namespace Demostracion10 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 Demostracion10 -- Lemas usados -- ============ 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)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.