English
If p−1 divides x−y and y≤x with y>0, then n^x ≡ n^y (mod p) for all integers n, given p prime.
Русский
Если p−1 делит x−y и y≤x, y>0, то для всех целых n получаем n^x ≡ n^y (mod p) при простом p.
LaTeX
$$$\\\\forall p,x,y \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\wedge (p-1) \\\\mid (x-y) \\\\wedge y \\\\le x \\\\wedge 0 < y \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{Z}, n^{x} \\\\equiv n^{y} \\\\pmod p$$$
Lean4
theorem pow_eq_pow {p x y : ℕ} (hp : Nat.Prime p) (h : p - 1 ∣ x - y) (hxy : y ≤ x) (hy : 0 < y) (n : ℤ) :
n ^ x ≡ n ^ y [ZMOD p] := by
rw [← Nat.mul_div_eq_iff_dvd] at h
by_cases hn : n ≡ 0 [ZMOD p]
· grw [hn, zero_pow (hy.trans_le hxy).ne', zero_pow hy.ne']
· rw [Int.modEq_zero_iff_dvd, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at hn
grw [← pow_sub_mul_pow n hxy, ← h, pow_mul, Int.ModEq.pow_card_sub_one_eq_one hp hn.symm, one_pow, one_mul]
