English
For x>0, y>1 and ExistsAddOfLE, there exists n ∈ ℤ with x ∈ Ioc(y^n, y^{n+1}).
Русский
Для x > 0, y > 1 и ExistsAddOfLE существует n ∈ ℤ такое, что x ∈ Ioc(y^n, y^{n+1}).
LaTeX
$$$\\exists n ∈ \\mathbb{Z},\\ x ∈ Ioc (y^n) (y^{n+1})$$$
Lean4
/-- Every positive `x` is between two successive integer powers of
another `y` greater than one. This is the same as `exists_mem_Ico_zpow`,
but with ≤ and < the other way around. -/
theorem exists_mem_Ioc_zpow (hx : 0 < x) (hy : 1 < y) : ∃ n : ℤ, x ∈ Ioc (y ^ n) (y ^ (n + 1)) :=
let ⟨m, hle, hlt⟩ := exists_mem_Ico_zpow (inv_pos.2 hx) hy
have hyp : 0 < y := lt_trans zero_lt_one hy
⟨-(m + 1), by rwa [zpow_neg, inv_lt_comm₀ (zpow_pos hyp _) hx], by
rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv_comm₀ hx (zpow_pos hyp _)]⟩
