le_log_of_pow_le — Mathlib

English

If 1 < b and y ≠ 0, then b^x ≤ y implies x ≤ log_b y.

Русский

Если 1 < b и y ≠ 0, то b^x ≤ y ⇒ x ≤ log_b y.

LaTeX

$$$\\forall b \\in \\mathbb{N}, \\; 1 < b \\land y \\neq 0 \\Rightarrow (b^x \\le y) \\Rightarrow x \\le \\log_b y$$$

Lean4

theorem le_log_of_pow_le {b x y : ℕ} (hb : 1 < b) (h : b ^ x ≤ y) : x ≤ log b y :=
  by
  rcases ne_or_eq y 0 with (hy | rfl)
  exacts [(le_log_iff_pow_le hb hy).2 h, (h.not_gt (Nat.pow_pos (Nat.zero_lt_one.trans hb))).elim]

Похожие утверждения