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	a1i	$⊢ φ \to (F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F))$
10	9	biimpa	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (F)$
11	1 2 3 4 5	climeq	$⊢ φ \to (F ⇝ ⇝ (F) \leftrightarrow G ⇝ ⇝ (F))$
12	11	adantr	$⊢ (φ \land F \in dom ⇝) \to (F ⇝ ⇝ (F) \leftrightarrow G ⇝ ⇝ (F))$
13	10 12	mpbid	$⊢ (φ \land F \in dom ⇝) \to G ⇝ ⇝ (F)$
14		breldmg	$⊢ (G \in W \land ⇝ (F) \in V \land G ⇝ ⇝ (F)) \to G \in dom ⇝$
15	6 7 13 14	syl3anc	$⊢ (φ \land F \in dom ⇝) \to G \in dom ⇝$
16	15	ex	$⊢ φ \to (F \in dom ⇝ \to G \in dom ⇝)$
17	2	adantr	$⊢ (φ \land G \in dom ⇝) \to F \in V$
18		fvexd	$⊢ (φ \land G \in dom ⇝) \to ⇝ (G) \in V$
19		climdm	$⊢ G \in dom ⇝ \leftrightarrow G ⇝ ⇝ (G)$
20	19	biimpi	$⊢ G \in dom ⇝ \to G ⇝ ⇝ (G)$
21	20	adantl	$⊢ (φ \land G \in dom ⇝) \to G ⇝ ⇝ (G)$
22	5	eqcomd	$⊢ (φ \land k \in Z) \to G (k) = F (k)$
23	1 3 2 4 22	climeq	$⊢ φ \to (G ⇝ ⇝ (G) \leftrightarrow F ⇝ ⇝ (G))$
24	23	adantr	$⊢ (φ \land G \in dom ⇝) \to (G ⇝ ⇝ (G) \leftrightarrow F ⇝ ⇝ (G))$
25	21 24	mpbid	$⊢ (φ \land G \in dom ⇝) \to F ⇝ ⇝ (G)$
26		breldmg	$⊢ (F \in V \land ⇝ (G) \in V \land F ⇝ ⇝ (G)) \to F \in dom ⇝$
27	17 18 25 26	syl3anc	$⊢ (φ \land G \in dom ⇝) \to F \in dom ⇝$
28	27	ex	$⊢ φ \to (G \in dom ⇝ \to F \in dom ⇝)$
29	16 28	impbid	$⊢ φ \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$

Metamath Proof Explorer

Theorem climeldmeq

Proof