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	bilani	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (F)$
8	7 6	sylibr	$⊢ (φ \land F \in dom ⇝) \to F \in dom ⇝$
9	1 2 3 4 5	climeldmeq	$⊢ φ \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
10	9	adantr	$⊢ (φ \land F \in dom ⇝) \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
11	8 10	mpbid	$⊢ (φ \land F \in dom ⇝) \to G \in dom ⇝$
12		climdm	$⊢ G \in dom ⇝ \leftrightarrow G ⇝ ⇝ (G)$
13	11 12	sylib	$⊢ (φ \land F \in dom ⇝) \to G ⇝ ⇝ (G)$
14	3	adantr	$⊢ (φ \land F \in dom ⇝) \to G \in W$
15	2	adantr	$⊢ (φ \land F \in dom ⇝) \to F \in V$
16	4	adantr	$⊢ (φ \land F \in dom ⇝) \to M \in ℤ$
17	5	eqcomd	$⊢ (φ \land k \in Z) \to G (k) = F (k)$
18	17	adantlr	$⊢ ((φ \land F \in dom ⇝) \land k \in Z) \to G (k) = F (k)$
19	1 14 15 16 18	climeq	$⊢ (φ \land F \in dom ⇝) \to (G ⇝ ⇝ (G) \leftrightarrow F ⇝ ⇝ (G))$
20	13 19	mpbid	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (G)$
21		climuni	$⊢ (F ⇝ ⇝ (F) \land F ⇝ ⇝ (G)) \to ⇝ (F) = ⇝ (G)$
22	7 20 21	syl2anc	$⊢ (φ \land F \in dom ⇝) \to ⇝ (F) = ⇝ (G)$
23		ndmfv	$⊢ \neg F \in dom ⇝ \to ⇝ (F) = \emptyset$
24	23	adantl	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (F) = \emptyset$
25		simpr	$⊢ (φ \land \neg F \in dom ⇝) \to \neg F \in dom ⇝$
26	9	adantr	$⊢ (φ \land \neg F \in dom ⇝) \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
27	25 26	mtbid	$⊢ (φ \land \neg F \in dom ⇝) \to \neg G \in dom ⇝$
28		ndmfv	$⊢ \neg G \in dom ⇝ \to ⇝ (G) = \emptyset$
29	27 28	syl	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (G) = \emptyset$
30	24 29	eqtr4d	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (F) = ⇝ (G)$
31	22 30	pm2.61dan	$⊢ φ \to ⇝ (F) = ⇝ (G)$

Metamath Proof Explorer

Theorem climfveq

Proof