This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )