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 φseq0+Adom
abelth.3 φM
abelth.4 φ0M
abelth.5 S=z|1zM1z
abelth.6 F=xSn0Anxn
abelth.7 φseq0+A0
abelthlem6.1 φXS1
Assertion abelthlem6 φFX=1Xn0seq0+AnXn

Proof

Step Hyp Ref Expression
1 abelth.1 φA:0
2 abelth.2 φseq0+Adom
3 abelth.3 φM
4 abelth.4 φ0M
5 abelth.5 S=z|1zM1z
6 abelth.6 F=xSn0Anxn
7 abelth.7 φseq0+A0
8 abelthlem6.1 φXS1
9 8 eldifad φXS
10 oveq1 x=Xxn=Xn
11 10 oveq2d x=XAnxn=AnXn
12 11 sumeq2sdv x=Xn0Anxn=n0AnXn
13 sumex n0AnXnV
14 12 6 13 fvmpt XSFX=n0AnXn
15 9 14 syl φFX=n0AnXn
16 nn0uz 0=0
17 0zd φ0
18 fveq2 k=nAk=An
19 oveq2 k=nXk=Xn
20 18 19 oveq12d k=nAkXk=AnXn
21 eqid k0AkXk=k0AkXk
22 ovex AnXnV
23 20 21 22 fvmpt n0k0AkXkn=AnXn
24 23 adantl φn0k0AkXkn=AnXn
25 1 ffvelrnda φn0An
26 5 ssrab3 S
27 26 9 sselid φX
28 expcl Xn0Xn
29 27 28 sylan φn0Xn
30 25 29 mulcld φn0AnXn
31 fveq2 k=nseq0+Ak=seq0+An
32 31 19 oveq12d k=nseq0+AkXk=seq0+AnXn
33 eqid k0seq0+AkXk=k0seq0+AkXk
34 ovex seq0+AnXnV
35 32 33 34 fvmpt n0k0seq0+AkXkn=seq0+AnXn
36 35 adantl φn0k0seq0+AkXkn=seq0+AnXn
37 16 17 25 serf φseq0+A:0
38 37 ffvelrnda φn0seq0+An
39 38 29 mulcld φn0seq0+AnXn
40 1 2 3 4 5 abelthlem2 φ1SS10ballabs1
41 40 simprd φS10ballabs1
42 41 8 sseldd φX0ballabs1
43 1 2 3 4 5 6 7 abelthlem5 φX0ballabs1seq0+k0seq0+AkXkdom
44 42 43 mpdan φseq0+k0seq0+AkXkdom
45 16 17 36 39 44 isumclim2 φseq0+k0seq0+AkXkn0seq0+AnXn
46 seqex seq0+k0AkXkV
47 46 a1i φseq0+k0AkXkV
48 0nn0 00
49 48 a1i φ00
50 oveq1 k=ik1=i1
51 50 oveq2d k=i0k1=0i1
52 51 sumeq1d k=im=0k1Am=m=0i1Am
53 oveq2 k=iXk=Xi
54 52 53 oveq12d k=im=0k1AmXk=m=0i1AmXi
55 eqid k0m=0k1AmXk=k0m=0k1AmXk
56 ovex m=0i1AmXiV
57 54 55 56 fvmpt i0k0m=0k1AmXki=m=0i1AmXi
58 57 adantl φi0k0m=0k1AmXki=m=0i1AmXi
59 fzfid φi00i1Fin
60 1 adantr φi0A:0
61 elfznn0 m0i1m0
62 ffvelrn A:0m0Am
63 60 61 62 syl2an φi0m0i1Am
64 59 63 fsumcl φi0m=0i1Am
65 expcl Xi0Xi
66 27 65 sylan φi0Xi
67 64 66 mulcld φi0m=0i1AmXi
68 58 67 eqeltrd φi0k0m=0k1AmXki
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 nn0+1
75 nnm1nn0 nn10
76 75 adantl φnn10
77 fveq2 k=n1seq0+Ak=seq0+An1
78 oveq2 k=n1Xk=Xn1
79 77 78 oveq12d k=n1seq0+AkXk=seq0+An1Xn1
80 79 oveq2d k=n1Xseq0+AkXk=Xseq0+An1Xn1
81 eqid k0Xseq0+AkXk=k0Xseq0+AkXk
82 ovex Xseq0+An1Xn1V
83 80 81 82 fvmpt n10k0Xseq0+AkXkn1=Xseq0+An1Xn1
84 76 83 syl φnk0Xseq0+AkXkn1=Xseq0+An1Xn1
85 ax-1cn 1
86 nncn nn
87 86 adantl φnn
88 nn0ex 0V
89 88 mptex k0Xseq0+AkXkV
90 89 shftval 1nk0Xseq0+AkXkshift1n=k0Xseq0+AkXkn1
91 85 87 90 sylancr φnk0Xseq0+AkXkshift1n=k0Xseq0+AkXkn1
92 eqidd φnm0n1Am=Am
93 76 16 eleqtrdi φnn10
94 1 adantr φnA:0
95 elfznn0 m0n1m0
96 94 95 62 syl2an φnm0n1Am
97 92 93 96 fsumser φnm=0n1Am=seq0+An1
98 expm1t XnXn=Xn1X
99 27 98 sylan φnXn=Xn1X
100 27 adantr φnX
101 expcl Xn10Xn1
102 27 75 101 syl2an φnXn1
103 100 102 mulcomd φnXXn1=Xn1X
104 99 103 eqtr4d φnXn=XXn1
105 97 104 oveq12d φnm=0n1AmXn=seq0+An1XXn1
106 nnnn0 nn0
107 106 adantl φnn0
108 oveq1 k=nk1=n1
109 108 oveq2d k=n0k1=0n1
110 109 sumeq1d k=nm=0k1Am=m=0n1Am
111 110 19 oveq12d k=nm=0k1AmXk=m=0n1AmXn
112 ovex m=0n1AmXnV
113 111 55 112 fvmpt n0k0m=0k1AmXkn=m=0n1AmXn
114 107 113 syl φnk0m=0k1AmXkn=m=0n1AmXn
115 ffvelrn seq0+A:0n10seq0+An1
116 37 75 115 syl2an φnseq0+An1
117 100 116 102 mul12d φnXseq0+An1Xn1=seq0+An1XXn1
118 105 114 117 3eqtr4d φnk0m=0k1AmXkn=Xseq0+An1Xn1
119 84 91 118 3eqtr4d φnk0Xseq0+AkXkshift1n=k0m=0k1AmXkn
120 74 119 sylan2br φn0+1k0Xseq0+AkXkshift1n=k0m=0k1AmXkn
121 69 120 seqfeq φseq0+1+k0Xseq0+AkXkshift1=seq0+1+k0m=0k1AmXk
122 fveq2 k=iseq0+Ak=seq0+Ai
123 122 53 oveq12d k=iseq0+AkXk=seq0+AiXi
124 ovex seq0+AiXiV
125 123 33 124 fvmpt i0k0seq0+AkXki=seq0+AiXi
126 125 adantl φi0k0seq0+AkXki=seq0+AiXi
127 37 ffvelrnda φi0seq0+Ai
128 127 66 mulcld φi0seq0+AiXi
129 126 128 eqeltrd φi0k0seq0+AkXki
130 123 oveq2d k=iXseq0+AkXk=Xseq0+AiXi
131 ovex Xseq0+AiXiV
132 130 81 131 fvmpt i0k0Xseq0+AkXki=Xseq0+AiXi
133 132 adantl φi0k0Xseq0+AkXki=Xseq0+AiXi
134 126 oveq2d φi0Xk0seq0+AkXki=Xseq0+AiXi
135 133 134 eqtr4d φi0k0Xseq0+AkXki=Xk0seq0+AkXki
136 16 17 27 45 129 135 isermulc2 φseq0+k0Xseq0+AkXkXn0seq0+AnXn
137 0z 0
138 1z 1
139 89 isershft 01seq0+k0Xseq0+AkXkXn0seq0+AnXnseq0+1+k0Xseq0+AkXkshift1Xn0seq0+AnXn
140 137 138 139 mp2an seq0+k0Xseq0+AkXkXn0seq0+AnXnseq0+1+k0Xseq0+AkXkshift1Xn0seq0+AnXn
141 136 140 sylib φseq0+1+k0Xseq0+AkXkshift1Xn0seq0+AnXn
142 121 141 eqbrtrrd φseq0+1+k0m=0k1AmXkXn0seq0+AnXn
143 16 49 68 142 clim2ser2 φseq0+k0m=0k1AmXkXn0seq0+AnXn+seq0+k0m=0k1AmXk0
144 seq1 0seq0+k0m=0k1AmXk0=k0m=0k1AmXk0
145 137 144 ax-mp seq0+k0m=0k1AmXk0=k0m=0k1AmXk0
146 oveq1 k=0k1=01
147 146 oveq2d k=00k1=001
148 risefall0lem 001=
149 147 148 eqtrdi k=00k1=
150 149 sumeq1d k=0m=0k1Am=mAm
151 sum0 mAm=0
152 150 151 eqtrdi k=0m=0k1Am=0
153 oveq2 k=0Xk=X0
154 152 153 oveq12d k=0m=0k1AmXk=0X0
155 ovex 0X0V
156 154 55 155 fvmpt 00k0m=0k1AmXk0=0X0
157 48 156 ax-mp k0m=0k1AmXk0=0X0
158 145 157 eqtri seq0+k0m=0k1AmXk0=0X0
159 expcl X00X0
160 27 48 159 sylancl φX0
161 160 mul02d φ0X0=0
162 158 161 eqtrid φseq0+k0m=0k1AmXk0=0
163 162 oveq2d φXn0seq0+AnXn+seq0+k0m=0k1AmXk0=Xn0seq0+AnXn+0
164 16 17 36 39 44 isumcl φn0seq0+AnXn
165 27 164 mulcld φXn0seq0+AnXn
166 165 addid1d φXn0seq0+AnXn+0=Xn0seq0+AnXn
167 163 166 eqtrd φXn0seq0+AnXn+seq0+k0m=0k1AmXk0=Xn0seq0+AnXn
168 143 167 breqtrd φseq0+k0m=0k1AmXkXn0seq0+AnXn
169 16 17 129 serf φseq0+k0seq0+AkXk:0
170 169 ffvelrnda φi0seq0+k0seq0+AkXki
171 16 17 68 serf φseq0+k0m=0k1AmXk:0
172 171 ffvelrnda φi0seq0+k0m=0k1AmXki
173 simpr φi0i0
174 173 16 eleqtrdi φi0i0
175 simpl φi0φ
176 elfznn0 n0in0
177 36 39 eqeltrd φn0k0seq0+AkXkn
178 175 176 177 syl2an φi0n0ik0seq0+AkXkn
179 113 adantl φn0k0m=0k1AmXkn=m=0n1AmXn
180 fzfid φn00n1Fin
181 1 adantr φn0A:0
182 181 95 62 syl2an φn0m0n1Am
183 180 182 fsumcl φn0m=0n1Am
184 183 29 mulcld φn0m=0n1AmXn
185 179 184 eqeltrd φn0k0m=0k1AmXkn
186 175 176 185 syl2an φi0n0ik0m=0k1AmXkn
187 eqidd φn0m0nAm=Am
188 simpr φn0n0
189 188 16 eleqtrdi φn0n0
190 elfznn0 m0nm0
191 181 190 62 syl2an φn0m0nAm
192 187 189 191 fsumser φn0m=0nAm=seq0+An
193 fveq2 m=nAm=An
194 189 191 193 fsumm1 φn0m=0nAm=m=0n1Am+An
195 192 194 eqtr3d φn0seq0+An=m=0n1Am+An
196 195 oveq1d φn0seq0+Anm=0n1Am=m=0n1Am+An-m=0n1Am
197 183 25 pncan2d φn0m=0n1Am+An-m=0n1Am=An
198 196 197 eqtr2d φn0An=seq0+Anm=0n1Am
199 198 oveq1d φn0AnXn=seq0+Anm=0n1AmXn
200 38 183 29 subdird φn0seq0+Anm=0n1AmXn=seq0+AnXnm=0n1AmXn
201 199 200 eqtrd φn0AnXn=seq0+AnXnm=0n1AmXn
202 36 179 oveq12d φn0k0seq0+AkXknk0m=0k1AmXkn=seq0+AnXnm=0n1AmXn
203 201 24 202 3eqtr4d φn0k0AkXkn=k0seq0+AkXknk0m=0k1AmXkn
204 175 176 203 syl2an φi0n0ik0AkXkn=k0seq0+AkXknk0m=0k1AmXkn
205 174 178 186 204 sersub φi0seq0+k0AkXki=seq0+k0seq0+AkXkiseq0+k0m=0k1AmXki
206 16 17 45 47 168 170 172 205 climsub φseq0+k0AkXkn0seq0+AnXnXn0seq0+AnXn
207 1cnd φ1
208 207 27 164 subdird φ1Xn0seq0+AnXn=1n0seq0+AnXnXn0seq0+AnXn
209 164 mulid2d φ1n0seq0+AnXn=n0seq0+AnXn
210 209 oveq1d φ1n0seq0+AnXnXn0seq0+AnXn=n0seq0+AnXnXn0seq0+AnXn
211 208 210 eqtrd φ1Xn0seq0+AnXn=n0seq0+AnXnXn0seq0+AnXn
212 206 211 breqtrrd φseq0+k0AkXk1Xn0seq0+AnXn
213 16 17 24 30 212 isumclim φn0AnXn=1Xn0seq0+AnXn
214 15 213 eqtrd φFX=1Xn0seq0+AnXn