α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
⊢ False
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
⊢ False
have hlz : LimZero (f * g) := by simpa
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
⊢ False
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
⊢ False
have hf' : ¬LimZero f := by simpa using show ¬LimZero (f - 0) from hf
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
⊢ False
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
⊢ False
have hg' : ¬LimZero g := by simpa using show ¬LimZero (g - 0) from hg
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
⊢ False
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
⊢ False
rcases abv_pos_of_not_limZero hf' with ⟨a1, ha1, N1, hN1⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
⊢ False
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
⊢ False
rcases abv_pos_of_not_limZero hg' with ⟨a2, ha2, N2, hN2⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
⊢ False
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
⊢ False
have : 0 < a1 * a2 := mul_pos ha1 ha2
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
⊢ False
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
⊢ False
cases' hlz _ this with N hN
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
⊢ False
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
⊢ False
let i := max N (max N1 N2)
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
⊢ False
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
⊢ False
have hN' := hN i (le_max_left _ _)
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1' : a1 ≤ abv (↑f i)
⊢ False
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
⊢ False
have hN1' := hN1 i (le_trans (le_max_left _ _) (le_max_right _ _))
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ False
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1' : a1 ≤ abv (↑f i)
⊢ False
have hN1' := hN2 i (le_trans (le_max_right _ _) (le_max_right _ _))
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑(f * g) i)
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ False
apply not_le_of_lt hN'
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑f i * ↑g i)
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑(f * g) i)
change _ ≤ abv (_ * _)
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑f i) * abv (↑g i)
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑f i * ↑g i)
rw [abv_mul abv]
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑f i) * abv (↑g i)
gcongr
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
⊢ LimZero (f * g)
simpa
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
⊢ ¬LimZero f
simpa using show ¬LimZero (f - 0) from hf
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
⊢ ¬LimZero g
simpa using show ¬LimZero (g - 0) from hg