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 = ℤ_{\geq M}$
	climeldmeq.f	$⊢ φ \to F \in V$
	climeldmeq.g	$⊢ φ \to G \in W$
	climeldmeq.m	$⊢ φ \to M \in ℤ$
	climeldmeq.e	$⊢ (φ \land k \in Z) \to F (k) = G (k)$
Assertion	climeldmeq	$⊢ φ \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$

Proof

Step	Hyp	Ref	Expression
1		climeldmeq.z	$⊢ Z = ℤ_{\geq M}$
2		climeldmeq.f	$⊢ φ \to F \in V$
3		climeldmeq.g	$⊢ φ \to G \in W$
4		climeldmeq.m	$⊢ φ \to M \in ℤ$
5		climeldmeq.e	$⊢ (φ \land k \in Z) \to F (k) = G (k)$
6	3	adantr	$⊢ (φ \land F \in dom ⇝) \to G \in W$
7		fvexd	$⊢ (φ \land F \in dom ⇝) \to ⇝ (F) \in V$
8		climdm	$⊢ F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F)$
9	8	bilani	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (F)$
10	1 2 3 4 5	climeq	$⊢ φ \to (F ⇝ ⇝ (F) \leftrightarrow G ⇝ ⇝ (F))$
11	10	adantr	$⊢ (φ \land F \in dom ⇝) \to (F ⇝ ⇝ (F) \leftrightarrow G ⇝ ⇝ (F))$
12	9 11	mpbid	$⊢ (φ \land F \in dom ⇝) \to G ⇝ ⇝ (F)$
13		breldmg	$⊢ (G \in W \land ⇝ (F) \in V \land G ⇝ ⇝ (F)) \to G \in dom ⇝$
14	6 7 12 13	syl3anc	$⊢ (φ \land F \in dom ⇝) \to G \in dom ⇝$
15	14	ex	$⊢ φ \to (F \in dom ⇝ \to G \in dom ⇝)$
16	2	adantr	$⊢ (φ \land G \in dom ⇝) \to F \in V$
17		fvexd	$⊢ (φ \land G \in dom ⇝) \to ⇝ (G) \in V$
18		climdm	$⊢ G \in dom ⇝ \leftrightarrow G ⇝ ⇝ (G)$
19	18	bilani	$⊢ (φ \land G \in dom ⇝) \to G ⇝ ⇝ (G)$
20	5	eqcomd	$⊢ (φ \land k \in Z) \to G (k) = F (k)$
21	1 3 2 4 20	climeq	$⊢ φ \to (G ⇝ ⇝ (G) \leftrightarrow F ⇝ ⇝ (G))$
22	21	adantr	$⊢ (φ \land G \in dom ⇝) \to (G ⇝ ⇝ (G) \leftrightarrow F ⇝ ⇝ (G))$
23	19 22	mpbid	$⊢ (φ \land G \in dom ⇝) \to F ⇝ ⇝ (G)$
24		breldmg	$⊢ (F \in V \land ⇝ (G) \in V \land F ⇝ ⇝ (G)) \to F \in dom ⇝$
25	16 17 23 24	syl3anc	$⊢ (φ \land G \in dom ⇝) \to F \in dom ⇝$
26	25	ex	$⊢ φ \to (G \in dom ⇝ \to F \in dom ⇝)$
27	15 26	impbid	$⊢ φ \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$

Metamath Proof Explorer

Theorem climeldmeq

Proof