1. Analysis
  2. 6.7. Real exponentiation, part II
Imports
import Mathlib.Tactic import Analysis.Section_5_epilogue import Analysis.Section_6_6

Analysis I, Section 6.7: Real exponentiation, part II

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

  • Real exponentiation.

Because the Chapter 5 reals have been deprecated in favor of the Mathlib reals, and Mathlib real exponentiation is defined without first going through rational exponentiation, we will adopt a somewhat awkward compromise, in that we will initially accept the Mathlib exponentiation operation (with all its API) when the exponent is a rational, and use this to define a notion of real exponentiation which in the epilogue to this chapter we will show is identical to the Mathlib operation.

namespace Chapter6open Sequence Real

Lemma 6.7.1 (Continuity of exponentiation)

lemma declaration uses `sorry`ratPow_continuous {x α:ℝ} (hx: x > 0) {q: ℕ → ℚ} (hq: ((fun n ↦ (q n:ℝ)):Sequence).TendsTo α) : ((fun n ↦ x^(q n:ℝ)):Sequence).Convergent := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo α⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent -- This proof is rearranged slightly from the original text. x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy M⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:x < 1⊢ (↑fun n ↦ x ^ ↑(q n)).Convergentα:ℝq:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mhx:1 > 0⊢ (↑fun n ↦ 1 ^ ↑(q n)).Convergentx:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < x⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:x < 1⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent All goals completed! 🐙 α:ℝq:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mhx:1 > 0⊢ (↑fun n ↦ 1 ^ ↑(q n)).Convergent α:ℝq:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mhx:1 > 0⊢ (↑fun n ↦ 1).Convergent; All goals completed! 🐙 have h': 1 ≤ x := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo α⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent All goals completed! 🐙 x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ x⊢ (↑fun n ↦ x ^ ↑(q n)).IsCauchy intro ε x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0⊢ ε.EventuallySteady ↑fun n ↦ x ^ ↑(q n) choose K hK hclose using lim_of_roots hx (ε*x^(-M)) (x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0⊢ ε * x ^ (-M) > 0 All goals completed! 🐙) choose N hN hq using IsCauchy.convergent ⟨ α, hq ⟩ (1/(K+1:ℝ)) (x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0K:ℤhK:K ≥ (↑fun n ↦ x ^ (1 / (↑n + 1))).mhclose:(ε * x ^ (-M)).CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from K) 1⊢ 1 / (↑K + 1) > 0 All goals completed! 🐙) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0K:ℤN:ℤhq:(1 / (↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from N)hclose:∀ (n : ℤ), 0 ≤ n → K ≤ n → |(if 0 ≤ n ∧ K ≤ n then if 0 ≤ n then x ^ (↑n.toNat + 1)⁻¹ else 0 else 0) - 1| ≤ ε * x ^ (-M)hK:0 ≤ KhN:0 ≤ N⊢ ε.EventuallySteady ↑fun n ↦ x ^ ↑(q n) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0K:ℤhclose:∀ (n : ℤ), 0 ≤ n → K ≤ n → |(if 0 ≤ n ∧ K ≤ n then if 0 ≤ n then x ^ (↑n.toNat + 1)⁻¹ else 0 else 0) - 1| ≤ ε * x ^ (-M)hK:0 ≤ KN:ℕhq:(1 / (↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)⊢ ε.EventuallySteady ↑fun n ↦ x ^ ↑(q n) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:∀ (n : ℤ), 0 ≤ n → ↑K ≤ n → |(if 0 ≤ n ∧ ↑K ≤ n then if 0 ≤ n then x ^ (↑n.toNat + 1)⁻¹ else 0 else 0) - 1| ≤ ε * x ^ (-M)hq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)⊢ ε.EventuallySteady ↑fun n ↦ x ^ ↑(q n) specialize hclose K (x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:∀ (n : ℤ), 0 ≤ n → ↑K ≤ n → |(if 0 ≤ n ∧ ↑K ≤ n then if 0 ≤ n then x ^ (↑n.toNat + 1)⁻¹ else 0 else 0) - 1| ≤ ε * x ^ (-M)hq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)⊢ 0 ≤ ↑K All goals completed! 🐙) (x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:∀ (n : ℤ), 0 ≤ n → ↑K ≤ n → |(if 0 ≤ n ∧ ↑K ≤ n then if 0 ≤ n then x ^ (↑n.toNat + 1)⁻¹ else 0 else 0) - 1| ≤ ε * x ^ (-M)hq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)⊢ ↑K ≤ ↑K All goals completed! 🐙); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)hclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)⊢ ε.EventuallySteady ↑fun n ↦ x ^ ↑(q n) use N, x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)hclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)⊢ ↑N ≥ (↑fun n ↦ x ^ ↑(q n)).m All goals completed! 🐙 intro n x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)hclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℤhn:n ≥ ((↑fun n ↦ x ^ ↑(q n)).from ↑N).m⊢ ∀ m ≥ ((↑fun n ↦ x ^ ↑(q n)).from ↑N).m, ε.Close (((↑fun n ↦ x ^ ↑(q n)).from ↑N).seq n) (((↑fun n ↦ x ^ ↑(q n)).from ↑N).seq m) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)hclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℤhn:n ≥ ((↑fun n ↦ x ^ ↑(q n)).from ↑N).mm:ℤ⊢ m ≥ ((↑fun n ↦ x ^ ↑(q n)).from ↑N).m → ε.Close (((↑fun n ↦ x ^ ↑(q n)).from ↑N).seq n) (((↑fun n ↦ x ^ ↑(q n)).from ↑N).seq m) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)hclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℤhn:n ≥ ((↑fun n ↦ x ^ ↑(q n)).from ↑N).mm:ℤhm:m ≥ ((↑fun n ↦ x ^ ↑(q n)).from ↑N).m⊢ ε.Close (((↑fun n ↦ x ^ ↑(q n)).from ↑N).seq n) (((↑fun n ↦ x ^ ↑(q n)).from ↑N).seq m); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)hclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ ε.Close (((↑fun n ↦ x ^ ↑(q n)).from ↑N).seq n) (((↑fun n ↦ x ^ ↑(q n)).from ↑N).seq m) specialize hq n (x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)hclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ n ≥ ((↑fun n ↦ ↑(q n)).from ↑N).m All goals completed! 🐙) m (x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhq:(1 / (↑↑K + 1)).Steady ((↑fun n ↦ ↑(q n)).from ↑N)hclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ m ≥ ((↑fun n ↦ ↑(q n)).from ↑N).m All goals completed! 🐙) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mhq:|(if 0 ≤ n then ↑(q n.toNat) else 0) - if 0 ≤ m then ↑(q m.toNat) else 0| ≤ (↑K + 1)⁻¹⊢ |(if 0 ≤ n then x ^ ↑(q n.toNat) else 0) - if 0 ≤ m then x ^ ↑(q m.toNat) else 0| ≤ ε have : 0 ≤ (N:ℤ) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo α⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent All goals completed! 🐙 lift n to ℕ using x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mhq:|(if 0 ≤ n then ↑(q n.toNat) else 0) - if 0 ≤ m then ↑(q m.toNat) else 0| ≤ (↑K + 1)⁻¹this:0 ≤ ↑N⊢ 0 ≤ n All goals completed! 🐙 lift m to ℕ using x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)m:ℤhm:↑N ≤ mthis:0 ≤ ↑Nn:ℕhn:↑N ≤ ↑nhq:|(if 0 ≤ ↑n then ↑(q (↑n).toNat) else 0) - if 0 ≤ m then ↑(q m.toNat) else 0| ≤ (↑K + 1)⁻¹⊢ 0 ≤ m All goals completed! 🐙 x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)this:0 ≤ ↑Nn:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹⊢ |x ^ ↑(q n) - x ^ ↑(q m)| ≤ ε x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)this:0 ≤ ↑Nn:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q n⊢ |x ^ ↑(q n) - x ^ ↑(q m)| ≤ εx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)this:0 ≤ ↑Nn:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q m⊢ |x ^ ↑(q n) - x ^ ↑(q m)| ≤ ε x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)this:0 ≤ ↑Nn:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q n⊢ |x ^ ↑(q n) - x ^ ↑(q m)| ≤ ε replace : x^(q m:ℝ) ≤ x^(q n:ℝ) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo α⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)this:0 ≤ ↑Nn:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q n⊢ ↑(q m) ≤ ↑(q n); All goals completed! 🐙 x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ x ^ ↑(q n) - x ^ ↑(q m) ≤ ε calc _ = x^(q m:ℝ) * (x^(q n - q m:ℝ) - 1) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ x ^ ↑(q n) - x ^ ↑(q m) = x ^ ↑(q m) * (x ^ (↑(q n) - ↑(q m)) - 1) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ x ^ ↑(q n) - x ^ ↑(q m) = -x ^ ↑(q m) + x ^ ↑(q m) * x ^ (↑(q n) - ↑(q m)); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ x ^ ↑(q n) - x ^ ↑(q m) = -x ^ ↑(q m) + x ^ (↑(q m) + (↑(q n) - ↑(q m))); All goals completed! 🐙 _ ≤ x^M * (x^(1/(K+1:ℝ)) - 1) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ x ^ ↑(q m) * (x ^ (↑(q n) - ↑(q m)) - 1) ≤ x ^ M * (x ^ (1 / (↑K + 1)) - 1) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 0 ≤ x ^ (↑(q n) - ↑(q m)) - 1x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ ↑(q m) ≤ Mx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ ↑(q n) - ↑(q m) ≤ 1 / (↑K + 1) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 0 ≤ x ^ (↑(q n) - ↑(q m)) - 1x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ ↑(q m) ≤ Mx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ ↑(q n) - ↑(q m) ≤ 1 / (↑K + 1) try x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ ↑(q n) - ↑(q m) ≤ 1 / (↑K + 1) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 0 ≤ x ^ (↑(q n) - ↑(q m)) - 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 1 ≤ x ^ (↑(q n) - ↑(q m)); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 0 ≤ ↑(q n) - ↑(q m); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 0 ≤ q n - q m; All goals completed! 🐙 x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ ↑(q m) ≤ M x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0h:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)hbound:|(↑fun n ↦ ↑(q n)).seq ↑m| ≤ M⊢ ↑(q m) ≤ M; All goals completed! 🐙 All goals completed! 🐙 _ ≤ x^M * (ε * x^(-M)) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ x ^ M * (x ^ (1 / (↑K + 1)) - 1) ≤ x ^ M * (ε * x ^ (-M)) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ x ^ (1 / (↑K + 1)) - 1 ≤ ε * x ^ (-M); All goals completed! 🐙 _ = ε := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ x ^ M * (ε * x ^ (-M)) = ε x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ ε * x ^ (-M + M) = εx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 0 < x; x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q m ≤ q nthis:x ^ ↑(q m) ≤ x ^ ↑(q n)⊢ 0 < x; All goals completed! 🐙 replace : x^(q n:ℝ) ≤ x^(q m:ℝ) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo α⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)this:0 ≤ ↑Nn:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q m⊢ ↑(q n) ≤ ↑(q m); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)this:0 ≤ ↑Nn:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q m⊢ q n ≤ q m; All goals completed! 🐙 x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ -(x ^ ↑(q n) - x ^ ↑(q m)) ≤ ε calc _ = x^(q n:ℝ) * (x^(q m - q n:ℝ) - 1) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ -(x ^ ↑(q n) - x ^ ↑(q m)) = x ^ ↑(q n) * (x ^ (↑(q m) - ↑(q n)) - 1) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ -x ^ ↑(q n) + x ^ ↑(q m) = -x ^ ↑(q n) + x ^ ↑(q n) * x ^ (↑(q m) - ↑(q n)); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ -x ^ ↑(q n) + x ^ ↑(q m) = -x ^ ↑(q n) + x ^ (↑(q n) + (↑(q m) - ↑(q n)))x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 < x; x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 < x; All goals completed! 🐙 _ ≤ x^M * (x^(1/(K+1:ℝ)) - 1) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ x ^ ↑(q n) * (x ^ (↑(q m) - ↑(q n)) - 1) ≤ x ^ M * (x ^ (1 / (↑K + 1)) - 1) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 ≤ x ^ (↑(q m) - ↑(q n)) - 1x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ ↑(q n) ≤ Mx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ ↑(q m) - ↑(q n) ≤ 1 / (↑K + 1) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 ≤ x ^ (↑(q m) - ↑(q n)) - 1x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ ↑(q n) ≤ Mx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ ↑(q m) - ↑(q n) ≤ 1 / (↑K + 1) try x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ ↑(q m) - ↑(q n) ≤ 1 / (↑K + 1) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 ≤ x ^ (↑(q m) - ↑(q n)) - 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 1 ≤ x ^ (↑(q m) - ↑(q n)); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 ≤ ↑(q m) - ↑(q n); x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 ≤ q m - q n; All goals completed! 🐙 x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ ↑(q n) ≤ M x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0h:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)hbound:|(↑fun n ↦ ↑(q n)).seq ↑n| ≤ M⊢ ↑(q n) ≤ M; All goals completed! 🐙 All goals completed! 🐙 _ ≤ x^M * (ε * x^(-M)) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ x ^ M * (x ^ (1 / (↑K + 1)) - 1) ≤ x ^ M * (ε * x ^ (-M)) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ x ^ (1 / (↑K + 1)) - 1 ≤ ε * x ^ (-M); All goals completed! 🐙 _ = ε := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ x ^ M * (ε * x ^ (-M)) = ε x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ ε * x ^ (-M + M) = εx:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 < x; x:ℝα:ℝhx:x > 0q:ℕ → ℚhq✝:(↑fun n ↦ ↑(q n)).TendsTo αM:ℝhM:M ≥ 0hbound:(↑fun n ↦ ↑(q n)).BoundedBy Mh:1 < xh':1 ≤ xε:ℝhε:ε > 0N:ℕK:ℕhclose:|x ^ (↑K + 1)⁻¹ - 1| ≤ ε * x ^ (-M)n:ℕm:ℕhn:N ≤ nhm:N ≤ mhq:|↑(q n) - ↑(q m)| ≤ (↑K + 1)⁻¹hqq:q n < q mthis:x ^ ↑(q n) ≤ x ^ ↑(q m)⊢ 0 < x; All goals completed! 🐙
lemma declaration uses `sorry`ratPow_lim_uniq {x α:ℝ} (hx: x > 0) {q q': ℕ → ℚ} (hq: ((fun n ↦ (q n:ℝ)):Sequence).TendsTo α) (hq': ((fun n ↦ (q' n:ℝ)):Sequence).TendsTo α) : lim ((fun n ↦ x^(q n:ℝ)):Sequence) = lim ((fun n ↦ x^(q' n:ℝ)):Sequence) := x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo α⊢ (lim ↑fun n ↦ x ^ ↑(q n)) = lim ↑fun n ↦ x ^ ↑(q' n) -- This proof is written to follow the structure of the original text. x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'⊢ (lim ↑fun n ↦ x ^ ↑(q n)) = lim ↑fun n ↦ x ^ ↑(q' n) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).TendsTo 1⊢ (lim ↑fun n ↦ x ^ ↑(q n)) = lim ↑fun n ↦ x ^ ↑(q' n)x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'⊢ (↑fun n ↦ x ^ ↑(r n)).TendsTo 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).TendsTo 1⊢ (lim ↑fun n ↦ x ^ ↑(q n)) = lim ↑fun n ↦ x ^ ↑(q' n) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).TendsTo 1⊢ (lim ↑fun n ↦ x ^ ↑(q n)) = (lim ↑fun n ↦ x ^ ↑(q' n)) * 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).Convergent ∧ (lim ↑fun n ↦ x ^ ↑(r n)) = 1⊢ (lim ↑fun n ↦ x ^ ↑(q n)) = (lim ↑fun n ↦ x ^ ↑(q' n)) * 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).Convergent ∧ (lim ↑fun n ↦ x ^ ↑(r n)) = 1⊢ (↑fun n ↦ x ^ ↑(q n)) = (↑fun n ↦ x ^ ↑(q' n)) * ↑fun n ↦ x ^ ↑(r n)x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).Convergent ∧ (lim ↑fun n ↦ x ^ ↑(r n)) = 1⊢ 1 = lim ↑fun n ↦ x ^ ↑(r n) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).Convergent ∧ (lim ↑fun n ↦ x ^ ↑(r n)) = 1⊢ (↑fun n ↦ x ^ ↑(q n)) = (↑fun n ↦ x ^ ↑(q' n)) * ↑fun n ↦ x ^ ↑(r n) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).Convergent ∧ (lim ↑fun n ↦ x ^ ↑(r n)) = 1⊢ (↑fun n ↦ x ^ ↑(q n)) = ↑fun n ↦ x ^ ↑(q' n) * x ^ ↑(r n) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).Convergent ∧ (lim ↑fun n ↦ x ^ ↑(r n)) = 1x✝:ℤn:ℕ⊢ x ^ ↑(q n) = x ^ ↑(q' n) * x ^ ↑(r n) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'this:(↑fun n ↦ x ^ ↑(r n)).Convergent ∧ (lim ↑fun n ↦ x ^ ↑(r n)) = 1x✝:ℤn:ℕ⊢ x ^ ↑(q n) = x ^ (↑(q' n) + ↑(r n)) All goals completed! 🐙 All goals completed! 🐙 intro ε x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 have h2 := tendsTo_inv h1 (x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1⊢ 1 ≠ 0 All goals completed! 🐙) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℤhK1:K1 ≥ (↑fun n ↦ x ^ (1 / (↑n + 1))).mh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from K1) 1⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℤhK1:K1 ≥ (↑fun n ↦ x ^ (1 / (↑n + 1))).mh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from K1) 1K2:ℤhK2:K2 ≥ (↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.mh4:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.from K2) 1⁻¹⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℤh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from K1) 1K2:ℤh4:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.from K2) 1⁻¹hK1:0 ≤ K1hK2:0 ≤ K2⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K2:ℤh4:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.from K2) 1⁻¹hK2:0 ≤ K2K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1; x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.from ↑K2) 1⁻¹⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2hr:((↑fun n ↦ ↑(q n)) - ↑fun n ↦ ↑(q' n)).TendsTo (α - α)⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2hr:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)⊢ ε.EventuallyClose (↑fun n ↦ x ^ ↑(r n)) 1 choose N hN hr using hr (1 / (K + 1:ℝ)) (x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2hr:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)⊢ 1 / (↑K + 1) > 0 All goals completed! 🐙) refine ⟨ N, x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mhr:(1 / (↑K + 1)).CloseSeq ((↑fun n ↦ ↑(q n) - ↑(q' n)).from N) (α - α)⊢ N ≥ (↑fun n ↦ x ^ ↑(r n)).m All goals completed! 🐙, ?_ ⟩ intro n x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mhr:(1 / (↑K + 1)).CloseSeq ((↑fun n ↦ ↑(q n) - ↑(q' n)).from N) (α - α)n:ℤhn:n ≥ ((↑fun n ↦ x ^ ↑(r n)).from N).m⊢ ε.Close (((↑fun n ↦ x ^ ↑(r n)).from N).seq n) 1; x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mhr:(1 / (↑K + 1)).CloseSeq ((↑fun n ↦ ↑(q n) - ↑(q' n)).from N) (α - α)n:ℤhn:0 ≤ n ∧ N ≤ n⊢ ε.Close (((↑fun n ↦ x ^ ↑(r n)).from N).seq n) 1 specialize h3 K (x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕh3:ε.CloseSeq ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1) 1K2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mhr:(1 / (↑K + 1)).CloseSeq ((↑fun n ↦ ↑(q n) - ↑(q' n)).from N) (α - α)n:ℤhn:0 ≤ n ∧ N ≤ n⊢ ↑K ≥ ((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1).m All goals completed! 🐙); specialize h4 K (x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕh4:ε.CloseSeq ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2) 1K:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mhr:(1 / (↑K + 1)).CloseSeq ((↑fun n ↦ ↑(q n) - ↑(q' n)).from N) (α - α)n:ℤhn:0 ≤ n ∧ N ≤ nh3:ε.Close (((↑fun n ↦ x ^ (1 / (↑n + 1))).from ↑K1).seq ↑K) 1⊢ ↑K ≥ ((↑fun n ↦ (x ^ (↑n + 1)⁻¹)⁻¹).from ↑K2).m All goals completed! 🐙) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mhr:(1 / (↑K + 1)).CloseSeq ((↑fun n ↦ ↑(q n) - ↑(q' n)).from N) (α - α)n:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹⊢ x ^ ↑(r n.toNat) ≤ ε + 1 ∧ 1 ≤ ε + x ^ ↑(r n.toNat) specialize hr n (x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mhr:(1 / (↑K + 1)).CloseSeq ((↑fun n ↦ ↑(q n) - ↑(q' n)).from N) (α - α)n:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹⊢ n ≥ ((↑fun n ↦ ↑(q n) - ↑(q' n)).from N).m All goals completed! 🐙) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)⊢ x ^ ↑(r n.toNat) ≤ ε + 1 ∧ 1 ≤ ε + x ^ ↑(r n.toNat) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:x < 1⊢ x ^ ↑(r n.toNat) ≤ ε + 1 ∧ 1 ≤ ε + x ^ ↑(r n.toNat)α:ℝq:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nhr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)hx:1 > 0h1:(↑fun n ↦ 1 ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ 1 ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹h3:1 ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + 1 ^ (↑(max K1 K2) + 1)⁻¹h4:(1 ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (1 ^ (↑(max K1 K2) + 1)⁻¹)⁻¹⊢ 1 ^ ↑(r n.toNat) ≤ ε + 1 ∧ 1 ≤ ε + 1 ^ ↑(r n.toNat)x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < x⊢ x ^ ↑(r n.toNat) ≤ ε + 1 ∧ 1 ≤ ε + x ^ ↑(r n.toNat) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:x < 1⊢ x ^ ↑(r n.toNat) ≤ ε + 1 ∧ 1 ≤ ε + x ^ ↑(r n.toNat) All goals completed! 🐙 α:ℝq:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nhr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)hx:1 > 0h1:(↑fun n ↦ 1 ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ 1 ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹h3:1 ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + 1 ^ (↑(max K1 K2) + 1)⁻¹h4:(1 ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (1 ^ (↑(max K1 K2) + 1)⁻¹)⁻¹⊢ 1 ^ ↑(r n.toNat) ≤ ε + 1 ∧ 1 ≤ ε + 1 ^ ↑(r n.toNat) α:ℝq:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nhr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)hx:1 > 0h1:(↑fun n ↦ 1 ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ 1 ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹h3:1 ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + 1 ^ (↑(max K1 K2) + 1)⁻¹h4:(1 ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (1 ^ (↑(max K1 K2) + 1)⁻¹)⁻¹⊢ 0 ≤ ε; All goals completed! 🐙 have h5 : x ^ (r n.toNat:ℝ) ≤ x^(K + 1:ℝ)⁻¹ := x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo α⊢ (lim ↑fun n ↦ x ^ ↑(q n)) = lim ↑fun n ↦ x ^ ↑(q' n) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < x⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < x⊢ ↑(r n.toNat) ≤ (↑K + 1)⁻¹; x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < x⊢ ↑(r n.toNat) ≤ (↑K + 1)⁻¹; All goals completed! 🐙 have h6 : (x^(K + 1:ℝ)⁻¹)⁻¹ ≤ x ^ (r n.toNat:ℝ) := x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo α⊢ (lim ↑fun n ↦ x ^ ↑(q n)) = lim ↑fun n ↦ x ^ ↑(q' n) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹⊢ x ^ (-(↑K + 1)⁻¹) ≤ x ^ ↑(r n.toNat) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹⊢ 1 ≤ xx:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹⊢ -(↑K + 1)⁻¹ ≤ ↑(r n.toNat); x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹⊢ -(↑K + 1)⁻¹ ≤ ↑(r n.toNat) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹⊢ ↑(q' n.toNat) ≤ ↑(q n.toNat) + (↑K + 1)⁻¹; All goals completed! 🐙 x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹h6:(x ^ (↑K + 1)⁻¹)⁻¹ ≤ x ^ ↑(r n.toNat)⊢ x ^ ↑(r n.toNat) ≤ ε + 1x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹h6:(x ^ (↑K + 1)⁻¹)⁻¹ ≤ x ^ ↑(r n.toNat)⊢ 1 ≤ ε + x ^ ↑(r n.toNat) x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹h6:(x ^ (↑K + 1)⁻¹)⁻¹ ≤ x ^ ↑(r n.toNat)⊢ x ^ ↑(r n.toNat) ≤ ε + 1x:ℝα:ℝhx:x > 0q:ℕ → ℚq':ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo αhq':(↑fun n ↦ ↑(q' n)).TendsTo αr:ℕ → ℚ := q - q'ε:ℝhε:ε > 0h1:(↑fun n ↦ x ^ (1 / (↑n + 1))).TendsTo 1h2:(↑fun n ↦ x ^ (1 / (↑n + 1)))⁻¹.TendsTo 1⁻¹K1:ℕK2:ℕK:ℕ := max K1 K2hr✝:(↑fun n ↦ ↑(q n) - ↑(q' n)).TendsTo (α - α)N:ℤhN:N ≥ (↑fun n ↦ ↑(q n) - ↑(q' n)).mn:ℤhn:0 ≤ n ∧ N ≤ nh3:x ^ (↑(max K1 K2) + 1)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + x ^ (↑(max K1 K2) + 1)⁻¹h4:(x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹ ≤ ε + 1 ∧ 1 ≤ ε + (x ^ (↑(max K1 K2) + 1)⁻¹)⁻¹hr:↑(q n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q' n.toNat) ∧ ↑(q' n.toNat) ≤ (↑K + 1)⁻¹ + ↑(q n.toNat)h:1 < xh5:x ^ ↑(r n.toNat) ≤ x ^ (↑K + 1)⁻¹h6:(x ^ (↑K + 1)⁻¹)⁻¹ ≤ x ^ ↑(r n.toNat)⊢ 1 ≤ ε + x ^ ↑(r n.toNat) All goals completed! 🐙theorem Real.eq_lim_of_rat (α:ℝ) : ∃ q: ℕ → ℚ, ((fun n ↦ (q n:ℝ)):Sequence).TendsTo α := α:ℝ⊢ ∃ q, (↑fun n ↦ ↑(q n)).TendsTo α α:ℝq:ℕ → ℚhcauchy:(↑q).IsCauchyhLIM:Chapter5.Real.equivR.symm α = Chapter5.LIM q⊢ ∃ q, (↑fun n ↦ ↑(q n)).TendsTo α; α:ℝq:ℕ → ℚhcauchy:(↑q).IsCauchyhLIM:Chapter5.Real.equivR.symm α = Chapter5.LIM q⊢ (↑fun n ↦ ↑(q n)).TendsTo α α:ℝq:ℕ → ℚhLIM:Chapter5.Real.equivR.symm α = Chapter5.LIM qhcauchy:(↑↑q).TendsTo (Chapter5.Real.equivR (Chapter5.LIM q))⊢ (↑fun n ↦ ↑(q n)).TendsTo α α:ℝq:ℕ → ℚhLIM:Chapter5.Real.equivR.symm α = Chapter5.LIM qhcauchy:(↑↑q).TendsTo α⊢ (↑fun n ↦ ↑(q n)).TendsTo α α:ℝq:ℕ → ℚhLIM:Chapter5.Real.equivR.symm α = Chapter5.LIM qhcauchy:(↑↑q).TendsTo α⊢ (↑fun n ↦ ↑(q n)) = ↑↑q; All goals completed! 🐙

Definition 6.7.2 (Exponentiation to a real exponent)

noncomputable abbrev Real.rpow (x:ℝ) (α:ℝ) :ℝ := lim ((fun n ↦ x^((eq_lim_of_rat α).choose n:ℝ)):Sequence)
lemma Real.rpow_eq_lim_ratPow {x α:ℝ} (hx: x > 0) {q: ℕ → ℚ} (hq: ((fun n ↦ (q n:ℝ)):Sequence).TendsTo α) : rpow x α = lim ((fun n ↦ x^(q n:ℝ)):Sequence) := ratPow_lim_uniq hx (eq_lim_of_rat α).choose_spec hqlemma Real.ratPow_tendsto_rpow {x α:ℝ} (hx: x > 0) {q: ℕ → ℚ} (hq: ((fun n ↦ (q n:ℝ)):Sequence).TendsTo α) : ((fun n ↦ x^(q n:ℝ)):Sequence).TendsTo (rpow x α) := x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo α⊢ (↑fun n ↦ x ^ ↑(q n)).TendsTo (rpow x α) x:ℝα:ℝhx:x > 0q:ℕ → ℚhq:(↑fun n ↦ ↑(q n)).TendsTo α⊢ (↑fun n ↦ x ^ ↑(q n)).Convergent ∧ (lim ↑fun n ↦ x ^ ↑(q n)) = rpow x α All goals completed! 🐙lemma Real.rpow_of_rat_eq_ratPow {x:ℝ} (hx: x > 0) {q: ℚ} : rpow x (q:ℝ) = x^(q:ℝ) := x:ℝhx:x > 0q:ℚ⊢ rpow x ↑q = x ^ ↑q x:ℝhx:x > 0q:ℚ⊢ x ^ ↑q = lim ↑fun n ↦ x ^ ↑q All goals completed! 🐙

Proposition 6.7.3(a) / Exercise 6.7.1

theorem declaration uses `sorry`Real.ratPow_nonneg {x:ℝ} (hx: x > 0) (q:ℝ) : rpow x q ≥ 0 := x:ℝhx:x > 0q:ℝ⊢ rpow x q ≥ 0 All goals completed! 🐙

Proposition 6.7.3(b)

theorem Real.ratPow_add {x:ℝ} (hx: x > 0) (q r:ℝ) : rpow x (q+r) = rpow x q * rpow x r := x:ℝhx:x > 0q:ℝr:ℝ⊢ rpow x (q + r) = rpow x q * rpow x r x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo q⊢ rpow x (q + r) = rpow x q * rpow x r x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo r⊢ rpow x (q + r) = rpow x q * rpow x r x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':((↑fun n ↦ ↑(q' n)) + ↑fun n ↦ ↑(r' n)).TendsTo (q + r)⊢ rpow x (q + r) = rpow x q * rpow x r x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n) + ↑(r' n)).TendsTo (q + r)⊢ rpow x (q + r) = rpow x q * rpow x r x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n) + ↑(r' n)).TendsTo (q + r)⊢ (↑fun n ↦ ↑(q' n) + ↑(r' n)) = ↑fun n ↦ ↑(q' n + r' n)x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n + r' n)).TendsTo (q + r)⊢ rpow x (q + r) = rpow x q * rpow x r x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n) + ↑(r' n)).TendsTo (q + r)⊢ (↑fun n ↦ ↑(q' n) + ↑(r' n)) = ↑fun n ↦ ↑(q' n + r' n) All goals completed! 🐙 x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n + r' n)).TendsTo (q + r)h1:(↑fun n ↦ x ^ ↑(q' n)).Convergent⊢ rpow x (q + r) = rpow x q * rpow x r x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n + r' n)).TendsTo (q + r)h1:(↑fun n ↦ x ^ ↑(q' n)).Convergenth2:(↑fun n ↦ x ^ ↑(r' n)).Convergent⊢ rpow x (q + r) = rpow x q * rpow x r x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n + r' n)).TendsTo (q + r)h1:(↑fun n ↦ x ^ ↑(q' n)).Convergenth2:(↑fun n ↦ x ^ ↑(r' n)).Convergent⊢ (lim ↑fun n ↦ x ^ ↑(q' n + r' n)) = lim ↑fun n ↦ x ^ ↑(q' n) * x ^ ↑(r' n) x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n + r' n)).TendsTo (q + r)h1:(↑fun n ↦ x ^ ↑(q' n)).Convergenth2:(↑fun n ↦ x ^ ↑(r' n)).Convergentn:ℕ⊢ x ^ ↑(q' n + r' n) = x ^ ↑(q' n) * x ^ ↑(r' n); x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n + r' n)).TendsTo (q + r)h1:(↑fun n ↦ x ^ ↑(q' n)).Convergenth2:(↑fun n ↦ x ^ ↑(r' n)).Convergentn:ℕ⊢ x ^ ↑(q' n + r' n) = x ^ (↑(q' n) + ↑(r' n))x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n + r' n)).TendsTo (q + r)h1:(↑fun n ↦ x ^ ↑(q' n)).Convergenth2:(↑fun n ↦ x ^ ↑(r' n)).Convergentn:ℕ⊢ 0 < x; x:ℝhx:x > 0q:ℝr:ℝq':ℕ → ℚhq':(↑fun n ↦ ↑(q' n)).TendsTo qr':ℕ → ℚhr':(↑fun n ↦ ↑(r' n)).TendsTo rhq'r':(↑fun n ↦ ↑(q' n + r' n)).TendsTo (q + r)h1:(↑fun n ↦ x ^ ↑(q' n)).Convergenth2:(↑fun n ↦ x ^ ↑(r' n)).Convergentn:ℕ⊢ 0 < x; All goals completed! 🐙

