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	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	climfveq.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	climfveq.3	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	climfveq.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climfveq.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion	climfveq	⊢ ( 𝜑 → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		climfveq.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
2		climfveq.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		climfveq.3	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
4		climfveq.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		climfveq.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
6		climdm	⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
7	6	bilani	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
8	7 6	sylibr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
9	1 2 3 4 5	climeldmeq	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
11	8 10	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ dom ⇝ )
12		climdm	⊢ ( 𝐺 ∈ dom ⇝ ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
13	11 12	sylib	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
14	3	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ 𝑊 )
15	2	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
16	4	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
17	5	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
18	17	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
19	1 14 15 16 18	climeq	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
20	13 19	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) )
21		climuni	⊢ ( ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ∧ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
22	7 20 21	syl2anc	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
23		ndmfv	⊢ ( ¬ 𝐹 ∈ dom ⇝ → ( ⇝ ‘ 𝐹 ) = ∅ )
24	23	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ∅ )
25		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐹 ∈ dom ⇝ )
26	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
27	25 26	mtbid	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐺 ∈ dom ⇝ )
28		ndmfv	⊢ ( ¬ 𝐺 ∈ dom ⇝ → ( ⇝ ‘ 𝐺 ) = ∅ )
29	27 28	syl	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐺 ) = ∅ )
30	24 29	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
31	22 30	pm2.61dan	⊢ ( 𝜑 → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem climfveq

Proof