English
Let b, m, n be natural numbers with m ≠ 0 or (1 < b and n ≠ 0). Then log_b n = m iff b^m ≤ n < b^(m+1).
Русский
Пусть b, m, n натуральны; при условии m ≠ 0 или (1 < b и n ≠ 0) лог_b n = m эквивално b^m ≤ n < b^(m+1).
LaTeX
$$$\\forall {b,m,n} \\in \\mathbb{N}, \\; (m \\neq 0 \\lor \\ (1 < b \\land n \\neq 0)) \\Rightarrow \\log_b n = m \\iff b^m \le n \\land n < b^{m+1}$$$
Lean4
theorem log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) : log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1) :=
by
rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
· rw [le_antisymm_iff, ← Nat.lt_succ_iff, le_log_iff_pow_le, log_lt_iff_lt_pow, and_comm] <;> assumption
have hm : m ≠ 0 := h.resolve_right hbn
rw [not_and_or, not_lt, Ne, not_not] at hbn
rcases hbn with (hb | rfl)
· obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb
any_goals
simp only [ne_eq, lt_self_iff_false, not_lt_zero, false_and, or_false] at h
simp [h, eq_comm (a := 0), Nat.zero_pow (Nat.pos_iff_ne_zero.2 _)] <;> omega
· simp [@eq_comm _ 0, hm]
