α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
⊢ ∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ ∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
haveI := Classical.propDecidable
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
nk : ¬∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
⊢ False
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
⊢ ∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
by_contra nk
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
nk : ¬∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
nk : ¬∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
⊢ False
refine' hf fun ε ε0 => _
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
nk : ¬∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
simp [not_forall] at nk
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
cases' f.cauchy₃ (half_pos ε0) with i hi
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
rcases nk _ (half_pos ε0) i with ⟨j, ij, hj⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
k : ℕ
jk : k ≥ j
⊢ abv (↑f k) < ε
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
refine' ⟨j, fun k jk => _⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this✝ : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
k : ℕ
jk : k ≥ j
this : abv (↑f k - ↑f j + ↑f j) < ε / 2 + ε / 2
⊢ abv (↑f k) < ε
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
k : ℕ
jk : k ≥ j
⊢ abv (↑f k) < ε
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi j ij k jk) hj)
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this✝ : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
k : ℕ
jk : k ≥ j
this : abv (↑f k - ↑f j + ↑f j) < ε / 2 + ε / 2
⊢ abv (↑f k) < ε
rwa [sub_add_cancel, add_halves] at this