Theorem climeq

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	climeq.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climeq.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	climeq.3	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	climeq.5	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climeq.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion	climeq	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climeq.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climeq.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		climeq.3	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
4		climeq.5	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		climeq.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
6	1 4 2 5	clim2	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
7		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
8	1 4 3 7	clim2	⊢ ( 𝜑 → ( 𝐺 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
9	6 8	bitr4d	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )