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

Metamath Proof Explorer

Theorem climeqf

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climeqf.p ⊢ Ⅎ 𝑘 𝜑
climeqf.k ⊢ Ⅎ 𝑘 𝐹
climeqf.n ⊢ Ⅎ 𝑘 𝐺
climeqf.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climeqf.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climeqf.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
climeqf.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
climeqf.e ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion climeqf ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 climeqf.p ⊢ Ⅎ 𝑘 𝜑
2 climeqf.k ⊢ Ⅎ 𝑘 𝐹
3 climeqf.n ⊢ Ⅎ 𝑘 𝐺
4 climeqf.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 climeqf.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6 climeqf.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
7 climeqf.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
8 climeqf.e ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
9 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
10 1 9 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
11 nfcv ⊢ Ⅎ 𝑘 𝑗
12 2 11 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
13 3 11 nffv ⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 )
14 12 13 nfeq ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 )
15 10 14 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
16 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
17 16 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
18 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
19 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
20 18 19 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) )
21 17 20 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) ) )
22 15 21 8 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
23 5 6 7 4 22 climeq ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )