Metamath Proof Explorer

Theorem seqcoll2

Description: The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F . (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses seqcoll2.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑍 + 𝑘 ) = 𝑘 )
seqcoll2.1b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑘 + 𝑍 ) = 𝑘 )
seqcoll2.c ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆 ) ) → ( 𝑘 + 𝑛 ) ∈ 𝑆 )
seqcoll2.a ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
seqcoll2.2 ⊢ ( 𝜑 → 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
seqcoll2.3 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
seqcoll2.5 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
seqcoll2.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
seqcoll2.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
seqcoll2.8 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) )
Assertion seqcoll2 ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 seqcoll2.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑍 + 𝑘 ) = 𝑘 )
2 seqcoll2.1b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑘 + 𝑍 ) = 𝑘 )
3 seqcoll2.c ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆 ) ) → ( 𝑘 + 𝑛 ) ∈ 𝑆 )
4 seqcoll2.a ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
5 seqcoll2.2 ⊢ ( 𝜑 → 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
6 seqcoll2.3 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
7 seqcoll2.5 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
8 seqcoll2.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
9 seqcoll2.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
10 seqcoll2.8 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) )
11 fzssuz ⊢ ( 𝑀 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 )
12 isof1o ⊢ ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
13 5 12 syl ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
14 f1of ⊢ ( 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
15 13 14 syl ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
16 fzfi ⊢ ( 𝑀 ... 𝑁 ) ∈ Fin
17 ssfi ⊢ ( ( ( 𝑀 ... 𝑁 ) ∈ Fin ∧ 𝐴 ⊆ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ Fin )
18 16 7 17 sylancr ⊢ ( 𝜑 → 𝐴 ∈ Fin )
19 hasheq0 ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
20 18 19 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
21 20 necon3bbid ⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 ≠ ∅ ) )
22 6 21 mpbird ⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝐴 ) = 0 )
23 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
24 18 23 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
25 elnn0 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∨ ( ♯ ‘ 𝐴 ) = 0 ) )
26 24 25 sylib ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∨ ( ♯ ‘ 𝐴 ) = 0 ) )
27 26 ord ⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) = 0 ) )
28 22 27 mt3d ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ )
29 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
30 28 29 eleqtrdi ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
31 eluzfz2 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) → ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
32 30 31 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
33 15 32 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ 𝐴 )
34 7 33 sseldd ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( 𝑀 ... 𝑁 ) )
35 11 34 sselid ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
36 elfzuz3 ⊢ ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
37 34 36 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
38 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) → ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ⊆ ( 𝑀 ... 𝑁 ) )
39 37 38 syl ⊢ ( 𝜑 → ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ⊆ ( 𝑀 ... 𝑁 ) )
40 39 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
41 40 8 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
42 35 41 3 seqcl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ∈ 𝑆 )
43 peano2uz ⊢ ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
44 35 43 syl ⊢ ( 𝜑 → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
45 fzss1 ⊢ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
46 44 45 syl ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
47 46 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
48 eluzelre ⊢ ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
49 35 48 syl ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
51 peano2re ⊢ ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℝ → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ∈ ℝ )
52 50 51 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ∈ ℝ )
53 elfzelz ⊢ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) → 𝑘 ∈ ℤ )
54 53 zred ⊢ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) → 𝑘 ∈ ℝ )
55 54 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℝ )
56 50 ltp1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) )
57 elfzle1 ⊢ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ≤ 𝑘 )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ≤ 𝑘 )
59 50 52 55 56 58 ltletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < 𝑘 )
60 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
61 f1ocnv ⊢ ( 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ◡ 𝐺 : 𝐴 –1-1-onto→ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
62 60 61 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ◡ 𝐺 : 𝐴 –1-1-onto→ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
63 f1of ⊢ ( ◡ 𝐺 : 𝐴 –1-1-onto→ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ◡ 𝐺 : 𝐴 ⟶ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
64 62 63 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ◡ 𝐺 : 𝐴 ⟶ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
65 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝑘 ∈ 𝐴 )
66 64 65 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
67 66 elfzelzd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ℤ )
68 67 zred ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ℝ )
69 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
70 69 nn0red ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℝ )
71 elfzle2 ⊢ ( ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( ◡ 𝐺 ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐴 ) )
72 66 71 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ 𝑘 ) ≤ ( ♯ ‘ 𝐴 ) )
73 68 70 72 lensymd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ¬ ( ♯ ‘ 𝐴 ) < ( ◡ 𝐺 ‘ 𝑘 ) )
74 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
75 32 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
76 isorel ⊢ ( ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( ( ♯ ‘ 𝐴 ) < ( ◡ 𝐺 ‘ 𝑘 ) ↔ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
77 74 75 66 76 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( ♯ ‘ 𝐴 ) < ( ◡ 𝐺 ‘ 𝑘 ) ↔ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
78 f1ocnvfv2 ⊢ ( ( 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) = 𝑘 )
79 60 65 78 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) = 𝑘 )
80 79 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < 𝑘 ) )
81 77 80 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( ♯ ‘ 𝐴 ) < ( ◡ 𝐺 ‘ 𝑘 ) ↔ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < 𝑘 ) )
82 73 81 mtbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ 𝐴 ) ) → ¬ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < 𝑘 )
83 82 expr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → ( 𝑘 ∈ 𝐴 → ¬ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) < 𝑘 ) )
84 59 83 mt2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → ¬ 𝑘 ∈ 𝐴 )
85 47 84 eldifd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∖ 𝐴 ) )
86 85 9 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
87 2 35 37 42 86 seqid2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
88 7 11 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
89 39 ssdifd ⊢ ( 𝜑 → ( ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) ⊆ ( ( 𝑀 ... 𝑁 ) ∖ 𝐴 ) )
90 89 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) ) → 𝑘 ∈ ( ( 𝑀 ... 𝑁 ) ∖ 𝐴 ) )
91 90 9 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
92 1 2 3 4 5 32 88 41 91 10 seqcoll ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ 𝐴 ) ) )
93 87 92 eqtr3d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ 𝐴 ) ) )