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 ( 𝜑 → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )