This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climeq

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climeq.1 ⊢ Z = ℤ ≥ M
climeq.2 ⊢ φ → F ∈ V
climeq.3 ⊢ φ → G ∈ W
climeq.5 ⊢ φ → M ∈ ℤ
climeq.6 ⊢ φ ∧ k ∈ Z → F ⁡ k = G ⁡ k
Assertion climeq ⊢ φ → F ⇝ A ↔ G ⇝ A

Proof

Step Hyp Ref Expression
1 climeq.1 ⊢ Z = ℤ ≥ M
2 climeq.2 ⊢ φ → F ∈ V
3 climeq.3 ⊢ φ → G ∈ W
4 climeq.5 ⊢ φ → M ∈ ℤ
5 climeq.6 ⊢ φ ∧ k ∈ Z → F ⁡ k = G ⁡ k
6 1 4 2 5 clim2 ⊢ φ → F ⇝ A ↔ A ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ y ∈ Z ∀ k ∈ ℤ ≥ y G ⁡ k ∈ ℂ ∧ G ⁡ k − A < x
7 eqidd ⊢ φ ∧ k ∈ Z → G ⁡ k = G ⁡ k
8 1 4 3 7 clim2 ⊢ φ → G ⇝ A ↔ A ∈ ℂ ∧ ∀ x ∈ ℝ + ∃ y ∈ Z ∀ k ∈ ℤ ≥ y G ⁡ k ∈ ℂ ∧ G ⁡ k − A < x
9 6 8 bitr4d ⊢ φ → F ⇝ A ↔ G ⇝ A