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

Metamath Proof Explorer

Theorem climfveqf

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

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

Proof

Step Hyp Ref Expression
1 climfveqf.p ⊢ Ⅎ 𝑘 𝜑
2 climfveqf.n ⊢ Ⅎ 𝑘 𝐹
3 climfveqf.o ⊢ Ⅎ 𝑘 𝐺
4 climfveqf.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 climfveqf.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
6 climfveqf.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
7 climfveqf.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8 climfveqf.e ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
9 climdm ⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
10 9 biimpi ⊢ ( 𝐹 ∈ dom ⇝ → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
12 11 9 sylibr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
13 nfcv ⊢ Ⅎ 𝑘 𝑗
14 13 nfel1 ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
15 1 14 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
16 2 13 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
17 3 13 nffv ⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 )
18 16 17 nfeq ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 )
19 15 18 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
20 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
21 20 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
22 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
23 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
24 22 23 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) )
25 21 24 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) ) )
26 19 25 8 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
27 4 5 6 7 26 climeldmeq ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
29 12 28 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ dom ⇝ )
30 climdm ⊢ ( 𝐺 ∈ dom ⇝ ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
31 29 30 sylib ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
32 6 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ 𝑊 )
33 5 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
34 7 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
35 26 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
36 35 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
37 4 32 33 34 36 climeq ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
38 31 37 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) )
39 climuni ⊢ ( ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ∧ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
40 11 38 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
41 ndmfv ⊢ ( ¬ 𝐹 ∈ dom ⇝ → ( ⇝ ‘ 𝐹 ) = ∅ )
42 41 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ∅ )
43 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐹 ∈ dom ⇝ )
44 27 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
45 43 44 mtbid ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐺 ∈ dom ⇝ )
46 ndmfv ⊢ ( ¬ 𝐺 ∈ dom ⇝ → ( ⇝ ‘ 𝐺 ) = ∅ )
47 45 46 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐺 ) = ∅ )
48 42 47 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
49 40 48 pm2.61dan ⊢ ( 𝜑 → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )