Step | Hyp | Ref
| Expression |
1 | | abelthlem6.1 |
. . . 4
|
2 | 1 | eldifad 3586 |
. . 3
|
3 | | oveq1 6657 |
. . . . . 6
|
4 | 3 | oveq2d 6666 |
. . . . 5
|
5 | 4 | sumeq2sdv 14435 |
. . . 4
|
6 | | abelth.6 |
. . . 4
|
7 | | sumex 14418 |
. . . 4
|
8 | 5, 6, 7 | fvmpt 6282 |
. . 3
|
9 | 2, 8 | syl 17 |
. 2
|
10 | | nn0uz 11722 |
. . 3
|
11 | | 0zd 11389 |
. . 3
|
12 | | fveq2 6191 |
. . . . . 6
|
13 | | oveq2 6658 |
. . . . . 6
|
14 | 12, 13 | oveq12d 6668 |
. . . . 5
|
15 | | eqid 2622 |
. . . . 5
|
16 | | ovex 6678 |
. . . . 5
|
17 | 14, 15, 16 | fvmpt 6282 |
. . . 4
|
18 | 17 | adantl 482 |
. . 3
|
19 | | abelth.1 |
. . . . 5
|
20 | 19 | ffvelrnda 6359 |
. . . 4
|
21 | | abelth.5 |
. . . . . . 7
|
22 | | ssrab2 3687 |
. . . . . . 7
|
23 | 21, 22 | eqsstri 3635 |
. . . . . 6
|
24 | 23, 2 | sseldi 3601 |
. . . . 5
|
25 | | expcl 12878 |
. . . . 5
|
26 | 24, 25 | sylan 488 |
. . . 4
|
27 | 20, 26 | mulcld 10060 |
. . 3
|
28 | | fveq2 6191 |
. . . . . . . . 9
|
29 | 28, 13 | oveq12d 6668 |
. . . . . . . 8
|
30 | | eqid 2622 |
. . . . . . . 8
|
31 | | ovex 6678 |
. . . . . . . 8
|
32 | 29, 30, 31 | fvmpt 6282 |
. . . . . . 7
|
33 | 32 | adantl 482 |
. . . . . 6
|
34 | 10, 11, 20 | serf 12829 |
. . . . . . . 8
|
35 | 34 | ffvelrnda 6359 |
. . . . . . 7
|
36 | 35, 26 | mulcld 10060 |
. . . . . 6
|
37 | | abelth.2 |
. . . . . . . . . 10
|
38 | | abelth.3 |
. . . . . . . . . 10
|
39 | | abelth.4 |
. . . . . . . . . 10
|
40 | 19, 37, 38, 39, 21 | abelthlem2 24186 |
. . . . . . . . 9
|
41 | 40 | simprd 479 |
. . . . . . . 8
|
42 | 41, 1 | sseldd 3604 |
. . . . . . 7
|
43 | | abelth.7 |
. . . . . . . 8
|
44 | 19, 37, 38, 39, 21, 6, 43 | abelthlem5 24189 |
. . . . . . 7
|
45 | 42, 44 | mpdan 702 |
. . . . . 6
|
46 | 10, 11, 33, 36, 45 | isumclim2 14489 |
. . . . 5
|
47 | | seqex 12803 |
. . . . . 6
|
48 | 47 | a1i 11 |
. . . . 5
|
49 | | 0nn0 11307 |
. . . . . . . 8
|
50 | 49 | a1i 11 |
. . . . . . 7
|
51 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
52 | 51 | oveq2d 6666 |
. . . . . . . . . . . 12
|
53 | 52 | sumeq1d 14431 |
. . . . . . . . . . 11
|
54 | | oveq2 6658 |
. . . . . . . . . . 11
|
55 | 53, 54 | oveq12d 6668 |
. . . . . . . . . 10
|
56 | | eqid 2622 |
. . . . . . . . . 10
|
57 | | ovex 6678 |
. . . . . . . . . 10
|
58 | 55, 56, 57 | fvmpt 6282 |
. . . . . . . . 9
|
59 | 58 | adantl 482 |
. . . . . . . 8
|
60 | | fzfid 12772 |
. . . . . . . . . 10
|
61 | 19 | adantr 481 |
. . . . . . . . . . 11
|
62 | | elfznn0 12433 |
. . . . . . . . . . 11
|
63 | | ffvelrn 6357 |
. . . . . . . . . . 11
|
64 | 61, 62, 63 | syl2an 494 |
. . . . . . . . . 10
|
65 | 60, 64 | fsumcl 14464 |
. . . . . . . . 9
|
66 | | expcl 12878 |
. . . . . . . . . 10
|
67 | 24, 66 | sylan 488 |
. . . . . . . . 9
|
68 | 65, 67 | mulcld 10060 |
. . . . . . . 8
|
69 | 59, 68 | eqeltrd 2701 |
. . . . . . 7
|
70 | 11 | peano2zd 11485 |
. . . . . . . . 9
|
71 | | nnuz 11723 |
. . . . . . . . . . . 12
|
72 | | 1e0p1 11552 |
. . . . . . . . . . . . 13
|
73 | 72 | fveq2i 6194 |
. . . . . . . . . . . 12
|
74 | 71, 73 | eqtri 2644 |
. . . . . . . . . . 11
|
75 | 74 | eleq2i 2693 |
. . . . . . . . . 10
|
76 | | nnm1nn0 11334 |
. . . . . . . . . . . . 13
|
77 | 76 | adantl 482 |
. . . . . . . . . . . 12
|
78 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
79 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
80 | 78, 79 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
81 | 80 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
82 | | eqid 2622 |
. . . . . . . . . . . . 13
|
83 | | ovex 6678 |
. . . . . . . . . . . . 13
|
84 | 81, 82, 83 | fvmpt 6282 |
. . . . . . . . . . . 12
|
85 | 77, 84 | syl 17 |
. . . . . . . . . . 11
|
86 | | ax-1cn 9994 |
. . . . . . . . . . . 12
|
87 | | nncn 11028 |
. . . . . . . . . . . . 13
|
88 | 87 | adantl 482 |
. . . . . . . . . . . 12
|
89 | | nn0ex 11298 |
. . . . . . . . . . . . . 14
|
90 | 89 | mptex 6486 |
. . . . . . . . . . . . 13
|
91 | 90 | shftval 13814 |
. . . . . . . . . . . 12
|
92 | 86, 88, 91 | sylancr 695 |
. . . . . . . . . . 11
|
93 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
94 | 77, 10 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
|
95 | 19 | adantr 481 |
. . . . . . . . . . . . . . 15
|
96 | | elfznn0 12433 |
. . . . . . . . . . . . . . 15
|
97 | 95, 96, 63 | syl2an 494 |
. . . . . . . . . . . . . 14
|
98 | 93, 94, 97 | fsumser 14461 |
. . . . . . . . . . . . 13
|
99 | | expm1t 12888 |
. . . . . . . . . . . . . . 15
|
100 | 24, 99 | sylan 488 |
. . . . . . . . . . . . . 14
|
101 | 24 | adantr 481 |
. . . . . . . . . . . . . . 15
|
102 | | expcl 12878 |
. . . . . . . . . . . . . . . 16
|
103 | 24, 76, 102 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
104 | 101, 103 | mulcomd 10061 |
. . . . . . . . . . . . . 14
|
105 | 100, 104 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
106 | 98, 105 | oveq12d 6668 |
. . . . . . . . . . . 12
|
107 | | nnnn0 11299 |
. . . . . . . . . . . . . 14
|
108 | 107 | adantl 482 |
. . . . . . . . . . . . 13
|
109 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
110 | 109 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
111 | 110 | sumeq1d 14431 |
. . . . . . . . . . . . . . 15
|
112 | 111, 13 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
113 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
114 | 112, 56, 113 | fvmpt 6282 |
. . . . . . . . . . . . 13
|
115 | 108, 114 | syl 17 |
. . . . . . . . . . . 12
|
116 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
|
117 | 34, 76, 116 | syl2an 494 |
. . . . . . . . . . . . 13
|
118 | 101, 117,
103 | mul12d 10245 |
. . . . . . . . . . . 12
|
119 | 106, 115,
118 | 3eqtr4d 2666 |
. . . . . . . . . . 11
|
120 | 85, 92, 119 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
121 | 75, 120 | sylan2br 493 |
. . . . . . . . 9
|
122 | 70, 121 | seqfeq 12826 |
. . . . . . . 8
|
123 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
124 | 123, 54 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
125 | | ovex 6678 |
. . . . . . . . . . . . 13
|
126 | 124, 30, 125 | fvmpt 6282 |
. . . . . . . . . . . 12
|
127 | 126 | adantl 482 |
. . . . . . . . . . 11
|
128 | 34 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
129 | 128, 67 | mulcld 10060 |
. . . . . . . . . . 11
|
130 | 127, 129 | eqeltrd 2701 |
. . . . . . . . . 10
|
131 | 124 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
132 | | ovex 6678 |
. . . . . . . . . . . . 13
|
133 | 131, 82, 132 | fvmpt 6282 |
. . . . . . . . . . . 12
|
134 | 133 | adantl 482 |
. . . . . . . . . . 11
|
135 | 127 | oveq2d 6666 |
. . . . . . . . . . 11
|
136 | 134, 135 | eqtr4d 2659 |
. . . . . . . . . 10
|
137 | 10, 11, 24, 46, 130, 136 | isermulc2 14388 |
. . . . . . . . 9
|
138 | | 0z 11388 |
. . . . . . . . . 10
|
139 | | 1z 11407 |
. . . . . . . . . 10
|
140 | 90 | isershft 14394 |
. . . . . . . . . 10
|
141 | 138, 139,
140 | mp2an 708 |
. . . . . . . . 9
|
142 | 137, 141 | sylib 208 |
. . . . . . . 8
|
143 | 122, 142 | eqbrtrrd 4677 |
. . . . . . 7
|
144 | 10, 50, 69, 143 | clim2ser2 14386 |
. . . . . 6
|
145 | | seq1 12814 |
. . . . . . . . . . 11
|
146 | 138, 145 | ax-mp 5 |
. . . . . . . . . 10
|
147 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
148 | 147 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
149 | | 0re 10040 |
. . . . . . . . . . . . . . . . . 18
|
150 | | ltm1 10863 |
. . . . . . . . . . . . . . . . . 18
|
151 | 149, 150 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
152 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . 19
|
153 | 138, 152 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
154 | | fzn 12357 |
. . . . . . . . . . . . . . . . . 18
|
155 | 138, 153,
154 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
|
156 | 151, 155 | mpbi 220 |
. . . . . . . . . . . . . . . 16
|
157 | 148, 156 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
158 | 157 | sumeq1d 14431 |
. . . . . . . . . . . . . 14
|
159 | | sum0 14452 |
. . . . . . . . . . . . . 14
|
160 | 158, 159 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
161 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
162 | 160, 161 | oveq12d 6668 |
. . . . . . . . . . . 12
|
163 | | ovex 6678 |
. . . . . . . . . . . 12
|
164 | 162, 56, 163 | fvmpt 6282 |
. . . . . . . . . . 11
|
165 | 49, 164 | ax-mp 5 |
. . . . . . . . . 10
|
166 | 146, 165 | eqtri 2644 |
. . . . . . . . 9
|
167 | | expcl 12878 |
. . . . . . . . . . 11
|
168 | 24, 49, 167 | sylancl 694 |
. . . . . . . . . 10
|
169 | 168 | mul02d 10234 |
. . . . . . . . 9
|
170 | 166, 169 | syl5eq 2668 |
. . . . . . . 8
|
171 | 170 | oveq2d 6666 |
. . . . . . 7
|
172 | 10, 11, 33, 36, 45 | isumcl 14492 |
. . . . . . . . 9
|
173 | 24, 172 | mulcld 10060 |
. . . . . . . 8
|
174 | 173 | addid1d 10236 |
. . . . . . 7
|
175 | 171, 174 | eqtrd 2656 |
. . . . . 6
|
176 | 144, 175 | breqtrd 4679 |
. . . . 5
|
177 | 10, 11, 130 | serf 12829 |
. . . . . 6
|
178 | 177 | ffvelrnda 6359 |
. . . . 5
|
179 | 10, 11, 69 | serf 12829 |
. . . . . 6
|
180 | 179 | ffvelrnda 6359 |
. . . . 5
|
181 | | simpr 477 |
. . . . . . 7
|
182 | 181, 10 | syl6eleq 2711 |
. . . . . 6
|
183 | | simpl 473 |
. . . . . . 7
|
184 | | elfznn0 12433 |
. . . . . . 7
|
185 | 33, 36 | eqeltrd 2701 |
. . . . . . 7
|
186 | 183, 184,
185 | syl2an 494 |
. . . . . 6
|
187 | 114 | adantl 482 |
. . . . . . . 8
|
188 | | fzfid 12772 |
. . . . . . . . . 10
|
189 | 19 | adantr 481 |
. . . . . . . . . . 11
|
190 | 189, 96, 63 | syl2an 494 |
. . . . . . . . . 10
|
191 | 188, 190 | fsumcl 14464 |
. . . . . . . . 9
|
192 | 191, 26 | mulcld 10060 |
. . . . . . . 8
|
193 | 187, 192 | eqeltrd 2701 |
. . . . . . 7
|
194 | 183, 184,
193 | syl2an 494 |
. . . . . 6
|
195 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
196 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
197 | 196, 10 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
|
198 | | elfznn0 12433 |
. . . . . . . . . . . . . . 15
|
199 | 189, 198,
63 | syl2an 494 |
. . . . . . . . . . . . . 14
|
200 | 195, 197,
199 | fsumser 14461 |
. . . . . . . . . . . . 13
|
201 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
202 | 197, 199,
201 | fsumm1 14480 |
. . . . . . . . . . . . 13
|
203 | 200, 202 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
204 | 203 | oveq1d 6665 |
. . . . . . . . . . 11
|
205 | 191, 20 | pncan2d 10394 |
. . . . . . . . . . 11
|
206 | 204, 205 | eqtr2d 2657 |
. . . . . . . . . 10
|
207 | 206 | oveq1d 6665 |
. . . . . . . . 9
|
208 | 35, 191, 26 | subdird 10487 |
. . . . . . . . 9
|
209 | 207, 208 | eqtrd 2656 |
. . . . . . . 8
|
210 | 33, 187 | oveq12d 6668 |
. . . . . . . 8
|
211 | 209, 18, 210 | 3eqtr4d 2666 |
. . . . . . 7
|
212 | 183, 184,
211 | syl2an 494 |
. . . . . 6
|
213 | 182, 186,
194, 212 | sersub 12844 |
. . . . 5
|
214 | 10, 11, 46, 48, 176, 178, 180, 213 | climsub 14364 |
. . . 4
|
215 | | 1cnd 10056 |
. . . . . 6
|
216 | 215, 24, 172 | subdird 10487 |
. . . . 5
|
217 | 172 | mulid2d 10058 |
. . . . . 6
|
218 | 217 | oveq1d 6665 |
. . . . 5
|
219 | 216, 218 | eqtrd 2656 |
. . . 4
|
220 | 214, 219 | breqtrrd 4681 |
. . 3
|
221 | 10, 11, 18, 27, 220 | isumclim 14488 |
. 2
|
222 | 9, 221 | eqtrd 2656 |
1
|