no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
classical exact
    let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    have he : ∃ m : ℤ, y ^ m ≤ x :=
      ⟨-N,
        le_of_lt
          (by
            rw [zpow_neg y ↑N, zpow_ofNat]
            exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
    let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
      ⟨M, fun m hm =>
        le_of_not_lt fun hlt =>
          not_lt_of_ge (zpow_le_of_le hy.le hlt.le)
            (lt_of_le_of_lt hm (by rwa [← zpow_ofNat] at hM))⟩
    let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
    ⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
exact
let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
have he : ∃ m : ℤ, y ^ m ≤ x :=
⟨-N,
le_of_lt
(by
  rw [zpow_neg y ↑N, zpow_ofNat]
  exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
⟨M, fun m hm =>
le_of_not_lt fun hlt =>
not_lt_of_ge (zpow_le_of_le hy.le hlt.le)
  (lt_of_le_of_lt hm (by rwa [← zpow_ofNat] at hM))⟩
let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ < x
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ y ^ (-↑N) < x
rw [zpow_neg y ↑N, zpow_ofNat]
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ < x
exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
he : ∃ m, y ^ m ≤ x
M : ℕ
hM : x < y ^ M
m : ℤ
hm : y ^ m ≤ x
hlt : ↑M < m
⊢ x < y ^ ↑M
rwa [← zpow_ofNat] at hM