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	a1i	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ) )
10	9	biimpa	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
11	1 2 3 4 5	climeq	⊢ ( 𝜑 → ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) )
13	10 12	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) )
14		breldmg	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( ⇝ ‘ 𝐹 ) ∈ V ∧ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) → 𝐺 ∈ dom ⇝ )
15	6 7 13 14	syl3anc	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ dom ⇝ )
16	15	ex	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ → 𝐺 ∈ dom ⇝ ) )
17	2	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
18		fvexd	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐺 ) ∈ V )
19		climdm	⊢ ( 𝐺 ∈ dom ⇝ ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
20	19	biimpi	⊢ ( 𝐺 ∈ dom ⇝ → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
22	5	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
23	1 3 2 4 22	climeq	⊢ ( 𝜑 → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
25	21 24	mpbid	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) )
26		breldmg	⊢ ( ( 𝐹 ∈ 𝑉 ∧ ( ⇝ ‘ 𝐺 ) ∈ V ∧ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) → 𝐹 ∈ dom ⇝ )
27	17 18 25 26	syl3anc	⊢ ( ( 𝜑 ∧ 𝐺 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
28	27	ex	⊢ ( 𝜑 → ( 𝐺 ∈ dom ⇝ → 𝐹 ∈ dom ⇝ ) )
29	16 28	impbid	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )

Metamath Proof Explorer

Theorem climeldmeq

Proof