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

Metamath Proof Explorer

Theorem climeldmeqmpt3

Description: Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climeldmeqmpt3.k ⊢ Ⅎ k φ
climeldmeqmpt3.m ⊢ φ → M ∈ ℤ
climeldmeqmpt3.z ⊢ Z = ℤ ≥ M
climeldmeqmpt3.a ⊢ φ → A ∈ V
climeldmeqmpt3.c ⊢ φ → C ∈ W
climeldmeqmpt3.i ⊢ φ → Z ⊆ A
climeldmeqmpt3.s ⊢ φ → Z ⊆ C
climeldmeqmpt3.b ⊢ φ ∧ k ∈ Z → B ∈ U
climeldmeqmpt3.e ⊢ φ ∧ k ∈ Z → B = D
Assertion climeldmeqmpt3 ⊢ φ → k ∈ A ⟼ B ∈ dom ⁡ ⇝ ↔ k ∈ C ⟼ D ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 climeldmeqmpt3.k ⊢ Ⅎ k φ
2 climeldmeqmpt3.m ⊢ φ → M ∈ ℤ
3 climeldmeqmpt3.z ⊢ Z = ℤ ≥ M
4 climeldmeqmpt3.a ⊢ φ → A ∈ V
5 climeldmeqmpt3.c ⊢ φ → C ∈ W
6 climeldmeqmpt3.i ⊢ φ → Z ⊆ A
7 climeldmeqmpt3.s ⊢ φ → Z ⊆ C
8 climeldmeqmpt3.b ⊢ φ ∧ k ∈ Z → B ∈ U
9 climeldmeqmpt3.e ⊢ φ ∧ k ∈ Z → B = D
10 4 mptexd ⊢ φ → k ∈ A ⟼ B ∈ V
11 5 mptexd ⊢ φ → k ∈ C ⟼ D ∈ V
12 nfv ⊢ Ⅎ k j ∈ Z
13 1 12 nfan ⊢ Ⅎ k φ ∧ j ∈ Z
14 nfcsb1v ⊢ Ⅎ _ k ⦋ j / k⦌ B
15 nfcv ⊢ Ⅎ _ k j
16 15 nfcsb1 ⊢ Ⅎ _ k ⦋ j / k⦌ D
17 14 16 nfeq ⊢ Ⅎ k ⦋ j / k⦌ B = ⦋ j / k⦌ D
18 13 17 nfim ⊢ Ⅎ k φ ∧ j ∈ Z → ⦋ j / k⦌ B = ⦋ j / k⦌ D
19 eleq1w ⊢ k = j → k ∈ Z ↔ j ∈ Z
20 19 anbi2d ⊢ k = j → φ ∧ k ∈ Z ↔ φ ∧ j ∈ Z
21 csbeq1a ⊢ k = j → B = ⦋ j / k⦌ B
22 csbeq1a ⊢ k = j → D = ⦋ j / k⦌ D
23 21 22 eqeq12d ⊢ k = j → B = D ↔ ⦋ j / k⦌ B = ⦋ j / k⦌ D
24 20 23 imbi12d ⊢ k = j → φ ∧ k ∈ Z → B = D ↔ φ ∧ j ∈ Z → ⦋ j / k⦌ B = ⦋ j / k⦌ D
25 18 24 9 chvarfv ⊢ φ ∧ j ∈ Z → ⦋ j / k⦌ B = ⦋ j / k⦌ D
26 6 sselda ⊢ φ ∧ j ∈ Z → j ∈ A
27 nfcv ⊢ Ⅎ _ k U
28 14 27 nfel ⊢ Ⅎ k ⦋ j / k⦌ B ∈ U
29 13 28 nfim ⊢ Ⅎ k φ ∧ j ∈ Z → ⦋ j / k⦌ B ∈ U
30 21 eleq1d ⊢ k = j → B ∈ U ↔ ⦋ j / k⦌ B ∈ U
31 20 30 imbi12d ⊢ k = j → φ ∧ k ∈ Z → B ∈ U ↔ φ ∧ j ∈ Z → ⦋ j / k⦌ B ∈ U
32 29 31 8 chvarfv ⊢ φ ∧ j ∈ Z → ⦋ j / k⦌ B ∈ U
33 15 nfcsb1 ⊢ Ⅎ _ k ⦋ j / k⦌ B
34 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
35 15 33 21 34 fvmptf ⊢ j ∈ A ∧ ⦋ j / k⦌ B ∈ U → k ∈ A ⟼ B ⁡ j = ⦋ j / k⦌ B
36 26 32 35 syl2anc ⊢ φ ∧ j ∈ Z → k ∈ A ⟼ B ⁡ j = ⦋ j / k⦌ B
37 7 sselda ⊢ φ ∧ j ∈ Z → j ∈ C
38 25 32 eqeltrrd ⊢ φ ∧ j ∈ Z → ⦋ j / k⦌ D ∈ U
39 eqid ⊢ k ∈ C ⟼ D = k ∈ C ⟼ D
40 15 16 22 39 fvmptf ⊢ j ∈ C ∧ ⦋ j / k⦌ D ∈ U → k ∈ C ⟼ D ⁡ j = ⦋ j / k⦌ D
41 37 38 40 syl2anc ⊢ φ ∧ j ∈ Z → k ∈ C ⟼ D ⁡ j = ⦋ j / k⦌ D
42 25 36 41 3eqtr4d ⊢ φ ∧ j ∈ Z → k ∈ A ⟼ B ⁡ j = k ∈ C ⟼ D ⁡ j
43 3 10 11 2 42 climeldmeq ⊢ φ → k ∈ A ⟼ B ∈ dom ⁡ ⇝ ↔ k ∈ C ⟼ D ∈ dom ⁡ ⇝