Step | Hyp | Ref
| Expression |
1 | | unieq 4444 |
. . . . . . . . . . 11
|
2 | | uni0 4465 |
. . . . . . . . . . 11
|
3 | 1, 2 | syl6eq 2672 |
. . . . . . . . . 10
|
4 | 3 | ineq2d 3814 |
. . . . . . . . 9
|
5 | | in0 3968 |
. . . . . . . . 9
|
6 | 4, 5 | syl6eq 2672 |
. . . . . . . 8
|
7 | 6 | fveq2d 6195 |
. . . . . . 7
|
8 | | hash0 13158 |
. . . . . . 7
|
9 | 7, 8 | syl6eq 2672 |
. . . . . 6
|
10 | 9 | oveq2d 6666 |
. . . . 5
|
11 | | pweq 4161 |
. . . . . . 7
|
12 | | pw0 4343 |
. . . . . . 7
|
13 | 11, 12 | syl6eq 2672 |
. . . . . 6
|
14 | 13 | sumeq1d 14431 |
. . . . 5
|
15 | 10, 14 | eqeq12d 2637 |
. . . 4
|
16 | 15 | ralbidv 2986 |
. . 3
|
17 | | unieq 4444 |
. . . . . . . 8
|
18 | 17 | ineq2d 3814 |
. . . . . . 7
|
19 | 18 | fveq2d 6195 |
. . . . . 6
|
20 | 19 | oveq2d 6666 |
. . . . 5
|
21 | | pweq 4161 |
. . . . . 6
|
22 | 21 | sumeq1d 14431 |
. . . . 5
|
23 | 20, 22 | eqeq12d 2637 |
. . . 4
|
24 | 23 | ralbidv 2986 |
. . 3
|
25 | | unieq 4444 |
. . . . . . . . 9
|
26 | | uniun 4456 |
. . . . . . . . . 10
|
27 | | vex 3203 |
. . . . . . . . . . . 12
|
28 | 27 | unisn 4451 |
. . . . . . . . . . 11
|
29 | 28 | uneq2i 3764 |
. . . . . . . . . 10
|
30 | 26, 29 | eqtri 2644 |
. . . . . . . . 9
|
31 | 25, 30 | syl6eq 2672 |
. . . . . . . 8
|
32 | 31 | ineq2d 3814 |
. . . . . . 7
|
33 | 32 | fveq2d 6195 |
. . . . . 6
|
34 | 33 | oveq2d 6666 |
. . . . 5
|
35 | | pweq 4161 |
. . . . . 6
|
36 | 35 | sumeq1d 14431 |
. . . . 5
|
37 | 34, 36 | eqeq12d 2637 |
. . . 4
|
38 | 37 | ralbidv 2986 |
. . 3
|
39 | | unieq 4444 |
. . . . . . . 8
|
40 | 39 | ineq2d 3814 |
. . . . . . 7
|
41 | 40 | fveq2d 6195 |
. . . . . 6
|
42 | 41 | oveq2d 6666 |
. . . . 5
|
43 | | pweq 4161 |
. . . . . 6
|
44 | 43 | sumeq1d 14431 |
. . . . 5
|
45 | 42, 44 | eqeq12d 2637 |
. . . 4
|
46 | 45 | ralbidv 2986 |
. . 3
|
47 | | hashcl 13147 |
. . . . . . 7
|
48 | 47 | nn0cnd 11353 |
. . . . . 6
|
49 | 48 | mulid2d 10058 |
. . . . 5
|
50 | | 0ex 4790 |
. . . . . 6
|
51 | 49, 48 | eqeltrd 2701 |
. . . . . 6
|
52 | | fveq2 6191 |
. . . . . . . . . . 11
|
53 | 52, 8 | syl6eq 2672 |
. . . . . . . . . 10
|
54 | 53 | oveq2d 6666 |
. . . . . . . . 9
|
55 | | neg1cn 11124 |
. . . . . . . . . 10
|
56 | | exp0 12864 |
. . . . . . . . . 10
|
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
|
58 | 54, 57 | syl6eq 2672 |
. . . . . . . 8
|
59 | | rint0 4517 |
. . . . . . . . 9
|
60 | 59 | fveq2d 6195 |
. . . . . . . 8
|
61 | 58, 60 | oveq12d 6668 |
. . . . . . 7
|
62 | 61 | sumsn 14475 |
. . . . . 6
|
63 | 50, 51, 62 | sylancr 695 |
. . . . 5
|
64 | 48 | subid1d 10381 |
. . . . 5
|
65 | 49, 63, 64 | 3eqtr4rd 2667 |
. . . 4
|
66 | 65 | rgen 2922 |
. . 3
|
67 | | fveq2 6191 |
. . . . . . . . . . . 12
|
68 | | ineq1 3807 |
. . . . . . . . . . . . 13
|
69 | 68 | fveq2d 6195 |
. . . . . . . . . . . 12
|
70 | 67, 69 | oveq12d 6668 |
. . . . . . . . . . 11
|
71 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
72 | 71 | ineq1d 3813 |
. . . . . . . . . . . . . 14
|
73 | 72 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
74 | 73 | oveq2d 6666 |
. . . . . . . . . . . 12
|
75 | 74 | sumeq2dv 14433 |
. . . . . . . . . . 11
|
76 | 70, 75 | eqeq12d 2637 |
. . . . . . . . . 10
|
77 | 76 | rspcva 3307 |
. . . . . . . . 9
|
78 | 77 | adantll 750 |
. . . . . . . 8
|
79 | | simpr 477 |
. . . . . . . . . 10
|
80 | | inss1 3833 |
. . . . . . . . . 10
|
81 | | ssfi 8180 |
. . . . . . . . . 10
|
82 | 79, 80, 81 | sylancl 694 |
. . . . . . . . 9
|
83 | | fveq2 6191 |
. . . . . . . . . . . 12
|
84 | | ineq1 3807 |
. . . . . . . . . . . . . 14
|
85 | | in32 3825 |
. . . . . . . . . . . . . . 15
|
86 | | inass 3823 |
. . . . . . . . . . . . . . 15
|
87 | 85, 86 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
88 | 84, 87 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
89 | 88 | fveq2d 6195 |
. . . . . . . . . . . 12
|
90 | 83, 89 | oveq12d 6668 |
. . . . . . . . . . 11
|
91 | | ineq1 3807 |
. . . . . . . . . . . . . . 15
|
92 | | in32 3825 |
. . . . . . . . . . . . . . . 16
|
93 | | inass 3823 |
. . . . . . . . . . . . . . . 16
|
94 | 92, 93 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
95 | 91, 94 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
97 | 96 | oveq2d 6666 |
. . . . . . . . . . . 12
|
98 | 97 | sumeq2sdv 14435 |
. . . . . . . . . . 11
|
99 | 90, 98 | eqeq12d 2637 |
. . . . . . . . . 10
|
100 | 99 | rspcva 3307 |
. . . . . . . . 9
|
101 | 82, 100 | sylan 488 |
. . . . . . . 8
|
102 | 78, 101 | oveq12d 6668 |
. . . . . . 7
|
103 | | inss1 3833 |
. . . . . . . . . . . . . 14
|
104 | | ssfi 8180 |
. . . . . . . . . . . . . 14
|
105 | 79, 103, 104 | sylancl 694 |
. . . . . . . . . . . . 13
|
106 | | hashun3 13173 |
. . . . . . . . . . . . 13
|
107 | 105, 82, 106 | syl2anc 693 |
. . . . . . . . . . . 12
|
108 | | indi 3873 |
. . . . . . . . . . . . 13
|
109 | 108 | fveq2i 6194 |
. . . . . . . . . . . 12
|
110 | | inindi 3830 |
. . . . . . . . . . . . . 14
|
111 | 110 | fveq2i 6194 |
. . . . . . . . . . . . 13
|
112 | 111 | oveq2i 6661 |
. . . . . . . . . . . 12
|
113 | 107, 109,
112 | 3eqtr4g 2681 |
. . . . . . . . . . 11
|
114 | | hashcl 13147 |
. . . . . . . . . . . . . 14
|
115 | 105, 114 | syl 17 |
. . . . . . . . . . . . 13
|
116 | 115 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
117 | | hashcl 13147 |
. . . . . . . . . . . . . 14
|
118 | 82, 117 | syl 17 |
. . . . . . . . . . . . 13
|
119 | 118 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
120 | | inss1 3833 |
. . . . . . . . . . . . . . 15
|
121 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
|
122 | 79, 120, 121 | sylancl 694 |
. . . . . . . . . . . . . 14
|
123 | | hashcl 13147 |
. . . . . . . . . . . . . 14
|
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . 13
|
125 | 124 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
126 | 116, 119,
125 | addsubassd 10412 |
. . . . . . . . . . 11
|
127 | 113, 126 | eqtrd 2656 |
. . . . . . . . . 10
|
128 | 127 | oveq2d 6666 |
. . . . . . . . 9
|
129 | | hashcl 13147 |
. . . . . . . . . . . 12
|
130 | 129 | adantl 482 |
. . . . . . . . . . 11
|
131 | 130 | nn0cnd 11353 |
. . . . . . . . . 10
|
132 | 119, 125 | subcld 10392 |
. . . . . . . . . 10
|
133 | 131, 116,
132 | subsub4d 10423 |
. . . . . . . . 9
|
134 | 128, 133 | eqtr4d 2659 |
. . . . . . . 8
|
135 | 134 | adantr 481 |
. . . . . . 7
|
136 | | disjdif 4040 |
. . . . . . . . . . 11
|
137 | 136 | a1i 11 |
. . . . . . . . . 10
|
138 | | ssun1 3776 |
. . . . . . . . . . . . . 14
|
139 | | sspwb 4917 |
. . . . . . . . . . . . . 14
|
140 | 138, 139 | mpbi 220 |
. . . . . . . . . . . . 13
|
141 | | undif 4049 |
. . . . . . . . . . . . 13
|
142 | 140, 141 | mpbi 220 |
. . . . . . . . . . . 12
|
143 | 142 | eqcomi 2631 |
. . . . . . . . . . 11
|
144 | 143 | a1i 11 |
. . . . . . . . . 10
|
145 | | simpll 790 |
. . . . . . . . . . . 12
|
146 | | snfi 8038 |
. . . . . . . . . . . 12
|
147 | | unfi 8227 |
. . . . . . . . . . . 12
|
148 | 145, 146,
147 | sylancl 694 |
. . . . . . . . . . 11
|
149 | | pwfi 8261 |
. . . . . . . . . . 11
|
150 | 148, 149 | sylib 208 |
. . . . . . . . . 10
|
151 | 55 | a1i 11 |
. . . . . . . . . . . 12
|
152 | | elpwi 4168 |
. . . . . . . . . . . . . 14
|
153 | | ssfi 8180 |
. . . . . . . . . . . . . 14
|
154 | 148, 152,
153 | syl2an 494 |
. . . . . . . . . . . . 13
|
155 | | hashcl 13147 |
. . . . . . . . . . . . 13
|
156 | 154, 155 | syl 17 |
. . . . . . . . . . . 12
|
157 | 151, 156 | expcld 13008 |
. . . . . . . . . . 11
|
158 | | simplr 792 |
. . . . . . . . . . . . . 14
|
159 | | inss1 3833 |
. . . . . . . . . . . . . 14
|
160 | | ssfi 8180 |
. . . . . . . . . . . . . 14
|
161 | 158, 159,
160 | sylancl 694 |
. . . . . . . . . . . . 13
|
162 | | hashcl 13147 |
. . . . . . . . . . . . 13
|
163 | 161, 162 | syl 17 |
. . . . . . . . . . . 12
|
164 | 163 | nn0cnd 11353 |
. . . . . . . . . . 11
|
165 | 157, 164 | mulcld 10060 |
. . . . . . . . . 10
|
166 | 137, 144,
150, 165 | fsumsplit 14471 |
. . . . . . . . 9
|
167 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
168 | 167 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
169 | | inteq 4478 |
. . . . . . . . . . . . . . . 16
|
170 | 27 | intunsn 4516 |
. . . . . . . . . . . . . . . 16
|
171 | 169, 170 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
172 | 171 | ineq2d 3814 |
. . . . . . . . . . . . . 14
|
173 | 172 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
174 | 168, 173 | oveq12d 6668 |
. . . . . . . . . . . 12
|
175 | | pwfi 8261 |
. . . . . . . . . . . . 13
|
176 | 145, 175 | sylib 208 |
. . . . . . . . . . . 12
|
177 | | eqid 2622 |
. . . . . . . . . . . . 13
|
178 | | elpwi 4168 |
. . . . . . . . . . . . . . . . 17
|
179 | 178 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
180 | | unss1 3782 |
. . . . . . . . . . . . . . . 16
|
181 | 179, 180 | syl 17 |
. . . . . . . . . . . . . . 15
|
182 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
183 | | snex 4908 |
. . . . . . . . . . . . . . . . 17
|
184 | 182, 183 | unex 6956 |
. . . . . . . . . . . . . . . 16
|
185 | 184 | elpw 4164 |
. . . . . . . . . . . . . . 15
|
186 | 181, 185 | sylibr 224 |
. . . . . . . . . . . . . 14
|
187 | | simpllr 799 |
. . . . . . . . . . . . . . 15
|
188 | | elpwi 4168 |
. . . . . . . . . . . . . . . 16
|
189 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . 18
|
190 | 27 | snss 4316 |
. . . . . . . . . . . . . . . . . 18
|
191 | 189, 190 | mpbir 221 |
. . . . . . . . . . . . . . . . 17
|
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
193 | | ssel 3597 |
. . . . . . . . . . . . . . . 16
|
194 | 188, 192,
193 | syl2imc 41 |
. . . . . . . . . . . . . . 15
|
195 | 187, 194 | mtod 189 |
. . . . . . . . . . . . . 14
|
196 | 186, 195 | eldifd 3585 |
. . . . . . . . . . . . 13
|
197 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . 18
|
198 | 197 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
199 | 198 | elpwid 4170 |
. . . . . . . . . . . . . . . 16
|
200 | | uncom 3757 |
. . . . . . . . . . . . . . . 16
|
201 | 199, 200 | syl6sseq 3651 |
. . . . . . . . . . . . . . 15
|
202 | | ssundif 4052 |
. . . . . . . . . . . . . . 15
|
203 | 201, 202 | sylib 208 |
. . . . . . . . . . . . . 14
|
204 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
205 | 204 | elpw2 4828 |
. . . . . . . . . . . . . 14
|
206 | 203, 205 | sylibr 224 |
. . . . . . . . . . . . 13
|
207 | | elpwunsn 4224 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 207 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
|
209 | 208 | snssd 4340 |
. . . . . . . . . . . . . . . . 17
|
210 | | ssequn2 3786 |
. . . . . . . . . . . . . . . . 17
|
211 | 209, 210 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
212 | 211 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
|
213 | | uneq1 3760 |
. . . . . . . . . . . . . . . . 17
|
214 | | undif1 4043 |
. . . . . . . . . . . . . . . . 17
|
215 | 213, 214 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
216 | 215 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
217 | 212, 216 | syl5ibrcom 237 |
. . . . . . . . . . . . . 14
|
218 | 178 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
|
219 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
|
220 | 218, 219 | ssneldd 3606 |
. . . . . . . . . . . . . . . . 17
|
221 | | difsnb 4337 |
. . . . . . . . . . . . . . . . 17
|
222 | 220, 221 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
223 | 222 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
|
224 | | difeq1 3721 |
. . . . . . . . . . . . . . . . 17
|
225 | | difun2 4048 |
. . . . . . . . . . . . . . . . 17
|
226 | 224, 225 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
227 | 226 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
228 | 223, 227 | syl5ibrcom 237 |
. . . . . . . . . . . . . 14
|
229 | 217, 228 | impbid 202 |
. . . . . . . . . . . . 13
|
230 | 177, 196,
206, 229 | f1o2d 6887 |
. . . . . . . . . . . 12
|
231 | | uneq1 3760 |
. . . . . . . . . . . . . 14
|
232 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
233 | 232, 183 | unex 6956 |
. . . . . . . . . . . . . 14
|
234 | 231, 177,
233 | fvmpt 6282 |
. . . . . . . . . . . . 13
|
235 | 234 | adantl 482 |
. . . . . . . . . . . 12
|
236 | 197, 165 | sylan2 491 |
. . . . . . . . . . . 12
|
237 | 174, 176,
230, 235, 236 | fsumf1o 14454 |
. . . . . . . . . . 11
|
238 | | uneq1 3760 |
. . . . . . . . . . . . . . . 16
|
239 | 238 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
240 | 239 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
241 | | inteq 4478 |
. . . . . . . . . . . . . . . . 17
|
242 | 241 | ineq1d 3813 |
. . . . . . . . . . . . . . . 16
|
243 | 242 | ineq2d 3814 |
. . . . . . . . . . . . . . 15
|
244 | 243 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
245 | 240, 244 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
246 | 245 | cbvsumv 14426 |
. . . . . . . . . . . 12
|
247 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
248 | | elpwi 4168 |
. . . . . . . . . . . . . . . . . . . 20
|
249 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . 20
|
250 | 145, 248,
249 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
251 | 250, 155 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
252 | 247, 251 | expp1d 13009 |
. . . . . . . . . . . . . . . . 17
|
253 | 248 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
254 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . 20
|
255 | 253, 254 | ssneldd 3606 |
. . . . . . . . . . . . . . . . . . 19
|
256 | | hashunsng 13181 |
. . . . . . . . . . . . . . . . . . . 20
|
257 | 27, 256 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
258 | 250, 255,
257 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
259 | 258 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
260 | 140 | sseli 3599 |
. . . . . . . . . . . . . . . . . . 19
|
261 | 260, 157 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
|
262 | 247, 261 | mulcomd 10061 |
. . . . . . . . . . . . . . . . 17
|
263 | 252, 259,
262 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . 16
|
264 | 261 | mulm1d 10482 |
. . . . . . . . . . . . . . . 16
|
265 | 263, 264 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
266 | 265 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
267 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . 19
|
268 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . 19
|
269 | 158, 267,
268 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
270 | | hashcl 13147 |
. . . . . . . . . . . . . . . . . 18
|
271 | 269, 270 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
272 | 271 | nn0cnd 11353 |
. . . . . . . . . . . . . . . 16
|
273 | 260, 272 | sylan2 491 |
. . . . . . . . . . . . . . 15
|
274 | 261, 273 | mulneg1d 10483 |
. . . . . . . . . . . . . 14
|
275 | 266, 274 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
276 | 275 | sumeq2dv 14433 |
. . . . . . . . . . . 12
|
277 | 246, 276 | syl5eq 2668 |
. . . . . . . . . . 11
|
278 | 157, 272 | mulcld 10060 |
. . . . . . . . . . . . 13
|
279 | 260, 278 | sylan2 491 |
. . . . . . . . . . . 12
|
280 | 176, 279 | fsumneg 14519 |
. . . . . . . . . . 11
|
281 | 237, 277,
280 | 3eqtrd 2660 |
. . . . . . . . . 10
|
282 | 281 | oveq2d 6666 |
. . . . . . . . 9
|
283 | 140 | a1i 11 |
. . . . . . . . . . . . 13
|
284 | 283 | sselda 3603 |
. . . . . . . . . . . 12
|
285 | 284, 165 | syldan 487 |
. . . . . . . . . . 11
|
286 | 176, 285 | fsumcl 14464 |
. . . . . . . . . 10
|
287 | 284, 278 | syldan 487 |
. . . . . . . . . . 11
|
288 | 176, 287 | fsumcl 14464 |
. . . . . . . . . 10
|
289 | 286, 288 | negsubd 10398 |
. . . . . . . . 9
|
290 | 166, 282,
289 | 3eqtrd 2660 |
. . . . . . . 8
|
291 | 290 | adantr 481 |
. . . . . . 7
|
292 | 102, 135,
291 | 3eqtr4d 2666 |
. . . . . 6
|
293 | 292 | ex 450 |
. . . . 5
|
294 | 293 | ralrimdva 2969 |
. . . 4
|
295 | | ineq1 3807 |
. . . . . . . 8
|
296 | 295 | fveq2d 6195 |
. . . . . . 7
|
297 | 67, 296 | oveq12d 6668 |
. . . . . 6
|
298 | | ineq1 3807 |
. . . . . . . . 9
|
299 | 298 | fveq2d 6195 |
. . . . . . . 8
|
300 | 299 | oveq2d 6666 |
. . . . . . 7
|
301 | 300 | sumeq2sdv 14435 |
. . . . . 6
|
302 | 297, 301 | eqeq12d 2637 |
. . . . 5
|
303 | 302 | cbvralv 3171 |
. . . 4
|
304 | 294, 303 | syl6ibr 242 |
. . 3
|
305 | 16, 24, 38, 46, 66, 304 | findcard2s 8201 |
. 2
|
306 | | fveq2 6191 |
. . . . 5
|
307 | | ineq1 3807 |
. . . . . 6
|
308 | 307 | fveq2d 6195 |
. . . . 5
|
309 | 306, 308 | oveq12d 6668 |
. . . 4
|
310 | | simpl 473 |
. . . . . . . 8
|
311 | 310 | ineq1d 3813 |
. . . . . . 7
|
312 | 311 | fveq2d 6195 |
. . . . . 6
|
313 | 312 | oveq2d 6666 |
. . . . 5
|
314 | 313 | sumeq2dv 14433 |
. . . 4
|
315 | 309, 314 | eqeq12d 2637 |
. . 3
|
316 | 315 | rspccva 3308 |
. 2
|
317 | 305, 316 | sylan 488 |
1
|