English
For any base b > 1 and any integer z, log_b(b^z) = z.
Русский
Для основания b > 1 и любого целого z выполняется log_b(b^z) = z.
LaTeX
$$$\log_b\bigl(b^z\bigr) = z$$$
Lean4
theorem log_zpow {b : ℕ} (hb : 1 < b) (z : ℤ) : log b (b ^ z : R) = z :=
by
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
·
rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast, ← Nat.cast_pow,
Nat.floor_natCast, Nat.log_pow hb]
·
rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <| neg_nonpos.2 (Int.natCast_nonneg _)),
zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
