Step | Hyp | Ref
| Expression |
1 | | elnn0 11294 |
. . 3
|
2 | | simp2 1062 |
. . . . . . 7
|
3 | | simp3 1063 |
. . . . . . 7
|
4 | | fzofi 12773 |
. . . . . . . . 9
..^ |
5 | 4 | a1i 11 |
. . . . . . . 8
..^ |
6 | 2 | adantr 481 |
. . . . . . . . . 10
..^ |
7 | | elfzonn0 12512 |
. . . . . . . . . . 11
..^
|
8 | 7 | adantl 482 |
. . . . . . . . . 10
..^ |
9 | 6, 8 | expcld 13008 |
. . . . . . . . 9
..^ |
10 | 3 | adantr 481 |
. . . . . . . . . 10
..^ |
11 | | ubmelm1fzo 12564 |
. . . . . . . . . . . 12
..^
..^ |
12 | | elfzonn0 12512 |
. . . . . . . . . . . 12
..^
|
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
..^
|
14 | 13 | adantl 482 |
. . . . . . . . . 10
..^ |
15 | 10, 14 | expcld 13008 |
. . . . . . . . 9
..^ |
16 | 9, 15 | mulcld 10060 |
. . . . . . . 8
..^ |
17 | 5, 16 | fsumcl 14464 |
. . . . . . 7
..^ |
18 | 2, 3, 17 | subdird 10487 |
. . . . . 6
..^ ..^ ..^ |
19 | 5, 2, 16 | fsummulc2 14516 |
. . . . . . . 8
..^ ..^ |
20 | 6, 9, 15 | mulassd 10063 |
. . . . . . . . . 10
..^ |
21 | 6, 9 | mulcomd 10061 |
. . . . . . . . . . . 12
..^ |
22 | | expp1 12867 |
. . . . . . . . . . . . 13
|
23 | 2, 7, 22 | syl2an 494 |
. . . . . . . . . . . 12
..^ |
24 | 21, 23 | eqtr4d 2659 |
. . . . . . . . . . 11
..^ |
25 | 24 | oveq1d 6665 |
. . . . . . . . . 10
..^ |
26 | 20, 25 | eqtr3d 2658 |
. . . . . . . . 9
..^ |
27 | 26 | sumeq2dv 14433 |
. . . . . . . 8
..^ ..^ |
28 | 19, 27 | eqtrd 2656 |
. . . . . . 7
..^ ..^ |
29 | 5, 3, 16 | fsummulc2 14516 |
. . . . . . . 8
..^ ..^ |
30 | 10, 16 | mulcomd 10061 |
. . . . . . . . . 10
..^ |
31 | 9, 15, 10 | mulassd 10063 |
. . . . . . . . . 10
..^ |
32 | | expp1 12867 |
. . . . . . . . . . . . . 14
|
33 | 32 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
34 | 3, 13, 33 | syl2an 494 |
. . . . . . . . . . . 12
..^ |
35 | | nncn 11028 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
37 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
..^ |
38 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . 16
..^
|
39 | 38 | zcnd 11483 |
. . . . . . . . . . . . . . 15
..^
|
40 | 39 | adantl 482 |
. . . . . . . . . . . . . 14
..^ |
41 | 37, 40 | subcld 10392 |
. . . . . . . . . . . . 13
..^ |
42 | | npcan1 10455 |
. . . . . . . . . . . . . 14
|
43 | 42 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
44 | 41, 43 | syl 17 |
. . . . . . . . . . . 12
..^ |
45 | 34, 44 | eqtrd 2656 |
. . . . . . . . . . 11
..^ |
46 | 45 | oveq2d 6666 |
. . . . . . . . . 10
..^ |
47 | 30, 31, 46 | 3eqtrd 2660 |
. . . . . . . . 9
..^ |
48 | 47 | sumeq2dv 14433 |
. . . . . . . 8
..^ ..^ |
49 | 29, 48 | eqtrd 2656 |
. . . . . . 7
..^ ..^ |
50 | 28, 49 | oveq12d 6668 |
. . . . . 6
..^ ..^
..^ ..^ |
51 | | nnz 11399 |
. . . . . . . . . . . 12
|
52 | 51 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
53 | | fzoval 12471 |
. . . . . . . . . . 11
..^
|
54 | 52, 53 | syl 17 |
. . . . . . . . . 10
..^
|
55 | 54 | sumeq1d 14431 |
. . . . . . . . 9
..^ |
56 | | nnm1nn0 11334 |
. . . . . . . . . . . 12
|
57 | | nn0uz 11722 |
. . . . . . . . . . . 12
|
58 | 56, 57 | syl6eleq 2711 |
. . . . . . . . . . 11
|
59 | 58 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
60 | 2 | adantr 481 |
. . . . . . . . . . . 12
|
61 | | elfznn0 12433 |
. . . . . . . . . . . . . 14
|
62 | | peano2nn0 11333 |
. . . . . . . . . . . . . 14
|
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . 13
|
64 | 63 | adantl 482 |
. . . . . . . . . . . 12
|
65 | 60, 64 | expcld 13008 |
. . . . . . . . . . 11
|
66 | 3 | adantr 481 |
. . . . . . . . . . . 12
|
67 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
|
68 | 61 | nn0cnd 11353 |
. . . . . . . . . . . . . . 15
|
69 | 68 | adantl 482 |
. . . . . . . . . . . . . 14
|
70 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
71 | 67, 69, 70 | sub32d 10424 |
. . . . . . . . . . . . 13
|
72 | | fznn0sub 12373 |
. . . . . . . . . . . . . 14
|
73 | 72 | adantl 482 |
. . . . . . . . . . . . 13
|
74 | 71, 73 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
75 | 66, 74 | expcld 13008 |
. . . . . . . . . . 11
|
76 | 65, 75 | mulcld 10060 |
. . . . . . . . . 10
|
77 | | oveq1 6657 |
. . . . . . . . . . . 12
|
78 | 77 | oveq2d 6666 |
. . . . . . . . . . 11
|
79 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
80 | 79 | oveq1d 6665 |
. . . . . . . . . . . 12
|
81 | 80 | oveq2d 6666 |
. . . . . . . . . . 11
|
82 | 78, 81 | oveq12d 6668 |
. . . . . . . . . 10
|
83 | 59, 76, 82 | fsumm1 14480 |
. . . . . . . . 9
|
84 | 55, 83 | eqtrd 2656 |
. . . . . . . 8
..^ |
85 | 54 | sumeq1d 14431 |
. . . . . . . . 9
..^ |
86 | 61 | adantl 482 |
. . . . . . . . . . . 12
|
87 | 60, 86 | expcld 13008 |
. . . . . . . . . . 11
|
88 | 54 | eleq2d 2687 |
. . . . . . . . . . . . . 14
..^
|
89 | | fzonnsub 12493 |
. . . . . . . . . . . . . . 15
..^
|
90 | 89 | nnnn0d 11351 |
. . . . . . . . . . . . . 14
..^
|
91 | 88, 90 | syl6bir 244 |
. . . . . . . . . . . . 13
|
92 | 91 | imp 445 |
. . . . . . . . . . . 12
|
93 | 66, 92 | expcld 13008 |
. . . . . . . . . . 11
|
94 | 87, 93 | mulcld 10060 |
. . . . . . . . . 10
|
95 | | oveq2 6658 |
. . . . . . . . . . 11
|
96 | | oveq2 6658 |
. . . . . . . . . . . 12
|
97 | 96 | oveq2d 6666 |
. . . . . . . . . . 11
|
98 | 95, 97 | oveq12d 6668 |
. . . . . . . . . 10
|
99 | 59, 94, 98 | fsum1p 14482 |
. . . . . . . . 9
|
100 | 2 | exp0d 13002 |
. . . . . . . . . . . 12
|
101 | 36 | subid1d 10381 |
. . . . . . . . . . . . 13
|
102 | 101 | oveq2d 6666 |
. . . . . . . . . . . 12
|
103 | 100, 102 | oveq12d 6668 |
. . . . . . . . . . 11
|
104 | | simp1 1061 |
. . . . . . . . . . . . . 14
|
105 | 104 | nnnn0d 11351 |
. . . . . . . . . . . . 13
|
106 | 3, 105 | expcld 13008 |
. . . . . . . . . . . 12
|
107 | 106 | mulid2d 10058 |
. . . . . . . . . . 11
|
108 | 103, 107 | eqtrd 2656 |
. . . . . . . . . 10
|
109 | | 0p1e1 11132 |
. . . . . . . . . . . . 13
|
110 | 109 | a1i 11 |
. . . . . . . . . . . 12
|
111 | 110 | oveq1d 6665 |
. . . . . . . . . . 11
|
112 | 111 | sumeq1d 14431 |
. . . . . . . . . 10
|
113 | 108, 112 | oveq12d 6668 |
. . . . . . . . 9
|
114 | 85, 99, 113 | 3eqtrd 2660 |
. . . . . . . 8
..^ |
115 | 84, 114 | oveq12d 6668 |
. . . . . . 7
..^ ..^
|
116 | | fzfid 12772 |
. . . . . . . . . 10
|
117 | 2 | adantr 481 |
. . . . . . . . . . . 12
|
118 | | elfznn 12370 |
. . . . . . . . . . . . . 14
|
119 | 118 | nnnn0d 11351 |
. . . . . . . . . . . . 13
|
120 | 119 | adantl 482 |
. . . . . . . . . . . 12
|
121 | 117, 120 | expcld 13008 |
. . . . . . . . . . 11
|
122 | 3 | adantr 481 |
. . . . . . . . . . . 12
|
123 | | fzoval 12471 |
. . . . . . . . . . . . . . . 16
..^
|
124 | 52, 123 | syl 17 |
. . . . . . . . . . . . . . 15
..^
|
125 | 124 | eleq2d 2687 |
. . . . . . . . . . . . . 14
..^
|
126 | | fzonnsub 12493 |
. . . . . . . . . . . . . . 15
..^
|
127 | 126 | nnnn0d 11351 |
. . . . . . . . . . . . . 14
..^
|
128 | 125, 127 | syl6bir 244 |
. . . . . . . . . . . . 13
|
129 | 128 | imp 445 |
. . . . . . . . . . . 12
|
130 | 122, 129 | expcld 13008 |
. . . . . . . . . . 11
|
131 | 121, 130 | mulcld 10060 |
. . . . . . . . . 10
|
132 | 116, 131 | fsumcl 14464 |
. . . . . . . . 9
|
133 | 2, 105 | expcld 13008 |
. . . . . . . . 9
|
134 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
135 | 134 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
136 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
137 | 136 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
138 | 137 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
139 | 135, 138 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
140 | 139 | cbvsumv 14426 |
. . . . . . . . . . . 12
|
141 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . 16
|
142 | 141 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
|
143 | 142 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
144 | 143 | a1i 11 |
. . . . . . . . . . . . 13
|
145 | 36 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
146 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . 18
|
147 | 146 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
|
148 | 147 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
149 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
|
150 | 145, 148,
149 | subsub4d 10423 |
. . . . . . . . . . . . . . 15
|
151 | 150 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
152 | 151 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
153 | 144, 152 | sumeq12dv 14437 |
. . . . . . . . . . . 12
|
154 | 140, 153 | syl5eq 2668 |
. . . . . . . . . . 11
|
155 | | 1zzd 11408 |
. . . . . . . . . . . 12
|
156 | | peano2zm 11420 |
. . . . . . . . . . . . 13
|
157 | 52, 156 | syl 17 |
. . . . . . . . . . . 12
|
158 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
159 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
160 | 159 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
161 | 158, 160 | oveq12d 6668 |
. . . . . . . . . . . 12
|
162 | 155, 155,
157, 131, 161 | fsumshftm 14513 |
. . . . . . . . . . 11
|
163 | 154, 162 | eqtr4d 2659 |
. . . . . . . . . 10
|
164 | | npcan1 10455 |
. . . . . . . . . . . . . 14
|
165 | 36, 164 | syl 17 |
. . . . . . . . . . . . 13
|
166 | 165 | oveq2d 6666 |
. . . . . . . . . . . 12
|
167 | | peano2cnm 10347 |
. . . . . . . . . . . . . . . . . 18
|
168 | 35, 167 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
169 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
|
170 | 35, 168, 169 | sub32d 10424 |
. . . . . . . . . . . . . . . 16
|
171 | 168 | subidd 10380 |
. . . . . . . . . . . . . . . 16
|
172 | 170, 171 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
173 | 172 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
174 | 173 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
175 | | exp0 12864 |
. . . . . . . . . . . . . 14
|
176 | 175 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
|
177 | 174, 176 | eqtrd 2656 |
. . . . . . . . . . . 12
|
178 | 166, 177 | oveq12d 6668 |
. . . . . . . . . . 11
|
179 | 133 | mulid1d 10057 |
. . . . . . . . . . 11
|
180 | 178, 179 | eqtrd 2656 |
. . . . . . . . . 10
|
181 | 163, 180 | oveq12d 6668 |
. . . . . . . . 9
|
182 | 132, 133,
181 | comraddd 10250 |
. . . . . . . 8
|
183 | 182 | oveq1d 6665 |
. . . . . . 7
|
184 | 133, 106,
132 | pnpcan2d 10430 |
. . . . . . 7
|
185 | 115, 183,
184 | 3eqtrd 2660 |
. . . . . 6
..^ ..^ |
186 | 18, 50, 185 | 3eqtrrd 2661 |
. . . . 5
..^ |
187 | 186 | 3exp 1264 |
. . . 4
..^ |
188 | | simp2 1062 |
. . . . . . . 8
|
189 | | simp3 1063 |
. . . . . . . 8
|
190 | 188, 189 | subcld 10392 |
. . . . . . 7
|
191 | 190 | mul01d 10235 |
. . . . . 6
|
192 | | oveq2 6658 |
. . . . . . . . . . 11
..^ ..^ |
193 | | fzo0 12492 |
. . . . . . . . . . 11
..^ |
194 | 192, 193 | syl6eq 2672 |
. . . . . . . . . 10
..^ |
195 | 194 | sumeq1d 14431 |
. . . . . . . . 9
..^ |
196 | 195 | 3ad2ant1 1082 |
. . . . . . . 8
..^ |
197 | | sum0 14452 |
. . . . . . . 8
|
198 | 196, 197 | syl6eq 2672 |
. . . . . . 7
..^ |
199 | 198 | oveq2d 6666 |
. . . . . 6
..^ |
200 | | oveq2 6658 |
. . . . . . . . . 10
|
201 | 200 | 3ad2ant1 1082 |
. . . . . . . . 9
|
202 | | exp0 12864 |
. . . . . . . . . 10
|
203 | 202 | 3ad2ant2 1083 |
. . . . . . . . 9
|
204 | 201, 203 | eqtrd 2656 |
. . . . . . . 8
|
205 | | oveq2 6658 |
. . . . . . . . . 10
|
206 | 205 | 3ad2ant1 1082 |
. . . . . . . . 9
|
207 | 175 | 3ad2ant3 1084 |
. . . . . . . . 9
|
208 | 206, 207 | eqtrd 2656 |
. . . . . . . 8
|
209 | 204, 208 | oveq12d 6668 |
. . . . . . 7
|
210 | 209, 141 | syl6eq 2672 |
. . . . . 6
|
211 | 191, 199,
210 | 3eqtr4rd 2667 |
. . . . 5
..^ |
212 | 211 | 3exp 1264 |
. . . 4
..^ |
213 | 187, 212 | jaoi 394 |
. . 3
..^ |
214 | 1, 213 | sylbi 207 |
. 2
..^ |
215 | 214 | 3imp 1256 |
1
..^ |