English
Let b > 1 and y ≠ 0. Then for all x, x ≤ log_b y iff b^x ≤ y.
Русский
Пусть b > 1 и y ≠ 0. Тогда для всех x: x ≤ log_b y эквивално b^x ≤ y.
LaTeX
$$$\\forall b \\in \\mathbb{N}, \\; 1 < b \\land y \\in \\mathbb{N}, y \\neq 0 \\Rightarrow \\forall x \\in \\mathbb{N}: \\; x \\le \\log_b y \\iff \\; b^x \\le y$$$
Lean4
/-- `pow b` and `log b` (almost) form a Galois connection. See also `Nat.pow_le_of_le_log` and
`Nat.le_log_of_pow_le` for individual implications under weaker assumptions. -/
theorem le_log_iff_pow_le {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : y ≠ 0) : x ≤ log b y ↔ b ^ x ≤ y :=
by
induction y using Nat.strong_induction_on generalizing x with
| h y ih => ?_
cases x with
| zero => dsimp; cutsat
| succ x =>
rw [log]; split_ifs with h
· have b_pos : 0 < b := lt_of_succ_lt hb
rw [Nat.add_le_add_iff_right, ih (y / b) (div_lt_self (Nat.pos_iff_ne_zero.2 hy) hb) (Nat.div_pos h.1 b_pos).ne',
le_div_iff_mul_le b_pos, pow_succ', Nat.mul_comm]
· exact iff_of_false (not_succ_le_zero _) (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩)
