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

Metamath Proof Explorer

Theorem climeldmeqf

Description: Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 climeldmeqf.p ⊢ Ⅎ k φ
2 climeldmeqf.n ⊢ Ⅎ _ k F
3 climeldmeqf.o ⊢ Ⅎ _ k G
4 climeldmeqf.z ⊢ Z = ℤ ≥ M
5 climeldmeqf.f ⊢ φ → F ∈ V
6 climeldmeqf.g ⊢ φ → G ∈ W
7 climeldmeqf.m ⊢ φ → M ∈ ℤ
8 climeldmeqf.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 4 5 6 7 22 climeldmeq ⊢ φ → F ∈ dom ⁡ ⇝ ↔ G ∈ dom ⁡ ⇝