English
For natural a,b,c, the congruence (a^c − 1) ≡ (a^{c mod b} − 1) mod (a^b − 1) holds; hence (a^c − 1) mod (a^b − 1) = a^{c mod b} − 1.
Русский
Для натуральных a,b,c выполняется равенство (a^c − 1) ≡ (a^{c mod b} − 1) mod (a^b − 1); следовательно (a^c − 1) mod (a^b − 1) = a^{c mod b} − 1.
LaTeX
$$$ (a^c - 1) \bmod (a^b - 1) = a^{(c \bmod b)} - 1. $$$
Lean4
@[simp]
theorem pow_sub_one_mod_pow_sub_one (a b c : ℕ) : (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1 :=
by
rcases eq_zero_or_pos a with rfl | ha0
· simp [zero_pow_eq]; split_ifs <;> simp
rcases Nat.eq_or_lt_of_le ha0 with rfl | ha1
· simp
rcases eq_zero_or_pos b with rfl | hb0
· simp
rcases lt_or_ge c b with h | h
· rw [mod_eq_of_lt, mod_eq_of_lt h]
rwa [Nat.sub_lt_sub_iff_right (one_le_pow c a ha0), Nat.pow_lt_pow_iff_right ha1]
· suffices a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1) by
rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self, mul_zero, zero_mod, zero_add,
mod_mod, pow_sub_one_mod_pow_sub_one]
rw [← Nat.add_sub_assoc (one_le_pow (c - b) a ha0), ← mul_add_one, pow_add, Nat.sub_add_cancel (one_le_pow b a ha0)]
