English
If x ≥ 1 and y > 1 in a suitable Archimedean ordered setting, there exists n ∈ ℕ such that y^n ≤ x < y^{n+1}. In other words, x lies between two consecutive natural powers of y.
Русский
Если x ≥ 1 и y > 1 в подходящей архимедовой упорядоченной системе, существует n ∈ ℕ такое, что y^n ≤ x < y^{n+1}. То есть x лежит между двумя последовательными степенями y.
LaTeX
$$$\\exists n \\in \\mathbb{N},\, y^n \\le x \\wedge x < y^{n+1}$$$
Lean4
/-- Every x greater than or equal to 1 is between two successive
natural-number powers of every y greater than one. -/
theorem exists_nat_pow_near (hx : 1 ≤ x) (hy : 1 < y) : ∃ n : ℕ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
by
have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy
classical
exact
let n := Nat.find h
have hn : x < y ^ n := Nat.find_spec h
have hnp : 0 < n := pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
⟨Nat.pred n, le_of_not_gt (Nat.find_min h hltn), by rwa [hnsp]⟩
