Step | Hyp | Ref
| Expression |
1 | | tsmssplit.b |
. . 3
|
2 | | tsmssplit.p |
. . 3
|
3 | | tsmssplit.1 |
. . 3
CMnd |
4 | | tsmssplit.2 |
. . 3
TopMnd |
5 | | tsmssplit.a |
. . 3
|
6 | | tsmssplit.f |
. . . . . 6
|
7 | 6 | ffvelrnda 6359 |
. . . . 5
|
8 | | cmnmnd 18208 |
. . . . . . . 8
CMnd |
9 | 3, 8 | syl 17 |
. . . . . . 7
|
10 | | eqid 2622 |
. . . . . . . 8
|
11 | 1, 10 | mndidcl 17308 |
. . . . . . 7
|
12 | 9, 11 | syl 17 |
. . . . . 6
|
13 | 12 | adantr 481 |
. . . . 5
|
14 | 7, 13 | ifcld 4131 |
. . . 4
|
15 | | eqid 2622 |
. . . 4
|
16 | 14, 15 | fmptd 6385 |
. . 3
|
17 | 7, 13 | ifcld 4131 |
. . . 4
|
18 | | eqid 2622 |
. . . 4
|
19 | 17, 18 | fmptd 6385 |
. . 3
|
20 | | tsmssplit.x |
. . . 4
tsums |
21 | 6 | feqmptd 6249 |
. . . . . . . 8
|
22 | 21 | reseq1d 5395 |
. . . . . . 7
|
23 | | ssun1 3776 |
. . . . . . . . 9
|
24 | | tsmssplit.u |
. . . . . . . . 9
|
25 | 23, 24 | syl5sseqr 3654 |
. . . . . . . 8
|
26 | | iftrue 4092 |
. . . . . . . . . 10
|
27 | 26 | mpteq2ia 4740 |
. . . . . . . . 9
|
28 | | resmpt 5449 |
. . . . . . . . 9
|
29 | | resmpt 5449 |
. . . . . . . . 9
|
30 | 27, 28, 29 | 3eqtr4a 2682 |
. . . . . . . 8
|
31 | 25, 30 | syl 17 |
. . . . . . 7
|
32 | 22, 31 | eqtr4d 2659 |
. . . . . 6
|
33 | 32 | oveq2d 6666 |
. . . . 5
tsums tsums |
34 | | tmdtps 21880 |
. . . . . . 7
TopMnd |
35 | 4, 34 | syl 17 |
. . . . . 6
|
36 | | eldifn 3733 |
. . . . . . . . 9
|
37 | 36 | adantl 482 |
. . . . . . . 8
|
38 | 37 | iffalsed 4097 |
. . . . . . 7
|
39 | 38, 5 | suppss2 7329 |
. . . . . 6
supp |
40 | 1, 10, 3, 35, 5, 16, 39 | tsmsres 21947 |
. . . . 5
tsums tsums |
41 | 33, 40 | eqtrd 2656 |
. . . 4
tsums tsums |
42 | 20, 41 | eleqtrd 2703 |
. . 3
tsums |
43 | | tsmssplit.y |
. . . 4
tsums |
44 | 21 | reseq1d 5395 |
. . . . . . 7
|
45 | | ssun2 3777 |
. . . . . . . . 9
|
46 | 45, 24 | syl5sseqr 3654 |
. . . . . . . 8
|
47 | | iftrue 4092 |
. . . . . . . . . 10
|
48 | 47 | mpteq2ia 4740 |
. . . . . . . . 9
|
49 | | resmpt 5449 |
. . . . . . . . 9
|
50 | | resmpt 5449 |
. . . . . . . . 9
|
51 | 48, 49, 50 | 3eqtr4a 2682 |
. . . . . . . 8
|
52 | 46, 51 | syl 17 |
. . . . . . 7
|
53 | 44, 52 | eqtr4d 2659 |
. . . . . 6
|
54 | 53 | oveq2d 6666 |
. . . . 5
tsums tsums |
55 | | eldifn 3733 |
. . . . . . . . 9
|
56 | 55 | adantl 482 |
. . . . . . . 8
|
57 | 56 | iffalsed 4097 |
. . . . . . 7
|
58 | 57, 5 | suppss2 7329 |
. . . . . 6
supp |
59 | 1, 10, 3, 35, 5, 19, 58 | tsmsres 21947 |
. . . . 5
tsums tsums |
60 | 54, 59 | eqtrd 2656 |
. . . 4
tsums tsums |
61 | 43, 60 | eleqtrd 2703 |
. . 3
tsums |
62 | 1, 2, 3, 4, 5, 16,
19, 42, 61 | tsmsadd 21950 |
. 2
tsums |
63 | 26 | adantl 482 |
. . . . . . . . 9
|
64 | | tsmssplit.i |
. . . . . . . . . . . . . . 15
|
65 | | noel 3919 |
. . . . . . . . . . . . . . . 16
|
66 | | eleq2 2690 |
. . . . . . . . . . . . . . . 16
|
67 | 65, 66 | mtbiri 317 |
. . . . . . . . . . . . . . 15
|
68 | 64, 67 | syl 17 |
. . . . . . . . . . . . . 14
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . 13
|
70 | | elin 3796 |
. . . . . . . . . . . . 13
|
71 | 69, 70 | sylnib 318 |
. . . . . . . . . . . 12
|
72 | | imnan 438 |
. . . . . . . . . . . 12
|
73 | 71, 72 | sylibr 224 |
. . . . . . . . . . 11
|
74 | 73 | imp 445 |
. . . . . . . . . 10
|
75 | 74 | iffalsed 4097 |
. . . . . . . . 9
|
76 | 63, 75 | oveq12d 6668 |
. . . . . . . 8
|
77 | 1, 2, 10 | mndrid 17312 |
. . . . . . . . . . 11
|
78 | 9, 77 | sylan 488 |
. . . . . . . . . 10
|
79 | 7, 78 | syldan 487 |
. . . . . . . . 9
|
80 | 79 | adantr 481 |
. . . . . . . 8
|
81 | 76, 80 | eqtrd 2656 |
. . . . . . 7
|
82 | 73 | con2d 129 |
. . . . . . . . . . 11
|
83 | 82 | imp 445 |
. . . . . . . . . 10
|
84 | 83 | iffalsed 4097 |
. . . . . . . . 9
|
85 | 47 | adantl 482 |
. . . . . . . . 9
|
86 | 84, 85 | oveq12d 6668 |
. . . . . . . 8
|
87 | 1, 2, 10 | mndlid 17311 |
. . . . . . . . . . 11
|
88 | 9, 87 | sylan 488 |
. . . . . . . . . 10
|
89 | 7, 88 | syldan 487 |
. . . . . . . . 9
|
90 | 89 | adantr 481 |
. . . . . . . 8
|
91 | 86, 90 | eqtrd 2656 |
. . . . . . 7
|
92 | 24 | eleq2d 2687 |
. . . . . . . . 9
|
93 | | elun 3753 |
. . . . . . . . 9
|
94 | 92, 93 | syl6bb 276 |
. . . . . . . 8
|
95 | 94 | biimpa 501 |
. . . . . . 7
|
96 | 81, 91, 95 | mpjaodan 827 |
. . . . . 6
|
97 | 96 | mpteq2dva 4744 |
. . . . 5
|
98 | 21, 97 | eqtr4d 2659 |
. . . 4
|
99 | | eqidd 2623 |
. . . . 5
|
100 | | eqidd 2623 |
. . . . 5
|
101 | 5, 14, 17, 99, 100 | offval2 6914 |
. . . 4
|
102 | 98, 101 | eqtr4d 2659 |
. . 3
|
103 | 102 | oveq2d 6666 |
. 2
tsums tsums |
104 | 62, 103 | eleqtrrd 2704 |
1
tsums |