Metamath Proof Explorer

Theorem climeqf

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climeqf.p ⊢ Ⅎ k φ
climeqf.k ⊢ Ⅎ _ k F
climeqf.n ⊢ Ⅎ _ k G
climeqf.m ⊢ φ → M ∈ ℤ
climeqf.z ⊢ Z = ℤ ≥ M
climeqf.f ⊢ φ → F ∈ V
climeqf.g ⊢ φ → G ∈ W
climeqf.e ⊢ φ ∧ k ∈ Z → F ⁡ k = G ⁡ k
Assertion climeqf ⊢ φ → F ⇝ A ↔ G ⇝ A

Proof

Step Hyp Ref Expression
1 climeqf.p ⊢ Ⅎ k φ
2 climeqf.k ⊢ Ⅎ _ k F
3 climeqf.n ⊢ Ⅎ _ k G
4 climeqf.m ⊢ φ → M ∈ ℤ
5 climeqf.z ⊢ Z = ℤ ≥ M
6 climeqf.f ⊢ φ → F ∈ V
7 climeqf.g ⊢ φ → G ∈ W
8 climeqf.e ⊢ φ ∧ k ∈ Z → F ⁡ k = G ⁡ k
9 nfv ⊢ Ⅎ k j ∈ Z
10 1 9 nfan ⊢ Ⅎ k φ ∧ j ∈ Z
11 nfcv ⊢ Ⅎ _ k j
12 2 11 nffv ⊢ Ⅎ _ k F ⁡ j
13 3 11 nffv ⊢ Ⅎ _ k G ⁡ j
14 12 13 nfeq ⊢ Ⅎ k F ⁡ j = G ⁡ j
15 10 14 nfim ⊢ Ⅎ k φ ∧ j ∈ Z → F ⁡ j = G ⁡ j
16 eleq1w ⊢ k = j → k ∈ Z ↔ j ∈ Z
17 16 anbi2d ⊢ k = j → φ ∧ k ∈ Z ↔ φ ∧ j ∈ Z
18 fveq2 ⊢ k = j → F ⁡ k = F ⁡ j
19 fveq2 ⊢ k = j → G ⁡ k = G ⁡ j
20 18 19 eqeq12d ⊢ k = j → F ⁡ k = G ⁡ k ↔ F ⁡ j = G ⁡ j
21 17 20 imbi12d ⊢ k = j → φ ∧ k ∈ Z → F ⁡ k = G ⁡ k ↔ φ ∧ j ∈ Z → F ⁡ j = G ⁡ j
22 15 21 8 chvarfv ⊢ φ ∧ j ∈ Z → F ⁡ j = G ⁡ j
23 5 6 7 4 22 climeq ⊢ φ → F ⇝ A ↔ G ⇝ A