Step | Hyp | Ref
| Expression |
1 | | ssid 3624 |
. 2
|
2 | | itgfsum.2 |
. . 3
|
3 | | sseq1 3626 |
. . . . . 6
|
4 | | sumeq1 14419 |
. . . . . . . . . . . 12
|
5 | | sum0 14452 |
. . . . . . . . . . . 12
|
6 | 4, 5 | syl6eq 2672 |
. . . . . . . . . . 11
|
7 | 6 | mpteq2dv 4745 |
. . . . . . . . . 10
|
8 | | fconstmpt 5163 |
. . . . . . . . . 10
|
9 | 7, 8 | syl6eqr 2674 |
. . . . . . . . 9
|
10 | 9 | eleq1d 2686 |
. . . . . . . 8
|
11 | 10 | anbi1d 741 |
. . . . . . 7
|
12 | | itgz 23547 |
. . . . . . . . 9
|
13 | 6 | adantr 481 |
. . . . . . . . . 10
|
14 | 13 | itgeq2dv 23548 |
. . . . . . . . 9
|
15 | | sumeq1 14419 |
. . . . . . . . . 10
|
16 | | sum0 14452 |
. . . . . . . . . 10
|
17 | 15, 16 | syl6eq 2672 |
. . . . . . . . 9
|
18 | 12, 14, 17 | 3eqtr4a 2682 |
. . . . . . . 8
|
19 | 18 | biantrud 528 |
. . . . . . 7
|
20 | 11, 19 | bitr4d 271 |
. . . . . 6
|
21 | 3, 20 | imbi12d 334 |
. . . . 5
|
22 | 21 | imbi2d 330 |
. . . 4
|
23 | | sseq1 3626 |
. . . . . 6
|
24 | | sumeq1 14419 |
. . . . . . . . 9
|
25 | 24 | mpteq2dv 4745 |
. . . . . . . 8
|
26 | 25 | eleq1d 2686 |
. . . . . . 7
|
27 | 24 | adantr 481 |
. . . . . . . . 9
|
28 | 27 | itgeq2dv 23548 |
. . . . . . . 8
|
29 | | sumeq1 14419 |
. . . . . . . 8
|
30 | 28, 29 | eqeq12d 2637 |
. . . . . . 7
|
31 | 26, 30 | anbi12d 747 |
. . . . . 6
|
32 | 23, 31 | imbi12d 334 |
. . . . 5
|
33 | 32 | imbi2d 330 |
. . . 4
|
34 | | sseq1 3626 |
. . . . . 6
|
35 | | sumeq1 14419 |
. . . . . . . . 9
|
36 | 35 | mpteq2dv 4745 |
. . . . . . . 8
|
37 | 36 | eleq1d 2686 |
. . . . . . 7
|
38 | 35 | adantr 481 |
. . . . . . . . 9
|
39 | 38 | itgeq2dv 23548 |
. . . . . . . 8
|
40 | | sumeq1 14419 |
. . . . . . . 8
|
41 | 39, 40 | eqeq12d 2637 |
. . . . . . 7
|
42 | 37, 41 | anbi12d 747 |
. . . . . 6
|
43 | 34, 42 | imbi12d 334 |
. . . . 5
|
44 | 43 | imbi2d 330 |
. . . 4
|
45 | | sseq1 3626 |
. . . . . 6
|
46 | | sumeq1 14419 |
. . . . . . . . 9
|
47 | 46 | mpteq2dv 4745 |
. . . . . . . 8
|
48 | 47 | eleq1d 2686 |
. . . . . . 7
|
49 | 46 | adantr 481 |
. . . . . . . . 9
|
50 | 49 | itgeq2dv 23548 |
. . . . . . . 8
|
51 | | sumeq1 14419 |
. . . . . . . 8
|
52 | 50, 51 | eqeq12d 2637 |
. . . . . . 7
|
53 | 48, 52 | anbi12d 747 |
. . . . . 6
|
54 | 45, 53 | imbi12d 334 |
. . . . 5
|
55 | 54 | imbi2d 330 |
. . . 4
|
56 | | itgfsum.1 |
. . . . . 6
|
57 | | ibl0 23553 |
. . . . . 6
|
58 | 56, 57 | syl 17 |
. . . . 5
|
59 | 58 | a1d 25 |
. . . 4
|
60 | | ssun1 3776 |
. . . . . . . . . 10
|
61 | | sstr 3611 |
. . . . . . . . . 10
|
62 | 60, 61 | mpan 706 |
. . . . . . . . 9
|
63 | 62 | imim1i 63 |
. . . . . . . 8
|
64 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
65 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
66 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
67 | 64, 65, 66 | cbvsumi 14427 |
. . . . . . . . . . . . . . . . 17
|
68 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
|
69 | | disjsn 4246 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | 68, 69 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
72 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . 21
|
76 | 73, 74, 75 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
78 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | 78 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
|
80 | | itgfsum.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
81 | | iblmbf 23534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
MblFn |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
MblFn |
83 | | itgfsum.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
84 | 83 | anass1rs 849 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
85 | 82, 84 | mbfmptcl 23404 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
86 | 85 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
87 | 86 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
88 | 87 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . 22
|
89 | 64 | nfel1 2779 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
90 | 65 | nfel1 2779 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
91 | 66 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
92 | 89, 90, 91 | cbvral 3167 |
. . . . . . . . . . . . . . . . . . . . . 22
|
93 | 88, 92 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
|
94 | 93 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | 79, 94 | syldan 487 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 71, 72, 77, 95 | fsumsplit 14471 |
. . . . . . . . . . . . . . . . . 18
|
97 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 74 | unssbd 3791 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
99 | 97 | snss 4316 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 98, 99 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | 100 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | | csbeq1 3536 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
103 | 102 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | 103 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 101, 93, 104 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | 102 | sumsn 14475 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | 97, 105, 106 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
|
108 | 107 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
109 | 96, 108 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
110 | 67, 109 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
|
111 | 110 | mpteq2dva 4744 |
. . . . . . . . . . . . . . 15
|
112 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
113 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . 17
|
114 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
115 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . 17
|
116 | 113, 114,
115 | nfov 6676 |
. . . . . . . . . . . . . . . 16
|
117 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . 17
|
118 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . 17
|
119 | 117, 118 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
120 | 112, 116,
119 | cbvmpt 4749 |
. . . . . . . . . . . . . . 15
|
121 | 111, 120 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
122 | 121 | adantr 481 |
. . . . . . . . . . . . 13
|
123 | | sumex 14418 |
. . . . . . . . . . . . . . . 16
|
124 | 123 | csbex 4793 |
. . . . . . . . . . . . . . 15
|
125 | 124 | a1i 11 |
. . . . . . . . . . . . . 14
|
126 | 64, 65, 66 | cbvsumi 14427 |
. . . . . . . . . . . . . . . . 17
|
127 | 126 | mpteq2i 4741 |
. . . . . . . . . . . . . . . 16
|
128 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
129 | 128, 113,
117 | cbvmpt 4749 |
. . . . . . . . . . . . . . . 16
|
130 | 127, 129 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
131 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
132 | 130, 131 | syl5eqelr 2706 |
. . . . . . . . . . . . . 14
|
133 | | elex 3212 |
. . . . . . . . . . . . . . . . . . 19
|
134 | 105, 133 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
135 | 134 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
|
136 | 135 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
137 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
|
138 | 115 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
|
139 | 118 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
140 | 137, 138,
139 | cbvral 3167 |
. . . . . . . . . . . . . . . 16
|
141 | 136, 140 | sylib 208 |
. . . . . . . . . . . . . . 15
|
142 | 141 | r19.21bi 2932 |
. . . . . . . . . . . . . 14
|
143 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
144 | 143, 115,
118 | cbvmpt 4749 |
. . . . . . . . . . . . . . . 16
|
145 | 80 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . 19
|
146 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
|
147 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . 22
|
148 | 147, 65 | nfmpt 4746 |
. . . . . . . . . . . . . . . . . . . . 21
|
149 | 148 | nfel1 2779 |
. . . . . . . . . . . . . . . . . . . 20
|
150 | 66 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . 21
|
151 | 150 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
|
152 | 146, 149,
151 | cbvral 3167 |
. . . . . . . . . . . . . . . . . . 19
|
153 | 145, 152 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
|
154 | 153 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
155 | 102 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . 19
|
156 | 155 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
|
157 | 156 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
|
158 | 100, 154,
157 | sylc 65 |
. . . . . . . . . . . . . . . 16
|
159 | 144, 158 | syl5eqelr 2706 |
. . . . . . . . . . . . . . 15
|
160 | 159 | adantr 481 |
. . . . . . . . . . . . . 14
|
161 | 125, 132,
142, 160 | ibladd 23587 |
. . . . . . . . . . . . 13
|
162 | 122, 161 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
163 | 125, 132,
142, 160 | itgadd 23591 |
. . . . . . . . . . . . . . 15
|
164 | 119, 112,
116 | cbvitg 23542 |
. . . . . . . . . . . . . . 15
|
165 | 117, 128,
113 | cbvitg 23542 |
. . . . . . . . . . . . . . . 16
|
166 | 118, 143,
115 | cbvitg 23542 |
. . . . . . . . . . . . . . . 16
|
167 | 165, 166 | oveq12i 6662 |
. . . . . . . . . . . . . . 15
|
168 | 163, 164,
167 | 3eqtr4g 2681 |
. . . . . . . . . . . . . 14
|
169 | 109 | itgeq2dv 23548 |
. . . . . . . . . . . . . . 15
|
170 | 169 | adantr 481 |
. . . . . . . . . . . . . 14
|
171 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
|
172 | 74 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
|
173 | 94 | an32s 846 |
. . . . . . . . . . . . . . . . . . 19
|
174 | 154 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . 19
|
175 | 173, 174 | itgcl 23550 |
. . . . . . . . . . . . . . . . . 18
|
176 | 172, 175 | syldan 487 |
. . . . . . . . . . . . . . . . 17
|
177 | 70, 171, 76, 176 | fsumsplit 14471 |
. . . . . . . . . . . . . . . 16
|
178 | 177 | adantr 481 |
. . . . . . . . . . . . . . 15
|
179 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
|
180 | | itgeq2 23544 |
. . . . . . . . . . . . . . . . . 18
|
181 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
182 | 180, 181 | mprg 2926 |
. . . . . . . . . . . . . . . . 17
|
183 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
184 | 147, 65 | nfitg 23541 |
. . . . . . . . . . . . . . . . . 18
|
185 | 66 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
186 | 185 | itgeq2dv 23548 |
. . . . . . . . . . . . . . . . . 18
|
187 | 183, 184,
186 | cbvsumi 14427 |
. . . . . . . . . . . . . . . . 17
|
188 | 179, 182,
187 | 3eqtr3g 2679 |
. . . . . . . . . . . . . . . 16
|
189 | 105, 158 | itgcl 23550 |
. . . . . . . . . . . . . . . . . . 19
|
190 | 189 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
191 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
192 | 191 | itgeq2dv 23548 |
. . . . . . . . . . . . . . . . . . 19
|
193 | 192 | sumsn 14475 |
. . . . . . . . . . . . . . . . . 18
|
194 | 97, 190, 193 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
195 | 194 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
|
196 | 188, 195 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
197 | 178, 196 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
198 | 168, 170,
197 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
|
199 | | itgeq2 23544 |
. . . . . . . . . . . . . 14
|
200 | 67 | a1i 11 |
. . . . . . . . . . . . . 14
|
201 | 199, 200 | mprg 2926 |
. . . . . . . . . . . . 13
|
202 | 183, 184,
186 | cbvsumi 14427 |
. . . . . . . . . . . . 13
|
203 | 198, 201,
202 | 3eqtr4g 2681 |
. . . . . . . . . . . 12
|
204 | 162, 203 | jca 554 |
. . . . . . . . . . 11
|
205 | 204 | ex 450 |
. . . . . . . . . 10
|
206 | 205 | expr 643 |
. . . . . . . . 9
|
207 | 206 | a2d 29 |
. . . . . . . 8
|
208 | 63, 207 | syl5 34 |
. . . . . . 7
|
209 | 208 | expcom 451 |
. . . . . 6
|
210 | 209 | adantl 482 |
. . . . 5
|
211 | 210 | a2d 29 |
. . . 4
|
212 | 22, 33, 44, 55, 59, 211 | findcard2s 8201 |
. . 3
|
213 | 2, 212 | mpcom 38 |
. 2
|
214 | 1, 213 | mpi 20 |
1
|