Proposition 6.7.3(b) / Exercise 6.7.1

theorem declaration uses `sorry`Real.ratPow_ratPow {x:ℝ} (hx: x > 0) (q r:ℝ) : rpow (rpow x q) r = rpow x (q*r) := x:ℝhx:x > 0q:ℝr:ℝ⊢ rpow (rpow x q) r = rpow x (q * r) All goals completed! 🐙

Proposition 6.7.3(c) / Exercise 6.7.1

theorem declaration uses `sorry`Real.ratPow_neg {x:ℝ} (hx: x > 0) (q:ℝ) : rpow x (-q) = 1 / rpow x q := x:ℝhx:x > 0q:ℝ⊢ rpow x (-q) = 1 / rpow x q All goals completed! 🐙

Proposition 6.7.3(d) / Exercise 6.7.1

theorem declaration uses `sorry`Real.ratPow_mono {x y:ℝ} (hx: x > 0) (hy: y > 0) {q:ℝ} (h: q > 0) : x > y ↔ rpow x q > rpow y q := x:ℝy:ℝhx:x > 0hy:y > 0q:ℝh:q > 0⊢ x > y ↔ rpow x q > rpow y q All goals completed! 🐙

Proposition 6.7.3(e) / Exercise 6.7.1

theorem declaration uses `sorry`Real.ratPow_mono_of_gt_one {x:ℝ} (hx: x > 1) {q r:ℝ} : rpow x q > rpow x r ↔ q > r := x:ℝhx:x > 1q:ℝr:ℝ⊢ rpow x q > rpow x r ↔ q > r All goals completed! 🐙

Proposition 6.7.3(e) / Exercise 6.7.1

theorem declaration uses `sorry`Real.ratPow_mono_of_lt_one {x:ℝ} (hx0: 0 < x) (hx: x < 1) {q r:ℝ} : rpow x q > rpow x r ↔ q < r := x:ℝhx0:0 < xhx:x < 1q:ℝr:ℝ⊢ rpow x q > rpow x r ↔ q < r All goals completed! 🐙

Proposition 6.7.3(f) / Exercise 6.7.1

theorem declaration uses `sorry`Real.ratPow_mul {x y:ℝ} (hx: x > 0) (hy: y > 0) (q:ℝ) : rpow (x*y) q = rpow x q * rpow y q := x:ℝy:ℝhx:x > 0hy:y > 0q:ℝ⊢ rpow (x * y) q = rpow x q * rpow y q All goals completed! 🐙
end Chapter6