Theorem climeqf

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

	Ref	Expression
Hypotheses	climeqf.p	⊢ Ⅎ 𝑘 𝜑
	climeqf.k	⊢ Ⅎ 𝑘 𝐹
	climeqf.n	⊢ Ⅎ 𝑘 𝐺
	climeqf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climeqf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climeqf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	climeqf.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	climeqf.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion	climeqf	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climeqf.p	⊢ Ⅎ 𝑘 𝜑
2		climeqf.k	⊢ Ⅎ 𝑘 𝐹
3		climeqf.n	⊢ Ⅎ 𝑘 𝐺
4		climeqf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		climeqf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6		climeqf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
7		climeqf.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
8		climeqf.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
9		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
10	1 9	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
11		nfcv	⊢ Ⅎ 𝑘 𝑗
12	2 11	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
13	3 11	nffv	⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 )
14	12 13	nfeq	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 )
15	10 14	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
16		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
17	16	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
18		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
19		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
20	18 19	eqeq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) )
21	17 20	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) ) )
22	15 21 8	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
23	5 6 7 4 22	climeq	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )