Metamath Proof Explorer


Theorem abelthlem6

Description: Lemma for abelth . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Hypotheses abelth.1 φ A : 0
abelth.2 φ seq 0 + A dom
abelth.3 φ M
abelth.4 φ 0 M
abelth.5 S = z | 1 z M 1 z
abelth.6 F = x S n 0 A n x n
abelth.7 φ seq 0 + A 0
abelthlem6.1 φ X S 1
Assertion abelthlem6 φ F X = 1 X n 0 seq 0 + A n X n

Proof

Step Hyp Ref Expression
1 abelth.1 φ A : 0
2 abelth.2 φ seq 0 + A dom
3 abelth.3 φ M
4 abelth.4 φ 0 M
5 abelth.5 S = z | 1 z M 1 z
6 abelth.6 F = x S n 0 A n x n
7 abelth.7 φ seq 0 + A 0
8 abelthlem6.1 φ X S 1
9 8 eldifad φ X S
10 oveq1 x = X x n = X n
11 10 oveq2d x = X A n x n = A n X n
12 11 sumeq2sdv x = X n 0 A n x n = n 0 A n X n
13 sumex n 0 A n X n V
14 12 6 13 fvmpt X S F X = n 0 A n X n
15 9 14 syl φ F X = n 0 A n X n
16 nn0uz 0 = 0
17 0zd φ 0
18 fveq2 k = n A k = A n
19 oveq2 k = n X k = X n
20 18 19 oveq12d k = n A k X k = A n X n
21 eqid k 0 A k X k = k 0 A k X k
22 ovex A n X n V
23 20 21 22 fvmpt n 0 k 0 A k X k n = A n X n
24 23 adantl φ n 0 k 0 A k X k n = A n X n
25 1 ffvelrnda φ n 0 A n
26 5 ssrab3 S
27 26 9 sselid φ X
28 expcl X n 0 X n
29 27 28 sylan φ n 0 X n
30 25 29 mulcld φ n 0 A n X n
31 fveq2 k = n seq 0 + A k = seq 0 + A n
32 31 19 oveq12d k = n seq 0 + A k X k = seq 0 + A n X n
33 eqid k 0 seq 0 + A k X k = k 0 seq 0 + A k X k
34 ovex seq 0 + A n X n V
35 32 33 34 fvmpt n 0 k 0 seq 0 + A k X k n = seq 0 + A n X n
36 35 adantl φ n 0 k 0 seq 0 + A k X k n = seq 0 + A n X n
37 16 17 25 serf φ seq 0 + A : 0
38 37 ffvelrnda φ n 0 seq 0 + A n
39 38 29 mulcld φ n 0 seq 0 + A n X n
40 1 2 3 4 5 abelthlem2 φ 1 S S 1 0 ball abs 1
41 40 simprd φ S 1 0 ball abs 1
42 41 8 sseldd φ X 0 ball abs 1
43 1 2 3 4 5 6 7 abelthlem5 φ X 0 ball abs 1 seq 0 + k 0 seq 0 + A k X k dom
44 42 43 mpdan φ seq 0 + k 0 seq 0 + A k X k dom
45 16 17 36 39 44 isumclim2 φ seq 0 + k 0 seq 0 + A k X k n 0 seq 0 + A n X n
46 seqex seq 0 + k 0 A k X k V
47 46 a1i φ seq 0 + k 0 A k X k V
48 0nn0 0 0
49 48 a1i φ 0 0
50 oveq1 k = i k 1 = i 1
51 50 oveq2d k = i 0 k 1 = 0 i 1
52 51 sumeq1d k = i m = 0 k 1 A m = m = 0 i 1 A m
53 oveq2 k = i X k = X i
54 52 53 oveq12d k = i m = 0 k 1 A m X k = m = 0 i 1 A m X i
55 eqid k 0 m = 0 k 1 A m X k = k 0 m = 0 k 1 A m X k
56 ovex m = 0 i 1 A m X i V
57 54 55 56 fvmpt i 0 k 0 m = 0 k 1 A m X k i = m = 0 i 1 A m X i
58 57 adantl φ i 0 k 0 m = 0 k 1 A m X k i = m = 0 i 1 A m X i
59 fzfid φ i 0 0 i 1 Fin
60 1 adantr φ i 0 A : 0
61 elfznn0 m 0 i 1 m 0
62 ffvelrn A : 0 m 0 A m
63 60 61 62 syl2an φ i 0 m 0 i 1 A m
64 59 63 fsumcl φ i 0 m = 0 i 1 A m
65 expcl X i 0 X i
66 27 65 sylan φ i 0 X i
67 64 66 mulcld φ i 0 m = 0 i 1 A m X i
68 58 67 eqeltrd φ i 0 k 0 m = 0 k 1 A m X k i
69 17 peano2zd φ 0 + 1
70 nnuz = 1
71 1e0p1 1 = 0 + 1
72 71 fveq2i 1 = 0 + 1
73 70 72 eqtri = 0 + 1
74 73 eleq2i n n 0 + 1
75 nnm1nn0 n n 1 0
76 75 adantl φ n n 1 0
77 fveq2 k = n 1 seq 0 + A k = seq 0 + A n 1
78 oveq2 k = n 1 X k = X n 1
79 77 78 oveq12d k = n 1 seq 0 + A k X k = seq 0 + A n 1 X n 1
80 79 oveq2d k = n 1 X seq 0 + A k X k = X seq 0 + A n 1 X n 1
81 eqid k 0 X seq 0 + A k X k = k 0 X seq 0 + A k X k
82 ovex X seq 0 + A n 1 X n 1 V
83 80 81 82 fvmpt n 1 0 k 0 X seq 0 + A k X k n 1 = X seq 0 + A n 1 X n 1
84 76 83 syl φ n k 0 X seq 0 + A k X k n 1 = X seq 0 + A n 1 X n 1
85 ax-1cn 1
86 nncn n n
87 86 adantl φ n n
88 nn0ex 0 V
89 88 mptex k 0 X seq 0 + A k X k V
90 89 shftval 1 n k 0 X seq 0 + A k X k shift 1 n = k 0 X seq 0 + A k X k n 1
91 85 87 90 sylancr φ n k 0 X seq 0 + A k X k shift 1 n = k 0 X seq 0 + A k X k n 1
92 eqidd φ n m 0 n 1 A m = A m
93 76 16 eleqtrdi φ n n 1 0
94 1 adantr φ n A : 0
95 elfznn0 m 0 n 1 m 0
96 94 95 62 syl2an φ n m 0 n 1 A m
97 92 93 96 fsumser φ n m = 0 n 1 A m = seq 0 + A n 1
98 expm1t X n X n = X n 1 X
99 27 98 sylan φ n X n = X n 1 X
100 27 adantr φ n X
101 expcl X n 1 0 X n 1
102 27 75 101 syl2an φ n X n 1
103 100 102 mulcomd φ n X X n 1 = X n 1 X
104 99 103 eqtr4d φ n X n = X X n 1
105 97 104 oveq12d φ n m = 0 n 1 A m X n = seq 0 + A n 1 X X n 1
106 nnnn0 n n 0
107 106 adantl φ n n 0
108 oveq1 k = n k 1 = n 1
109 108 oveq2d k = n 0 k 1 = 0 n 1
110 109 sumeq1d k = n m = 0 k 1 A m = m = 0 n 1 A m
111 110 19 oveq12d k = n m = 0 k 1 A m X k = m = 0 n 1 A m X n
112 ovex m = 0 n 1 A m X n V
113 111 55 112 fvmpt n 0 k 0 m = 0 k 1 A m X k n = m = 0 n 1 A m X n
114 107 113 syl φ n k 0 m = 0 k 1 A m X k n = m = 0 n 1 A m X n
115 ffvelrn seq 0 + A : 0 n 1 0 seq 0 + A n 1
116 37 75 115 syl2an φ n seq 0 + A n 1
117 100 116 102 mul12d φ n X seq 0 + A n 1 X n 1 = seq 0 + A n 1 X X n 1
118 105 114 117 3eqtr4d φ n k 0 m = 0 k 1 A m X k n = X seq 0 + A n 1 X n 1
119 84 91 118 3eqtr4d φ n k 0 X seq 0 + A k X k shift 1 n = k 0 m = 0 k 1 A m X k n
120 74 119 sylan2br φ n 0 + 1 k 0 X seq 0 + A k X k shift 1 n = k 0 m = 0 k 1 A m X k n
121 69 120 seqfeq φ seq 0 + 1 + k 0 X seq 0 + A k X k shift 1 = seq 0 + 1 + k 0 m = 0 k 1 A m X k
122 fveq2 k = i seq 0 + A k = seq 0 + A i
123 122 53 oveq12d k = i seq 0 + A k X k = seq 0 + A i X i
124 ovex seq 0 + A i X i V
125 123 33 124 fvmpt i 0 k 0 seq 0 + A k X k i = seq 0 + A i X i
126 125 adantl φ i 0 k 0 seq 0 + A k X k i = seq 0 + A i X i
127 37 ffvelrnda φ i 0 seq 0 + A i
128 127 66 mulcld φ i 0 seq 0 + A i X i
129 126 128 eqeltrd φ i 0 k 0 seq 0 + A k X k i
130 123 oveq2d k = i X seq 0 + A k X k = X seq 0 + A i X i
131 ovex X seq 0 + A i X i V
132 130 81 131 fvmpt i 0 k 0 X seq 0 + A k X k i = X seq 0 + A i X i
133 132 adantl φ i 0 k 0 X seq 0 + A k X k i = X seq 0 + A i X i
134 126 oveq2d φ i 0 X k 0 seq 0 + A k X k i = X seq 0 + A i X i
135 133 134 eqtr4d φ i 0 k 0 X seq 0 + A k X k i = X k 0 seq 0 + A k X k i
136 16 17 27 45 129 135 isermulc2 φ seq 0 + k 0 X seq 0 + A k X k X n 0 seq 0 + A n X n
137 0z 0
138 1z 1
139 89 isershft 0 1 seq 0 + k 0 X seq 0 + A k X k X n 0 seq 0 + A n X n seq 0 + 1 + k 0 X seq 0 + A k X k shift 1 X n 0 seq 0 + A n X n
140 137 138 139 mp2an seq 0 + k 0 X seq 0 + A k X k X n 0 seq 0 + A n X n seq 0 + 1 + k 0 X seq 0 + A k X k shift 1 X n 0 seq 0 + A n X n
141 136 140 sylib φ seq 0 + 1 + k 0 X seq 0 + A k X k shift 1 X n 0 seq 0 + A n X n
142 121 141 eqbrtrrd φ seq 0 + 1 + k 0 m = 0 k 1 A m X k X n 0 seq 0 + A n X n
143 16 49 68 142 clim2ser2 φ seq 0 + k 0 m = 0 k 1 A m X k X n 0 seq 0 + A n X n + seq 0 + k 0 m = 0 k 1 A m X k 0
144 seq1 0 seq 0 + k 0 m = 0 k 1 A m X k 0 = k 0 m = 0 k 1 A m X k 0
145 137 144 ax-mp seq 0 + k 0 m = 0 k 1 A m X k 0 = k 0 m = 0 k 1 A m X k 0
146 oveq1 k = 0 k 1 = 0 1
147 146 oveq2d k = 0 0 k 1 = 0 0 1
148 risefall0lem 0 0 1 =
149 147 148 eqtrdi k = 0 0 k 1 =
150 149 sumeq1d k = 0 m = 0 k 1 A m = m A m
151 sum0 m A m = 0
152 150 151 eqtrdi k = 0 m = 0 k 1 A m = 0
153 oveq2 k = 0 X k = X 0
154 152 153 oveq12d k = 0 m = 0 k 1 A m X k = 0 X 0
155 ovex 0 X 0 V
156 154 55 155 fvmpt 0 0 k 0 m = 0 k 1 A m X k 0 = 0 X 0
157 48 156 ax-mp k 0 m = 0 k 1 A m X k 0 = 0 X 0
158 145 157 eqtri seq 0 + k 0 m = 0 k 1 A m X k 0 = 0 X 0
159 expcl X 0 0 X 0
160 27 48 159 sylancl φ X 0
161 160 mul02d φ 0 X 0 = 0
162 158 161 eqtrid φ seq 0 + k 0 m = 0 k 1 A m X k 0 = 0
163 162 oveq2d φ X n 0 seq 0 + A n X n + seq 0 + k 0 m = 0 k 1 A m X k 0 = X n 0 seq 0 + A n X n + 0
164 16 17 36 39 44 isumcl φ n 0 seq 0 + A n X n
165 27 164 mulcld φ X n 0 seq 0 + A n X n
166 165 addid1d φ X n 0 seq 0 + A n X n + 0 = X n 0 seq 0 + A n X n
167 163 166 eqtrd φ X n 0 seq 0 + A n X n + seq 0 + k 0 m = 0 k 1 A m X k 0 = X n 0 seq 0 + A n X n
168 143 167 breqtrd φ seq 0 + k 0 m = 0 k 1 A m X k X n 0 seq 0 + A n X n
169 16 17 129 serf φ seq 0 + k 0 seq 0 + A k X k : 0
170 169 ffvelrnda φ i 0 seq 0 + k 0 seq 0 + A k X k i
171 16 17 68 serf φ seq 0 + k 0 m = 0 k 1 A m X k : 0
172 171 ffvelrnda φ i 0 seq 0 + k 0 m = 0 k 1 A m X k i
173 simpr φ i 0 i 0
174 173 16 eleqtrdi φ i 0 i 0
175 simpl φ i 0 φ
176 elfznn0 n 0 i n 0
177 36 39 eqeltrd φ n 0 k 0 seq 0 + A k X k n
178 175 176 177 syl2an φ i 0 n 0 i k 0 seq 0 + A k X k n
179 113 adantl φ n 0 k 0 m = 0 k 1 A m X k n = m = 0 n 1 A m X n
180 fzfid φ n 0 0 n 1 Fin
181 1 adantr φ n 0 A : 0
182 181 95 62 syl2an φ n 0 m 0 n 1 A m
183 180 182 fsumcl φ n 0 m = 0 n 1 A m
184 183 29 mulcld φ n 0 m = 0 n 1 A m X n
185 179 184 eqeltrd φ n 0 k 0 m = 0 k 1 A m X k n
186 175 176 185 syl2an φ i 0 n 0 i k 0 m = 0 k 1 A m X k n
187 eqidd φ n 0 m 0 n A m = A m
188 simpr φ n 0 n 0
189 188 16 eleqtrdi φ n 0 n 0
190 elfznn0 m 0 n m 0
191 181 190 62 syl2an φ n 0 m 0 n A m
192 187 189 191 fsumser φ n 0 m = 0 n A m = seq 0 + A n
193 fveq2 m = n A m = A n
194 189 191 193 fsumm1 φ n 0 m = 0 n A m = m = 0 n 1 A m + A n
195 192 194 eqtr3d φ n 0 seq 0 + A n = m = 0 n 1 A m + A n
196 195 oveq1d φ n 0 seq 0 + A n m = 0 n 1 A m = m = 0 n 1 A m + A n - m = 0 n 1 A m
197 183 25 pncan2d φ n 0 m = 0 n 1 A m + A n - m = 0 n 1 A m = A n
198 196 197 eqtr2d φ n 0 A n = seq 0 + A n m = 0 n 1 A m
199 198 oveq1d φ n 0 A n X n = seq 0 + A n m = 0 n 1 A m X n
200 38 183 29 subdird φ n 0 seq 0 + A n m = 0 n 1 A m X n = seq 0 + A n X n m = 0 n 1 A m X n
201 199 200 eqtrd φ n 0 A n X n = seq 0 + A n X n m = 0 n 1 A m X n
202 36 179 oveq12d φ n 0 k 0 seq 0 + A k X k n k 0 m = 0 k 1 A m X k n = seq 0 + A n X n m = 0 n 1 A m X n
203 201 24 202 3eqtr4d φ n 0 k 0 A k X k n = k 0 seq 0 + A k X k n k 0 m = 0 k 1 A m X k n
204 175 176 203 syl2an φ i 0 n 0 i k 0 A k X k n = k 0 seq 0 + A k X k n k 0 m = 0 k 1 A m X k n
205 174 178 186 204 sersub φ i 0 seq 0 + k 0 A k X k i = seq 0 + k 0 seq 0 + A k X k i seq 0 + k 0 m = 0 k 1 A m X k i
206 16 17 45 47 168 170 172 205 climsub φ seq 0 + k 0 A k X k n 0 seq 0 + A n X n X n 0 seq 0 + A n X n
207 1cnd φ 1
208 207 27 164 subdird φ 1 X n 0 seq 0 + A n X n = 1 n 0 seq 0 + A n X n X n 0 seq 0 + A n X n
209 164 mulid2d φ 1 n 0 seq 0 + A n X n = n 0 seq 0 + A n X n
210 209 oveq1d φ 1 n 0 seq 0 + A n X n X n 0 seq 0 + A n X n = n 0 seq 0 + A n X n X n 0 seq 0 + A n X n
211 208 210 eqtrd φ 1 X n 0 seq 0 + A n X n = n 0 seq 0 + A n X n X n 0 seq 0 + A n X n
212 206 211 breqtrrd φ seq 0 + k 0 A k X k 1 X n 0 seq 0 + A n X n
213 16 17 24 30 212 isumclim φ n 0 A n X n = 1 X n 0 seq 0 + A n X n
214 15 213 eqtrd φ F X = 1 X n 0 seq 0 + A n X n