Theorem climeldmeqf

Description: Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		climeldmeqf.p	⊢ Ⅎ 𝑘 𝜑
2		climeldmeqf.n	⊢ Ⅎ 𝑘 𝐹
3		climeldmeqf.o	⊢ Ⅎ 𝑘 𝐺
4		climeldmeqf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		climeldmeqf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
6		climeldmeqf.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
7		climeldmeqf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8		climeldmeqf.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	4 5 6 7 22	climeldmeq	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )