Theorem 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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climeldmeq.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	climeldmeq.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	climeldmeq.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climeldmeq.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion	climeldmeq	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )

Proof

Step	Hyp	Ref	Expression
1		climeldmeq.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climeldmeq.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		climeldmeq.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
4		climeldmeq.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		climeldmeq.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ 𝑊 )
7		fvexd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) ∈ V )
8		climdm	⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
9	8	bilani	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
10	1 2 3 4 5	climeq	⊢ ( 𝜑 → ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) )
12	9 11	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) )
13		breldmg	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( ⇝ ‘ 𝐹 ) ∈ V ∧ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) → 𝐺 ∈ dom ⇝ )
14	6 7 12 13	syl3anc	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ dom ⇝ )
15	14	ex	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ → 𝐺 ∈ dom ⇝ ) )
16	2	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
17		fvexd	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐺 ) ∈ V )
18		climdm	⊢ ( 𝐺 ∈ dom ⇝ ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
19	18	bilani	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
20	5	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
21	1 3 2 4 20	climeq	⊢ ( 𝜑 → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
23	19 22	mpbid	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) )
24		breldmg	⊢ ( ( 𝐹 ∈ 𝑉 ∧ ( ⇝ ‘ 𝐺 ) ∈ V ∧ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) → 𝐹 ∈ dom ⇝ )
25	16 17 23 24	syl3anc	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
26	25	ex	⊢ ( 𝜑 → ( 𝐺 ∈ dom ⇝ → 𝐹 ∈ dom ⇝ ) )
27	15 26	impbid	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )