Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . . . . . . . . . . 12
|
2 | | sspwb 4917 |
. . . . . . . . . . . 12
|
3 | 1, 2 | mpbi 220 |
. . . . . . . . . . 11
|
4 | | ssrin 3838 |
. . . . . . . . . . 11
|
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . 10
|
6 | | simpr 477 |
. . . . . . . . . 10
|
7 | 5, 6 | sseldi 3601 |
. . . . . . . . 9
|
8 | | elfpw 8268 |
. . . . . . . . . . . . . . . 16
|
9 | 8 | simplbi 476 |
. . . . . . . . . . . . . . 15
|
10 | 9 | adantl 482 |
. . . . . . . . . . . . . 14
|
11 | | ssrin 3838 |
. . . . . . . . . . . . . 14
|
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
|
13 | 8 | simprbi 480 |
. . . . . . . . . . . . . . 15
|
14 | 13 | adantl 482 |
. . . . . . . . . . . . . 14
|
15 | | inss1 3833 |
. . . . . . . . . . . . . 14
|
16 | | ssfi 8180 |
. . . . . . . . . . . . . 14
|
17 | 14, 15, 16 | sylancl 694 |
. . . . . . . . . . . . 13
|
18 | | elfpw 8268 |
. . . . . . . . . . . . 13
|
19 | 12, 17, 18 | sylanbrc 698 |
. . . . . . . . . . . 12
|
20 | | sseq2 3627 |
. . . . . . . . . . . . . . 15
|
21 | | ssin 3835 |
. . . . . . . . . . . . . . 15
|
22 | 20, 21 | syl6bbr 278 |
. . . . . . . . . . . . . 14
|
23 | | reseq2 5391 |
. . . . . . . . . . . . . . . . 17
|
24 | | inss2 3834 |
. . . . . . . . . . . . . . . . . 18
|
25 | | resabs1 5427 |
. . . . . . . . . . . . . . . . . 18
|
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
27 | 23, 26 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
28 | 27 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
g g
|
29 | 28 | eleq1d 2686 |
. . . . . . . . . . . . . 14
g g
|
30 | 22, 29 | imbi12d 334 |
. . . . . . . . . . . . 13
g g
|
31 | 30 | rspcv 3305 |
. . . . . . . . . . . 12
g
g
|
32 | 19, 31 | syl 17 |
. . . . . . . . . . 11
g
g
|
33 | | elfpw 8268 |
. . . . . . . . . . . . . . . 16
|
34 | 33 | simplbi 476 |
. . . . . . . . . . . . . . 15
|
35 | 34 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
36 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
37 | 35, 36 | syl6ss 3615 |
. . . . . . . . . . . . 13
|
38 | 37 | biantrud 528 |
. . . . . . . . . . . 12
|
39 | | resres 5409 |
. . . . . . . . . . . . . . 15
|
40 | 39 | oveq2i 6661 |
. . . . . . . . . . . . . 14
g g
|
41 | | tsmsres.b |
. . . . . . . . . . . . . . 15
|
42 | | tsmsres.z |
. . . . . . . . . . . . . . 15
|
43 | | tsmsres.1 |
. . . . . . . . . . . . . . . 16
CMnd |
44 | 43 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
CMnd |
45 | | tsmsres.f |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
47 | 46, 10 | fssresd 6071 |
. . . . . . . . . . . . . . 15
|
48 | | tsmsres.a |
. . . . . . . . . . . . . . . . . . 19
|
49 | | fex 6490 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 45, 48, 49 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
51 | 50 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
52 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
|
53 | 42, 52 | eqeltri 2697 |
. . . . . . . . . . . . . . . . 17
|
54 | | ressuppss 7314 |
. . . . . . . . . . . . . . . . 17
supp
supp |
55 | 51, 53, 54 | sylancl 694 |
. . . . . . . . . . . . . . . 16
supp supp |
56 | | tsmsres.s |
. . . . . . . . . . . . . . . . 17
supp |
57 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
supp |
58 | 55, 57 | sstrd 3613 |
. . . . . . . . . . . . . . 15
supp |
59 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
60 | 47, 14, 59 | fdmfifsupp 8285 |
. . . . . . . . . . . . . . 15
finSupp |
61 | 41, 42, 44, 14, 47, 58, 60 | gsumres 18314 |
. . . . . . . . . . . . . 14
g
g |
62 | 40, 61 | syl5reqr 2671 |
. . . . . . . . . . . . 13
g g
|
63 | 62 | eleq1d 2686 |
. . . . . . . . . . . 12
g
g
|
64 | 38, 63 | imbi12d 334 |
. . . . . . . . . . 11
g g
|
65 | 32, 64 | sylibrd 249 |
. . . . . . . . . 10
g
g
|
66 | 65 | ralrimdva 2969 |
. . . . . . . . 9
g
g |
67 | | sseq1 3626 |
. . . . . . . . . . . 12
|
68 | 67 | imbi1d 331 |
. . . . . . . . . . 11
g g |
69 | 68 | ralbidv 2986 |
. . . . . . . . . 10
g g |
70 | 69 | rspcev 3309 |
. . . . . . . . 9
g
g |
71 | 7, 66, 70 | syl6an 568 |
. . . . . . . 8
g
g |
72 | 71 | rexlimdva 3031 |
. . . . . . 7
g
g |
73 | | elfpw 8268 |
. . . . . . . . . . . . 13
|
74 | 73 | simplbi 476 |
. . . . . . . . . . . 12
|
75 | 74 | adantl 482 |
. . . . . . . . . . 11
|
76 | | ssrin 3838 |
. . . . . . . . . . 11
|
77 | 75, 76 | syl 17 |
. . . . . . . . . 10
|
78 | 73 | simprbi 480 |
. . . . . . . . . . . 12
|
79 | 78 | adantl 482 |
. . . . . . . . . . 11
|
80 | | inss1 3833 |
. . . . . . . . . . 11
|
81 | | ssfi 8180 |
. . . . . . . . . . 11
|
82 | 79, 80, 81 | sylancl 694 |
. . . . . . . . . 10
|
83 | | elfpw 8268 |
. . . . . . . . . 10
|
84 | 77, 82, 83 | sylanbrc 698 |
. . . . . . . . 9
|
85 | 74 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
86 | | elfpw 8268 |
. . . . . . . . . . . . . . . . 17
|
87 | 86 | simplbi 476 |
. . . . . . . . . . . . . . . 16
|
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . 15
|
89 | 88, 1 | syl6ss 3615 |
. . . . . . . . . . . . . 14
|
90 | 85, 89 | unssd 3789 |
. . . . . . . . . . . . 13
|
91 | 86 | simprbi 480 |
. . . . . . . . . . . . . 14
|
92 | | unfi 8227 |
. . . . . . . . . . . . . 14
|
93 | 79, 91, 92 | syl2an 494 |
. . . . . . . . . . . . 13
|
94 | | elfpw 8268 |
. . . . . . . . . . . . 13
|
95 | 90, 93, 94 | sylanbrc 698 |
. . . . . . . . . . . 12
|
96 | | ssun1 3776 |
. . . . . . . . . . . . . . . 16
|
97 | | id 22 |
. . . . . . . . . . . . . . . 16
|
98 | 96, 97 | syl5sseqr 3654 |
. . . . . . . . . . . . . . 15
|
99 | | pm5.5 351 |
. . . . . . . . . . . . . . 15
g g |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . 14
g g |
101 | | reseq2 5391 |
. . . . . . . . . . . . . . . 16
|
102 | 101 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
g g |
103 | 102 | eleq1d 2686 |
. . . . . . . . . . . . . 14
g g |
104 | 100, 103 | bitrd 268 |
. . . . . . . . . . . . 13
g g |
105 | 104 | rspcv 3305 |
. . . . . . . . . . . 12
g
g
|
106 | 95, 105 | syl 17 |
. . . . . . . . . . 11
g g |
107 | 43 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
CMnd |
108 | 93 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
|
109 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
110 | 90 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
|
111 | 109, 110 | fssresd 6071 |
. . . . . . . . . . . . . . . . 17
|
112 | 50, 53 | jctir 561 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 112 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
114 | | ressuppss 7314 |
. . . . . . . . . . . . . . . . . . 19
supp supp |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . 18
supp supp |
116 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
supp
|
117 | 115, 116 | sstrd 3613 |
. . . . . . . . . . . . . . . . 17
supp |
118 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
119 | 111, 108,
118 | fdmfifsupp 8285 |
. . . . . . . . . . . . . . . . 17
finSupp
|
120 | 41, 42, 107, 108, 111, 117, 119 | gsumres 18314 |
. . . . . . . . . . . . . . . 16
g
g
|
121 | | resres 5409 |
. . . . . . . . . . . . . . . . . . 19
|
122 | | indir 3875 |
. . . . . . . . . . . . . . . . . . . . 21
|
123 | 88, 36 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
124 | 123 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
125 | | df-ss 3588 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
126 | 124, 125 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
127 | 126 | uneq2d 3767 |
. . . . . . . . . . . . . . . . . . . . . 22
|
128 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
129 | | ssequn1 3783 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
130 | 128, 129 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . 22
|
131 | 127, 130 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
132 | 122, 131 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . 20
|
133 | 132 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . 19
|
134 | 121, 133 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
|
135 | 124 | resabs1d 5428 |
. . . . . . . . . . . . . . . . . 18
|
136 | 134, 135 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
|
137 | 136 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
g
g |
138 | 120, 137 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
g
g
|
139 | 138 | eleq1d 2686 |
. . . . . . . . . . . . . 14
g g |
140 | 139 | biimpd 219 |
. . . . . . . . . . . . 13
g g |
141 | 140 | expr 643 |
. . . . . . . . . . . 12
g
g |
142 | 141 | com23 86 |
. . . . . . . . . . 11
g
g |
143 | 106, 142 | syld 47 |
. . . . . . . . . 10
g
g |
144 | 143 | ralrimdva 2969 |
. . . . . . . . 9
g
g |
145 | | sseq1 3626 |
. . . . . . . . . . . 12
|
146 | 145 | imbi1d 331 |
. . . . . . . . . . 11
g g
|
147 | 146 | ralbidv 2986 |
. . . . . . . . . 10
g g |
148 | 147 | rspcev 3309 |
. . . . . . . . 9
g g |
149 | 84, 144, 148 | syl6an 568 |
. . . . . . . 8
g
g |
150 | 149 | rexlimdva 3031 |
. . . . . . 7
g g |
151 | 72, 150 | impbid 202 |
. . . . . 6
g g |
152 | 151 | imbi2d 330 |
. . . . 5
g
g |
153 | 152 | ralbidv 2986 |
. . . 4
g
g |
154 | 153 | anbi2d 740 |
. . 3
g
g |
155 | | eqid 2622 |
. . . 4
|
156 | | eqid 2622 |
. . . 4
|
157 | | tsmsres.2 |
. . . 4
|
158 | | inex1g 4801 |
. . . . 5
|
159 | 48, 158 | syl 17 |
. . . 4
|
160 | | fssres 6070 |
. . . . . 6
|
161 | 45, 1, 160 | sylancl 694 |
. . . . 5
|
162 | | resres 5409 |
. . . . . . 7
|
163 | | ffn 6045 |
. . . . . . . . 9
|
164 | | fnresdm 6000 |
. . . . . . . . 9
|
165 | 45, 163, 164 | 3syl 18 |
. . . . . . . 8
|
166 | 165 | reseq1d 5395 |
. . . . . . 7
|
167 | 162, 166 | syl5eqr 2670 |
. . . . . 6
|
168 | 167 | feq1d 6030 |
. . . . 5
|
169 | 161, 168 | mpbid 222 |
. . . 4
|
170 | 41, 155, 156, 43, 157, 159, 169 | eltsms 21936 |
. . 3
tsums
g |
171 | | eqid 2622 |
. . . 4
|
172 | 41, 155, 171, 43, 157, 48, 45 | eltsms 21936 |
. . 3
tsums
g |
173 | 154, 170,
172 | 3bitr4d 300 |
. 2
tsums
tsums |
174 | 173 | eqrdv 2620 |
1
tsums tsums |