Metamath Proof Explorer

Theorem climeldmeq

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

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

Proof

Step Hyp Ref Expression
1 climeldmeq.z ⊢ Z = ℤ ≥ M
2 climeldmeq.f ⊢ φ → F ∈ V
3 climeldmeq.g ⊢ φ → G ∈ W
4 climeldmeq.m ⊢ φ → M ∈ ℤ
5 climeldmeq.e ⊢ φ ∧ k ∈ Z → F ⁡ k = G ⁡ k
6 3 adantr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → G ∈ W
7 fvexd ⊢ φ ∧ F ∈ dom ⁡ ⇝ → ⇝ ⁡ F ∈ V
8 climdm ⊢ F ∈ dom ⁡ ⇝ ↔ F ⇝ ⇝ ⁡ F
9 8 a1i ⊢ φ → F ∈ dom ⁡ ⇝ ↔ F ⇝ ⇝ ⁡ F
10 9 biimpa ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ⇝ ⇝ ⁡ F
11 1 2 3 4 5 climeq ⊢ φ → F ⇝ ⇝ ⁡ F ↔ G ⇝ ⇝ ⁡ F
12 11 adantr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ⇝ ⇝ ⁡ F ↔ G ⇝ ⇝ ⁡ F
13 10 12 mpbid ⊢ φ ∧ F ∈ dom ⁡ ⇝ → G ⇝ ⇝ ⁡ F
14 breldmg ⊢ G ∈ W ∧ ⇝ ⁡ F ∈ V ∧ G ⇝ ⇝ ⁡ F → G ∈ dom ⁡ ⇝
15 6 7 13 14 syl3anc ⊢ φ ∧ F ∈ dom ⁡ ⇝ → G ∈ dom ⁡ ⇝
16 15 ex ⊢ φ → F ∈ dom ⁡ ⇝ → G ∈ dom ⁡ ⇝
17 2 adantr ⊢ φ ∧ G ∈ dom ⁡ ⇝ → F ∈ V
18 fvexd ⊢ φ ∧ G ∈ dom ⁡ ⇝ → ⇝ ⁡ G ∈ V
19 climdm ⊢ G ∈ dom ⁡ ⇝ ↔ G ⇝ ⇝ ⁡ G
20 19 biimpi ⊢ G ∈ dom ⁡ ⇝ → G ⇝ ⇝ ⁡ G
21 20 adantl ⊢ φ ∧ G ∈ dom ⁡ ⇝ → G ⇝ ⇝ ⁡ G
22 5 eqcomd ⊢ φ ∧ k ∈ Z → G ⁡ k = F ⁡ k
23 1 3 2 4 22 climeq ⊢ φ → G ⇝ ⇝ ⁡ G ↔ F ⇝ ⇝ ⁡ G
24 23 adantr ⊢ φ ∧ G ∈ dom ⁡ ⇝ → G ⇝ ⇝ ⁡ G ↔ F ⇝ ⇝ ⁡ G
25 21 24 mpbid ⊢ φ ∧ G ∈ dom ⁡ ⇝ → F ⇝ ⇝ ⁡ G
26 breldmg ⊢ F ∈ V ∧ ⇝ ⁡ G ∈ V ∧ F ⇝ ⇝ ⁡ G → F ∈ dom ⁡ ⇝
27 17 18 25 26 syl3anc ⊢ φ ∧ G ∈ dom ⁡ ⇝ → F ∈ dom ⁡ ⇝
28 27 ex ⊢ φ → G ∈ dom ⁡ ⇝ → F ∈ dom ⁡ ⇝
29 16 28 impbid ⊢ φ → F ∈ dom ⁡ ⇝ ↔ G ∈ dom ⁡ ⇝