pow_le_of_le_log — Mathlib

English

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

Русский

Пусть y ≠ 0 и x ≤ log_b y, тогда b^x ≤ y.

LaTeX

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

Lean4

theorem pow_le_of_le_log {b x y : ℕ} (hy : y ≠ 0) (h : x ≤ log b y) : b ^ x ≤ y :=
  by
  refine (le_or_gt b 1).elim (fun hb => ?_) fun hb => (le_log_iff_pow_le hb hy).1 h
  rw [log_of_left_le_one hb, Nat.le_zero] at h
  rwa [h, Nat.pow_zero, one_le_iff_ne_zero]

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