Metamath Proof Explorer


Theorem climeldmeq

Description: Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climeldmeq.z 𝑍 = ( ℤ𝑀 )
climeldmeq.f ( 𝜑𝐹𝑉 )
climeldmeq.g ( 𝜑𝐺𝑊 )
climeldmeq.m ( 𝜑𝑀 ∈ ℤ )
climeldmeq.e ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = ( 𝐺𝑘 ) )
Assertion climeldmeq ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )

Proof

Step Hyp Ref Expression
1 climeldmeq.z 𝑍 = ( ℤ𝑀 )
2 climeldmeq.f ( 𝜑𝐹𝑉 )
3 climeldmeq.g ( 𝜑𝐺𝑊 )
4 climeldmeq.m ( 𝜑𝑀 ∈ ℤ )
5 climeldmeq.e ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = ( 𝐺𝑘 ) )
6 3 adantr ( ( 𝜑𝐹 ∈ dom ⇝ ) → 𝐺𝑊 )
7 fvexd ( ( 𝜑𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) ∈ V )
8 climdm ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
9 8 a1i ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ) )
10 9 biimpa ( ( 𝜑𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
11 1 2 3 4 5 climeq ( 𝜑 → ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) )
12 11 adantr ( ( 𝜑𝐹 ∈ dom ⇝ ) → ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) )
13 10 12 mpbid ( ( 𝜑𝐹 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) )
14 breldmg ( ( 𝐺𝑊 ∧ ( ⇝ ‘ 𝐹 ) ∈ V ∧ 𝐺 ⇝ ( ⇝ ‘ 𝐹 ) ) → 𝐺 ∈ dom ⇝ )
15 6 7 13 14 syl3anc ( ( 𝜑𝐹 ∈ dom ⇝ ) → 𝐺 ∈ dom ⇝ )
16 15 ex ( 𝜑 → ( 𝐹 ∈ dom ⇝ → 𝐺 ∈ dom ⇝ ) )
17 2 adantr ( ( 𝜑𝐺 ∈ dom ⇝ ) → 𝐹𝑉 )
18 fvexd ( ( 𝜑𝐺 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐺 ) ∈ V )
19 climdm ( 𝐺 ∈ dom ⇝ ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
20 19 biimpi ( 𝐺 ∈ dom ⇝ → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
21 20 adantl ( ( 𝜑𝐺 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
22 5 eqcomd ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( 𝐹𝑘 ) )
23 1 3 2 4 22 climeq ( 𝜑 → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
24 23 adantr ( ( 𝜑𝐺 ∈ dom ⇝ ) → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
25 21 24 mpbid ( ( 𝜑𝐺 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) )
26 breldmg ( ( 𝐹𝑉 ∧ ( ⇝ ‘ 𝐺 ) ∈ V ∧ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) → 𝐹 ∈ dom ⇝ )
27 17 18 25 26 syl3anc ( ( 𝜑𝐺 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
28 27 ex ( 𝜑 → ( 𝐺 ∈ dom ⇝ → 𝐹 ∈ dom ⇝ ) )
29 16 28 impbid ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )