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

Metamath Proof Explorer

Theorem climeldmeqmpt

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 climeldmeqmpt.k ⊢ Ⅎ 𝑘 𝜑
climeldmeqmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climeldmeqmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climeldmeqmpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
climeldmeqmpt.i ⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
climeldmeqmpt.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
climeldmeqmpt.t ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
climeldmeqmpt.l ⊢ ( 𝜑 → 𝑍 ⊆ 𝐶 )
climeldmeqmpt.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐷 ∈ 𝑊 )
climeldmeqmpt.e ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 )
Assertion climeldmeqmpt ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ dom ⇝ ↔ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ∈ dom ⇝ ) )

Proof

Step Hyp Ref Expression
1 climeldmeqmpt.k ⊢ Ⅎ 𝑘 𝜑
2 climeldmeqmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climeldmeqmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 climeldmeqmpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
5 climeldmeqmpt.i ⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
6 climeldmeqmpt.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
7 climeldmeqmpt.t ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
8 climeldmeqmpt.l ⊢ ( 𝜑 → 𝑍 ⊆ 𝐶 )
9 climeldmeqmpt.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐷 ∈ 𝑊 )
10 climeldmeqmpt.e ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 )
11 4 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
12 7 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ∈ V )
13 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
14 1 13 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
15 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
16 nfcv ⊢ Ⅎ 𝑘 𝑗
17 16 nfcsb1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐷
18 15 17 nfeq ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷
19 14 18 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
20 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
21 20 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
22 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
23 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐷 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
24 22 23 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 = 𝐷 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ) )
25 21 24 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ) ) )
26 19 25 10 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
27 5 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝐴 )
28 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
29 1 28 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
30 nfcv ⊢ Ⅎ 𝑘 𝑉
31 15 30 nfel ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉
32 29 31 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 )
33 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
34 33 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
35 22 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 ) )
36 34 35 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 ) ) )
37 32 36 6 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 )
38 27 37 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 )
39 16 nfcsb1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
40 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
41 16 39 22 40 fvmptf ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
42 27 38 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
43 8 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝐶 )
44 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝐶
45 1 44 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐶 )
46 nfcv ⊢ Ⅎ 𝑘 𝑊
47 17 46 nfel ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊
48 45 47 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 )
49 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐶 ↔ 𝑗 ∈ 𝐶 ) )
50 49 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) ) )
51 23 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐷 ∈ 𝑊 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 ) )
52 50 51 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐷 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 ) ) )
53 48 52 9 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 )
54 43 53 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 )
55 eqid ⊢ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑘 ∈ 𝐶 ↦ 𝐷 )
56 16 17 23 55 fvmptf ⊢ ( ( 𝑗 ∈ 𝐶 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
57 43 54 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
58 26 42 57 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) )
59 3 11 12 2 58 climeldmeq ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ dom ⇝ ↔ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ∈ dom ⇝ ) )