English
For a>1 in a commutative group with order and Archimedean property, there exists a unique integer k such that a^k ≤ g < a^{k+1}.
Русский
Для a>1 в коммутативной группе с порядком и Архимедовым свойством существует единственный целочисленный показатель k, такой что a^k ≤ g < a^{k+1}.
LaTeX
$$$\\forall a>1\\;\\forall g:\\, G\\;\\exists! k\\in \\mathbb{Z},\\ a^{k} \\le g < a^{k+1}. $$$
Lean4
theorem add_one_pow_unbounded_of_pos (x : R) (hy : 0 < y) : ∃ n : ℕ, x < (y + 1) ^ n :=
have : 0 ≤ 1 + y := add_nonneg zero_le_one hy.le
(Archimedean.arch x hy).imp fun n h ↦
calc
x ≤ n • y := h
_ = n * y := (nsmul_eq_mul _ _)
_ < 1 + n * y := (lt_one_add _)
_ ≤ (1 + y) ^ n :=
(one_add_mul_le_pow' (mul_nonneg hy.le hy.le) (mul_nonneg this this) (add_nonneg zero_le_two hy.le) _)
_ = (y + 1) ^ n := by rw [add_comm]
