Step | Hyp | Ref
| Expression |
1 | | gsumle.a |
. . 3
|
2 | | ssid 3624 |
. . . 4
|
3 | | sseq1 3626 |
. . . . . . . 8
|
4 | 3 | anbi2d 740 |
. . . . . . 7
|
5 | | reseq2 5391 |
. . . . . . . . 9
|
6 | 5 | oveq2d 6666 |
. . . . . . . 8
g
g
|
7 | | reseq2 5391 |
. . . . . . . . 9
|
8 | 7 | oveq2d 6666 |
. . . . . . . 8
g
g
|
9 | 6, 8 | breq12d 4666 |
. . . . . . 7
g g
g
g |
10 | 4, 9 | imbi12d 334 |
. . . . . 6
g g
g g |
11 | | sseq1 3626 |
. . . . . . . 8
|
12 | 11 | anbi2d 740 |
. . . . . . 7
|
13 | | reseq2 5391 |
. . . . . . . . 9
|
14 | 13 | oveq2d 6666 |
. . . . . . . 8
g g |
15 | | reseq2 5391 |
. . . . . . . . 9
|
16 | 15 | oveq2d 6666 |
. . . . . . . 8
g g |
17 | 14, 16 | breq12d 4666 |
. . . . . . 7
g g
g
g |
18 | 12, 17 | imbi12d 334 |
. . . . . 6
g g
g
g |
19 | | sseq1 3626 |
. . . . . . . 8
|
20 | 19 | anbi2d 740 |
. . . . . . 7
|
21 | | reseq2 5391 |
. . . . . . . . 9
|
22 | 21 | oveq2d 6666 |
. . . . . . . 8
g g |
23 | | reseq2 5391 |
. . . . . . . . 9
|
24 | 23 | oveq2d 6666 |
. . . . . . . 8
g g |
25 | 22, 24 | breq12d 4666 |
. . . . . . 7
g
g
g
g
|
26 | 20, 25 | imbi12d 334 |
. . . . . 6
g g
g g |
27 | | sseq1 3626 |
. . . . . . . 8
|
28 | 27 | anbi2d 740 |
. . . . . . 7
|
29 | | reseq2 5391 |
. . . . . . . . 9
|
30 | 29 | oveq2d 6666 |
. . . . . . . 8
g g |
31 | | reseq2 5391 |
. . . . . . . . 9
|
32 | 31 | oveq2d 6666 |
. . . . . . . 8
g g |
33 | 30, 32 | breq12d 4666 |
. . . . . . 7
g g
g
g |
34 | 28, 33 | imbi12d 334 |
. . . . . 6
g g
g
g |
35 | | gsumle.m |
. . . . . . . . . 10
oMnd |
36 | | omndtos 29705 |
. . . . . . . . . 10
oMnd Toset |
37 | | tospos 29658 |
. . . . . . . . . 10
Toset |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . 9
|
39 | | res0 5400 |
. . . . . . . . . . . 12
|
40 | 39 | oveq2i 6661 |
. . . . . . . . . . 11
g
g |
41 | | eqid 2622 |
. . . . . . . . . . . 12
|
42 | 41 | gsum0 17278 |
. . . . . . . . . . 11
g |
43 | 40, 42 | eqtri 2644 |
. . . . . . . . . 10
g
|
44 | | omndmnd 29704 |
. . . . . . . . . . 11
oMnd |
45 | | gsumle.b |
. . . . . . . . . . . 12
|
46 | 45, 41 | mndidcl 17308 |
. . . . . . . . . . 11
|
47 | 35, 44, 46 | 3syl 18 |
. . . . . . . . . 10
|
48 | 43, 47 | syl5eqel 2705 |
. . . . . . . . 9
g |
49 | | gsumle.l |
. . . . . . . . . 10
|
50 | 45, 49 | posref 16951 |
. . . . . . . . 9
g g g |
51 | 38, 48, 50 | syl2anc 693 |
. . . . . . . 8
g g |
52 | | res0 5400 |
. . . . . . . . . 10
|
53 | 39, 52 | eqtr4i 2647 |
. . . . . . . . 9
|
54 | 53 | oveq2i 6661 |
. . . . . . . 8
g
g |
55 | 51, 54 | syl6breq 4694 |
. . . . . . 7
g g |
56 | 55 | adantr 481 |
. . . . . 6
g
g |
57 | | ssun1 3776 |
. . . . . . . . . 10
|
58 | | sstr2 3610 |
. . . . . . . . . 10
|
59 | 57, 58 | ax-mp 5 |
. . . . . . . . 9
|
60 | 59 | anim2i 593 |
. . . . . . . 8
|
61 | 60 | imim1i 63 |
. . . . . . 7
g g
g
g |
62 | | simplr 792 |
. . . . . . . . . 10
g
g
|
63 | | simpllr 799 |
. . . . . . . . . 10
g
g
|
64 | | simpr 477 |
. . . . . . . . . 10
g
g g g
|
65 | | eqid 2622 |
. . . . . . . . . . . 12
|
66 | 35 | ad3antrrr 766 |
. . . . . . . . . . . 12
g g
oMnd |
67 | | gsumle.g |
. . . . . . . . . . . . . . 15
|
68 | 67 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
69 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
70 | | ssun2 3777 |
. . . . . . . . . . . . . . . . 17
|
71 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
72 | 71 | snss 4316 |
. . . . . . . . . . . . . . . . 17
|
73 | 70, 72 | mpbir 221 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
|
75 | 69, 74 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
76 | 68, 75 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
77 | 76 | adantr 481 |
. . . . . . . . . . . 12
g g
|
78 | | gsumle.n |
. . . . . . . . . . . . . . 15
CMnd |
79 | 78 | ad2antrr 762 |
. . . . . . . . . . . . . 14
CMnd |
80 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
81 | 80 | a1i 11 |
. . . . . . . . . . . . . 14
|
82 | | gsumle.f |
. . . . . . . . . . . . . . . 16
|
83 | 82 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
84 | 57, 69 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
|
85 | 83, 84 | fssresd 6071 |
. . . . . . . . . . . . . 14
|
86 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
87 | | fvexd 6203 |
. . . . . . . . . . . . . . . 16
|
88 | 83, 86, 87 | fdmfifsupp 8285 |
. . . . . . . . . . . . . . 15
finSupp |
89 | 88, 87 | fsuppres 8300 |
. . . . . . . . . . . . . 14
finSupp |
90 | 45, 41, 79, 81, 85, 89 | gsumcl 18316 |
. . . . . . . . . . . . 13
g |
91 | 90 | adantr 481 |
. . . . . . . . . . . 12
g g
g |
92 | 83, 75 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
93 | 92 | adantr 481 |
. . . . . . . . . . . 12
g g
|
94 | 68, 84 | fssresd 6071 |
. . . . . . . . . . . . . 14
|
95 | | ssfi 8180 |
. . . . . . . . . . . . . . . 16
|
96 | 86, 84, 95 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
97 | 94, 96, 87 | fdmfifsupp 8285 |
. . . . . . . . . . . . . 14
finSupp |
98 | 45, 41, 79, 81, 94, 97 | gsumcl 18316 |
. . . . . . . . . . . . 13
g |
99 | 98 | adantr 481 |
. . . . . . . . . . . 12
g g
g |
100 | | simpr 477 |
. . . . . . . . . . . 12
g g
g g
|
101 | | simpll 790 |
. . . . . . . . . . . . . 14
|
102 | | gsumle.c |
. . . . . . . . . . . . . . 15
|
103 | 102 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
104 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
|
105 | 82, 104 | syl 17 |
. . . . . . . . . . . . . . 15
|
106 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
|
107 | 67, 106 | syl 17 |
. . . . . . . . . . . . . . 15
|
108 | | inidm 3822 |
. . . . . . . . . . . . . . 15
|
109 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
|
110 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
|
111 | 105, 107,
1, 1, 108, 109, 110 | ofrval 6907 |
. . . . . . . . . . . . . 14
|
112 | 101, 103,
75, 111 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
113 | 112 | adantr 481 |
. . . . . . . . . . . 12
g g
|
114 | 79 | adantr 481 |
. . . . . . . . . . . 12
g g
CMnd |
115 | 45, 49, 65, 66, 77, 91, 93, 99, 100, 113, 114 | omndadd2d 29708 |
. . . . . . . . . . 11
g g
g g |
116 | 96 | adantr 481 |
. . . . . . . . . . . . 13
g g
|
117 | 82 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
118 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
|
119 | | elun1 3780 |
. . . . . . . . . . . . . . . . . . 19
|
120 | 119 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
121 | 118, 120 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
|
122 | 117, 121 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
123 | 122 | ex 450 |
. . . . . . . . . . . . . . 15
|
124 | 123 | ad2antrr 762 |
. . . . . . . . . . . . . 14
g g
|
125 | 124 | imp 445 |
. . . . . . . . . . . . 13
g g
|
126 | 71 | a1i 11 |
. . . . . . . . . . . . 13
g g
|
127 | | simplr 792 |
. . . . . . . . . . . . 13
g g
|
128 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
129 | 45, 65, 114, 116, 125, 126, 127, 93, 128 | gsumunsn 18359 |
. . . . . . . . . . . 12
g g
g g |
130 | 83, 69 | feqresmpt 6250 |
. . . . . . . . . . . . . . 15
|
131 | 130 | oveq2d 6666 |
. . . . . . . . . . . . . 14
g g |
132 | 83, 84 | feqresmpt 6250 |
. . . . . . . . . . . . . . . 16
|
133 | 132 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
g g |
134 | 133 | oveq1d 6665 |
. . . . . . . . . . . . . 14
g g |
135 | 131, 134 | eqeq12d 2637 |
. . . . . . . . . . . . 13
g g
g g |
136 | 135 | adantr 481 |
. . . . . . . . . . . 12
g g
g g
g g |
137 | 129, 136 | mpbird 247 |
. . . . . . . . . . 11
g g
g g
|
138 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
139 | 138 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
140 | 121 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
141 | 139, 140 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
142 | 71 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
143 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
144 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
145 | 45, 65, 79, 96, 141, 142, 143, 76, 144 | gsumunsn 18359 |
. . . . . . . . . . . . . . 15
g g |
146 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
147 | 138, 146 | feqresmpt 6250 |
. . . . . . . . . . . . . . . . . 18
|
148 | 147 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
g g |
149 | | resabs1 5427 |
. . . . . . . . . . . . . . . . . . . . 21
|
150 | 57, 149 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
|
151 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
152 | 138, 151 | feqresmpt 6250 |
. . . . . . . . . . . . . . . . . . . 20
|
153 | 150, 152 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
154 | 153 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
g g |
155 | | resabs1 5427 |
. . . . . . . . . . . . . . . . . . . . . 22
|
156 | 70, 155 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
|
157 | 70, 146 | syl5ss 3614 |
. . . . . . . . . . . . . . . . . . . . . 22
|
158 | 138, 157 | feqresmpt 6250 |
. . . . . . . . . . . . . . . . . . . . 21
|
159 | 156, 158 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
|
160 | 159 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
g g |
161 | 35, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
162 | 161 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
163 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
164 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
165 | 146, 164 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
|
166 | 138, 165 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
|
167 | 144 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
168 | 45, 162, 163, 166, 167 | gsumsnd 18352 |
. . . . . . . . . . . . . . . . . . 19
g |
169 | 160, 168 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
g |
170 | 154, 169 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
g
g
g |
171 | 148, 170 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
g g g
g g |
172 | 171 | adantr 481 |
. . . . . . . . . . . . . . 15
g g g
g g |
173 | 145, 172 | mpbird 247 |
. . . . . . . . . . . . . 14
g g g |
174 | 57, 149 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
175 | 174 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
g g |
176 | 70, 155 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
177 | 176 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
g g
|
178 | 175, 177 | oveq12i 6662 |
. . . . . . . . . . . . . 14
g g g g
|
179 | 173, 178 | syl6eq 2672 |
. . . . . . . . . . . . 13
g g
g |
180 | 70, 69 | syl5ss 3614 |
. . . . . . . . . . . . . . . . 17
|
181 | 68, 180 | feqresmpt 6250 |
. . . . . . . . . . . . . . . 16
|
182 | 181 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
g g |
183 | | cmnmnd 18208 |
. . . . . . . . . . . . . . . . 17
CMnd |
184 | 79, 183 | syl 17 |
. . . . . . . . . . . . . . . 16
|
185 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
186 | 45, 185 | gsumsn 18354 |
. . . . . . . . . . . . . . . 16
g |
187 | 184, 142,
76, 186 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
g |
188 | 182, 187 | eqtrd 2656 |
. . . . . . . . . . . . . 14
g |
189 | 188 | oveq2d 6666 |
. . . . . . . . . . . . 13
g g
g
|
190 | 179, 189 | eqtrd 2656 |
. . . . . . . . . . . 12
g g
|
191 | 190 | adantr 481 |
. . . . . . . . . . 11
g g
g g
|
192 | 115, 137,
191 | 3brtr4d 4685 |
. . . . . . . . . 10
g g
g g |
193 | 62, 63, 64, 192 | syl21anc 1325 |
. . . . . . . . 9
g
g g g |
194 | 193 | exp31 630 |
. . . . . . . 8
g
g g g |
195 | 194 | a2d 29 |
. . . . . . 7
g
g g g |
196 | 61, 195 | syl5 34 |
. . . . . 6
g g
g
g
|
197 | 10, 18, 26, 34, 56, 196 | findcard2s 8201 |
. . . . 5
g
g
|
198 | 197 | imp 445 |
. . . 4
g
g
|
199 | 2, 198 | mpanr2 720 |
. . 3
g
g |
200 | 1, 199 | mpancom 703 |
. 2
g
g
|
201 | | fnresdm 6000 |
. . . 4
|
202 | 105, 201 | syl 17 |
. . 3
|
203 | 202 | oveq2d 6666 |
. 2
g g |
204 | | fnresdm 6000 |
. . . 4
|
205 | 107, 204 | syl 17 |
. . 3
|
206 | 205 | oveq2d 6666 |
. 2
g g |
207 | 200, 203,
206 | 3brtr3d 4684 |
1
g g |