climfveq

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

	Ref	Expression
Hypotheses	climfveq.1	$⊢ Z = ℤ_{\geq M}$
	climfveq.2	$⊢ φ \to F \in V$
	climfveq.3	$⊢ φ \to G \in W$
	climfveq.4	$⊢ φ \to M \in ℤ$
	climfveq.5	$⊢ (φ \land k \in Z) \to F (k) = G (k)$
Assertion	climfveq	$⊢ φ \to ⇝ (F) = ⇝ (G)$

Proof

Step	Hyp	Ref	Expression
1		climfveq.1	$⊢ Z = ℤ_{\geq M}$
2		climfveq.2	$⊢ φ \to F \in V$
3		climfveq.3	$⊢ φ \to G \in W$
4		climfveq.4	$⊢ φ \to M \in ℤ$
5		climfveq.5	$⊢ (φ \land k \in Z) \to F (k) = G (k)$
6		climdm	$⊢ F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F)$
7	6	biimpi	$⊢ F \in dom ⇝ \to F ⇝ ⇝ (F)$
8	7	adantl	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (F)$
9	8 6	sylibr	$⊢ (φ \land F \in dom ⇝) \to F \in dom ⇝$
10	1 2 3 4 5	climeldmeq	$⊢ φ \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
11	10	adantr	$⊢ (φ \land F \in dom ⇝) \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
12	9 11	mpbid	$⊢ (φ \land F \in dom ⇝) \to G \in dom ⇝$
13		climdm	$⊢ G \in dom ⇝ \leftrightarrow G ⇝ ⇝ (G)$
14	12 13	sylib	$⊢ (φ \land F \in dom ⇝) \to G ⇝ ⇝ (G)$
15	3	adantr	$⊢ (φ \land F \in dom ⇝) \to G \in W$
16	2	adantr	$⊢ (φ \land F \in dom ⇝) \to F \in V$
17	4	adantr	$⊢ (φ \land F \in dom ⇝) \to M \in ℤ$
18	5	eqcomd	$⊢ (φ \land k \in Z) \to G (k) = F (k)$
19	18	adantlr	$⊢ ((φ \land F \in dom ⇝) \land k \in Z) \to G (k) = F (k)$
20	1 15 16 17 19	climeq	$⊢ (φ \land F \in dom ⇝) \to (G ⇝ ⇝ (G) \leftrightarrow F ⇝ ⇝ (G))$
21	14 20	mpbid	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (G)$
22		climuni	$⊢ (F ⇝ ⇝ (F) \land F ⇝ ⇝ (G)) \to ⇝ (F) = ⇝ (G)$
23	8 21 22	syl2anc	$⊢ (φ \land F \in dom ⇝) \to ⇝ (F) = ⇝ (G)$
24		ndmfv	$⊢ \neg F \in dom ⇝ \to ⇝ (F) = \emptyset$
25	24	adantl	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (F) = \emptyset$
26		simpr	$⊢ (φ \land \neg F \in dom ⇝) \to \neg F \in dom ⇝$
27	10	adantr	$⊢ (φ \land \neg F \in dom ⇝) \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
28	26 27	mtbid	$⊢ (φ \land \neg F \in dom ⇝) \to \neg G \in dom ⇝$
29		ndmfv	$⊢ \neg G \in dom ⇝ \to ⇝ (G) = \emptyset$
30	28 29	syl	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (G) = \emptyset$
31	25 30	eqtr4d	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (F) = ⇝ (G)$
32	23 31	pm2.61dan	$⊢ φ \to ⇝ (F) = ⇝ (G)$

Metamath Proof Explorer

Theorem climfveq

Proof