Step | Hyp | Ref
| Expression |
1 | | cnex 10017 |
. . . 4
|
2 | 1 | a1i 11 |
. . 3
|
3 | | sumex 14418 |
. . . 4
|
4 | 3 | a1i 11 |
. . 3
|
5 | | sumex 14418 |
. . . 4
|
6 | 5 | a1i 11 |
. . 3
|
7 | | plyaddlem.f |
. . 3
|
8 | | plyaddlem.g |
. . 3
|
9 | 2, 4, 6, 7, 8 | offval2 6914 |
. 2
|
10 | | fveq2 6191 |
. . . . . . . 8
|
11 | | oveq2 6658 |
. . . . . . . 8
|
12 | 10, 11 | oveq12d 6668 |
. . . . . . 7
|
13 | 12 | oveq2d 6666 |
. . . . . 6
|
14 | | fveq2 6191 |
. . . . . . . 8
|
15 | | oveq2 6658 |
. . . . . . . 8
|
16 | 14, 15 | oveq12d 6668 |
. . . . . . 7
|
17 | 16 | oveq2d 6666 |
. . . . . 6
|
18 | | elfznn0 12433 |
. . . . . . . . 9
|
19 | | plyaddlem.a |
. . . . . . . . . . . 12
|
20 | 19 | adantr 481 |
. . . . . . . . . . 11
|
21 | 20 | ffvelrnda 6359 |
. . . . . . . . . 10
|
22 | | expcl 12878 |
. . . . . . . . . . 11
|
23 | 22 | adantll 750 |
. . . . . . . . . 10
|
24 | 21, 23 | mulcld 10060 |
. . . . . . . . 9
|
25 | 18, 24 | sylan2 491 |
. . . . . . . 8
|
26 | | elfznn0 12433 |
. . . . . . . . 9
|
27 | | plyaddlem.b |
. . . . . . . . . . . 12
|
28 | 27 | adantr 481 |
. . . . . . . . . . 11
|
29 | 28 | ffvelrnda 6359 |
. . . . . . . . . 10
|
30 | | expcl 12878 |
. . . . . . . . . . 11
|
31 | 30 | adantll 750 |
. . . . . . . . . 10
|
32 | 29, 31 | mulcld 10060 |
. . . . . . . . 9
|
33 | 26, 32 | sylan2 491 |
. . . . . . . 8
|
34 | 25, 33 | anim12dan 882 |
. . . . . . 7
|
35 | | mulcl 10020 |
. . . . . . 7
|
36 | 34, 35 | syl 17 |
. . . . . 6
|
37 | 13, 17, 36 | fsum0diag2 14515 |
. . . . 5
|
38 | | plyaddlem.m |
. . . . . . . . . . . . . 14
|
39 | 38 | nn0cnd 11353 |
. . . . . . . . . . . . 13
|
40 | 39 | ad2antrr 762 |
. . . . . . . . . . . 12
|
41 | | plyaddlem.n |
. . . . . . . . . . . . . 14
|
42 | 41 | nn0cnd 11353 |
. . . . . . . . . . . . 13
|
43 | 42 | ad2antrr 762 |
. . . . . . . . . . . 12
|
44 | | elfznn0 12433 |
. . . . . . . . . . . . . 14
|
45 | 44 | adantl 482 |
. . . . . . . . . . . . 13
|
46 | 45 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
47 | 40, 43, 46 | addsubd 10413 |
. . . . . . . . . . 11
|
48 | | fznn0sub 12373 |
. . . . . . . . . . . . . 14
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . 13
|
50 | | nn0uz 11722 |
. . . . . . . . . . . . 13
|
51 | 49, 50 | syl6eleq 2711 |
. . . . . . . . . . . 12
|
52 | 41 | nn0zd 11480 |
. . . . . . . . . . . . 13
|
53 | 52 | ad2antrr 762 |
. . . . . . . . . . . 12
|
54 | | eluzadd 11716 |
. . . . . . . . . . . 12
|
55 | 51, 53, 54 | syl2anc 693 |
. . . . . . . . . . 11
|
56 | 47, 55 | eqeltrd 2701 |
. . . . . . . . . 10
|
57 | 43 | addid2d 10237 |
. . . . . . . . . . 11
|
58 | 57 | fveq2d 6195 |
. . . . . . . . . 10
|
59 | 56, 58 | eleqtrd 2703 |
. . . . . . . . 9
|
60 | | fzss2 12381 |
. . . . . . . . 9
|
61 | 59, 60 | syl 17 |
. . . . . . . 8
|
62 | 44, 24 | sylan2 491 |
. . . . . . . . . 10
|
63 | 62 | adantr 481 |
. . . . . . . . 9
|
64 | | elfznn0 12433 |
. . . . . . . . . . 11
|
65 | 64, 32 | sylan2 491 |
. . . . . . . . . 10
|
66 | 65 | adantlr 751 |
. . . . . . . . 9
|
67 | 63, 66 | mulcld 10060 |
. . . . . . . 8
|
68 | | eldifn 3733 |
. . . . . . . . . . . . . . . . 17
|
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
70 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 70, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
73 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
74 | 41, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
75 | 74, 50 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
76 | | uzsplit 12412 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
78 | 50, 77 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
80 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
81 | 42, 79, 80 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
82 | 81 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
83 | 82 | uneq1d 3766 |
. . . . . . . . . . . . . . . . . . . . 21
|
84 | 78, 83 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | 84 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
|
86 | 72, 85 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . 18
|
87 | | elun 3753 |
. . . . . . . . . . . . . . . . . 18
|
88 | 86, 87 | sylib 208 |
. . . . . . . . . . . . . . . . 17
|
89 | 88 | ord 392 |
. . . . . . . . . . . . . . . 16
|
90 | 69, 89 | mpd 15 |
. . . . . . . . . . . . . . 15
|
91 | | ffun 6048 |
. . . . . . . . . . . . . . . . . 18
|
92 | 27, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
93 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 93, 78 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . 18
|
95 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 27, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
97 | 94, 96 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . 17
|
98 | | funfvima2 6493 |
. . . . . . . . . . . . . . . . 17
|
99 | 92, 97, 98 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
100 | 99 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
101 | 90, 100 | mpd 15 |
. . . . . . . . . . . . . 14
|
102 | | plyaddlem.b2 |
. . . . . . . . . . . . . . 15
|
103 | 102 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
|
104 | 101, 103 | eleqtrd 2703 |
. . . . . . . . . . . . 13
|
105 | | elsni 4194 |
. . . . . . . . . . . . 13
|
106 | 104, 105 | syl 17 |
. . . . . . . . . . . 12
|
107 | 106 | oveq1d 6665 |
. . . . . . . . . . 11
|
108 | | simplr 792 |
. . . . . . . . . . . . 13
|
109 | 108, 71, 30 | syl2an 494 |
. . . . . . . . . . . 12
|
110 | 109 | mul02d 10234 |
. . . . . . . . . . 11
|
111 | 107, 110 | eqtrd 2656 |
. . . . . . . . . 10
|
112 | 111 | oveq2d 6666 |
. . . . . . . . 9
|
113 | 62 | adantr 481 |
. . . . . . . . . 10
|
114 | 113 | mul01d 10235 |
. . . . . . . . 9
|
115 | 112, 114 | eqtrd 2656 |
. . . . . . . 8
|
116 | | fzfid 12772 |
. . . . . . . 8
|
117 | 61, 67, 115, 116 | fsumss 14456 |
. . . . . . 7
|
118 | 117 | sumeq2dv 14433 |
. . . . . 6
|
119 | | fzfid 12772 |
. . . . . . 7
|
120 | | fzfid 12772 |
. . . . . . 7
|
121 | 119, 120,
62, 65 | fsum2mul 14521 |
. . . . . 6
|
122 | 39, 42 | addcomd 10238 |
. . . . . . . . . 10
|
123 | 41, 50 | syl6eleq 2711 |
. . . . . . . . . . . 12
|
124 | 38 | nn0zd 11480 |
. . . . . . . . . . . 12
|
125 | | eluzadd 11716 |
. . . . . . . . . . . 12
|
126 | 123, 124,
125 | syl2anc 693 |
. . . . . . . . . . 11
|
127 | 39 | addid2d 10237 |
. . . . . . . . . . . 12
|
128 | 127 | fveq2d 6195 |
. . . . . . . . . . 11
|
129 | 126, 128 | eleqtrd 2703 |
. . . . . . . . . 10
|
130 | 122, 129 | eqeltrd 2701 |
. . . . . . . . 9
|
131 | | fzss2 12381 |
. . . . . . . . 9
|
132 | 130, 131 | syl 17 |
. . . . . . . 8
|
133 | 132 | adantr 481 |
. . . . . . 7
|
134 | 62 | adantr 481 |
. . . . . . . . 9
|
135 | 33 | adantlr 751 |
. . . . . . . . 9
|
136 | 134, 135 | mulcld 10060 |
. . . . . . . 8
|
137 | 116, 136 | fsumcl 14464 |
. . . . . . 7
|
138 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . 19
|
139 | 138 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
140 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
141 | 140, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
142 | 141 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
143 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
144 | 38, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
145 | 144, 50 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
146 | | uzsplit 12412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
148 | 50, 147 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
149 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
150 | 39, 79, 149 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
151 | 150 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
152 | 151 | uneq1d 3766 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
153 | 148, 152 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
154 | 153 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
|
155 | 142, 154 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . 20
|
156 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . 20
|
157 | 155, 156 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
|
158 | 157 | ord 392 |
. . . . . . . . . . . . . . . . . 18
|
159 | 139, 158 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
160 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | 19, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
162 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . . . 21
|
163 | 162, 148 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . . . 20
|
164 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
|
165 | 19, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
166 | 163, 165 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . . . 19
|
167 | | funfvima2 6493 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 161, 166,
167 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
169 | 168 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
170 | 159, 169 | mpd 15 |
. . . . . . . . . . . . . . . 16
|
171 | | plyaddlem.a2 |
. . . . . . . . . . . . . . . . 17
|
172 | 171 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
173 | 170, 172 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
|
174 | | elsni 4194 |
. . . . . . . . . . . . . . 15
|
175 | 173, 174 | syl 17 |
. . . . . . . . . . . . . 14
|
176 | 175 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
177 | 141, 23 | sylan2 491 |
. . . . . . . . . . . . . 14
|
178 | 177 | mul02d 10234 |
. . . . . . . . . . . . 13
|
179 | 176, 178 | eqtrd 2656 |
. . . . . . . . . . . 12
|
180 | 179 | adantr 481 |
. . . . . . . . . . 11
|
181 | 180 | oveq1d 6665 |
. . . . . . . . . 10
|
182 | 33 | adantlr 751 |
. . . . . . . . . . 11
|
183 | 182 | mul02d 10234 |
. . . . . . . . . 10
|
184 | 181, 183 | eqtrd 2656 |
. . . . . . . . 9
|
185 | 184 | sumeq2dv 14433 |
. . . . . . . 8
|
186 | | fzfid 12772 |
. . . . . . . . . 10
|
187 | 186 | olcd 408 |
. . . . . . . . 9
|
188 | | sumz 14453 |
. . . . . . . . 9
|
189 | 187, 188 | syl 17 |
. . . . . . . 8
|
190 | 185, 189 | eqtrd 2656 |
. . . . . . 7
|
191 | | fzfid 12772 |
. . . . . . 7
|
192 | 133, 137,
190, 191 | fsumss 14456 |
. . . . . 6
|
193 | 118, 121,
192 | 3eqtr3d 2664 |
. . . . 5
|
194 | | fzfid 12772 |
. . . . . . . 8
|
195 | | elfznn0 12433 |
. . . . . . . . 9
|
196 | 195, 31 | sylan2 491 |
. . . . . . . 8
|
197 | | simpll 790 |
. . . . . . . . . 10
|
198 | | elfznn0 12433 |
. . . . . . . . . 10
|
199 | 19 | ffvelrnda 6359 |
. . . . . . . . . 10
|
200 | 197, 198,
199 | syl2an 494 |
. . . . . . . . 9
|
201 | | fznn0sub 12373 |
. . . . . . . . . 10
|
202 | 27 | ffvelrnda 6359 |
. . . . . . . . . 10
|
203 | 197, 201,
202 | syl2an 494 |
. . . . . . . . 9
|
204 | 200, 203 | mulcld 10060 |
. . . . . . . 8
|
205 | 194, 196,
204 | fsummulc1 14517 |
. . . . . . 7
|
206 | | simplr 792 |
. . . . . . . . . . 11
|
207 | 206, 198,
22 | syl2an 494 |
. . . . . . . . . 10
|
208 | | expcl 12878 |
. . . . . . . . . . 11
|
209 | 206, 201,
208 | syl2an 494 |
. . . . . . . . . 10
|
210 | 200, 207,
203, 209 | mul4d 10248 |
. . . . . . . . 9
|
211 | 206 | adantr 481 |
. . . . . . . . . . . 12
|
212 | 201 | adantl 482 |
. . . . . . . . . . . 12
|
213 | 198 | adantl 482 |
. . . . . . . . . . . 12
|
214 | 211, 212,
213 | expaddd 13010 |
. . . . . . . . . . 11
|
215 | 213 | nn0cnd 11353 |
. . . . . . . . . . . . 13
|
216 | 195 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
217 | 216 | nn0cnd 11353 |
. . . . . . . . . . . . 13
|
218 | 215, 217 | pncan3d 10395 |
. . . . . . . . . . . 12
|
219 | 218 | oveq2d 6666 |
. . . . . . . . . . 11
|
220 | 214, 219 | eqtr3d 2658 |
. . . . . . . . . 10
|
221 | 220 | oveq2d 6666 |
. . . . . . . . 9
|
222 | 210, 221 | eqtrd 2656 |
. . . . . . . 8
|
223 | 222 | sumeq2dv 14433 |
. . . . . . 7
|
224 | 205, 223 | eqtr4d 2659 |
. . . . . 6
|
225 | 224 | sumeq2dv 14433 |
. . . . 5
|
226 | 37, 193, 225 | 3eqtr4rd 2667 |
. . . 4
|
227 | | fveq2 6191 |
. . . . . . 7
|
228 | | oveq2 6658 |
. . . . . . 7
|
229 | 227, 228 | oveq12d 6668 |
. . . . . 6
|
230 | 229 | cbvsumv 14426 |
. . . . 5
|
231 | 230 | oveq2i 6661 |
. . . 4
|
232 | 226, 231 | syl6eq 2672 |
. . 3
|
233 | 232 | mpteq2dva 4744 |
. 2
|
234 | 9, 233 | eqtr4d 2659 |
1
|