Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
|
2 | | hash0 13158 |
. . . . 5
|
3 | 1, 2 | syl6eq 2672 |
. . . 4
|
4 | 3 | breq2d 4665 |
. . 3
|
5 | | sumeq1 14419 |
. . . . 5
|
6 | | sum0 14452 |
. . . . 5
|
7 | 5, 6 | syl6eq 2672 |
. . . 4
|
8 | 7 | breq2d 4665 |
. . 3
|
9 | 4, 8 | bibi12d 335 |
. 2
|
10 | | fveq2 6191 |
. . . 4
|
11 | 10 | breq2d 4665 |
. . 3
|
12 | | sumeq1 14419 |
. . . 4
|
13 | 12 | breq2d 4665 |
. . 3
|
14 | 11, 13 | bibi12d 335 |
. 2
|
15 | | fveq2 6191 |
. . . 4
|
16 | 15 | breq2d 4665 |
. . 3
|
17 | | sumeq1 14419 |
. . . 4
|
18 | 17 | breq2d 4665 |
. . 3
|
19 | 16, 18 | bibi12d 335 |
. 2
|
20 | | fveq2 6191 |
. . . 4
|
21 | 20 | breq2d 4665 |
. . 3
|
22 | | sumeq1 14419 |
. . . 4
|
23 | 22 | breq2d 4665 |
. . 3
|
24 | 21, 23 | bibi12d 335 |
. 2
|
25 | | biidd 252 |
. 2
|
26 | | eldifi 3732 |
. . . . . . . . . . . . . 14
|
27 | 26 | adantl 482 |
. . . . . . . . . . . . 13
|
28 | 27 | adantl 482 |
. . . . . . . . . . . 12
|
29 | | sumeven.b |
. . . . . . . . . . . . . 14
|
30 | 29 | adantlr 751 |
. . . . . . . . . . . . 13
|
31 | 30 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
32 | | rspcsbela 4006 |
. . . . . . . . . . . 12
|
33 | 28, 31, 32 | syl2anc 693 |
. . . . . . . . . . 11
|
34 | | sumodd.o |
. . . . . . . . . . . . . . 15
|
35 | 34 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
|
36 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
37 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
38 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
39 | 36, 37, 38 | nfbr 4699 |
. . . . . . . . . . . . . . . . 17
|
40 | 39 | nfn 1784 |
. . . . . . . . . . . . . . . 16
|
41 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
42 | 41 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | notbid 308 |
. . . . . . . . . . . . . . . 16
|
44 | 40, 43 | rspc 3303 |
. . . . . . . . . . . . . . 15
|
45 | 26, 44 | syl 17 |
. . . . . . . . . . . . . 14
|
46 | 35, 45 | syl5com 31 |
. . . . . . . . . . . . 13
|
47 | 46 | a1d 25 |
. . . . . . . . . . . 12
|
48 | 47 | imp32 449 |
. . . . . . . . . . 11
|
49 | 33, 48 | jca 554 |
. . . . . . . . . 10
|
50 | 49 | adantr 481 |
. . . . . . . . 9
|
51 | | sumeven.a |
. . . . . . . . . . . . 13
|
52 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
|
53 | 52 | expcom 451 |
. . . . . . . . . . . . . 14
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . 13
|
55 | 51, 54 | syl5com 31 |
. . . . . . . . . . . 12
|
56 | 55 | imp 445 |
. . . . . . . . . . 11
|
57 | | simpll 790 |
. . . . . . . . . . . 12
|
58 | | ssel 3597 |
. . . . . . . . . . . . . . 15
|
59 | 58 | adantr 481 |
. . . . . . . . . . . . . 14
|
60 | 59 | adantl 482 |
. . . . . . . . . . . . 13
|
61 | 60 | imp 445 |
. . . . . . . . . . . 12
|
62 | 57, 61, 29 | syl2anc 693 |
. . . . . . . . . . 11
|
63 | 56, 62 | fsumzcl 14466 |
. . . . . . . . . 10
|
64 | 63 | anim1i 592 |
. . . . . . . . 9
|
65 | | opeo 15089 |
. . . . . . . . 9
|
66 | 50, 64, 65 | syl2anc 693 |
. . . . . . . 8
|
67 | 63 | zcnd 11483 |
. . . . . . . . . 10
|
68 | 33 | zcnd 11483 |
. . . . . . . . . 10
|
69 | | addcom 10222 |
. . . . . . . . . . . 12
|
70 | 69 | breq2d 4665 |
. . . . . . . . . . 11
|
71 | 70 | notbid 308 |
. . . . . . . . . 10
|
72 | 67, 68, 71 | syl2anc 693 |
. . . . . . . . 9
|
73 | 72 | adantr 481 |
. . . . . . . 8
|
74 | 66, 73 | mpbird 247 |
. . . . . . 7
|
75 | 74 | ex 450 |
. . . . . 6
|
76 | 63 | anim1i 592 |
. . . . . . . . 9
|
77 | 49 | adantr 481 |
. . . . . . . . 9
|
78 | | opoe 15087 |
. . . . . . . . 9
|
79 | 76, 77, 78 | syl2anc 693 |
. . . . . . . 8
|
80 | 79 | ex 450 |
. . . . . . 7
|
81 | 80 | con1d 139 |
. . . . . 6
|
82 | 75, 81 | impbid 202 |
. . . . 5
|
83 | | bitr3 342 |
. . . . 5
|
84 | 82, 83 | syl 17 |
. . . 4
|
85 | | bicom 212 |
. . . 4
|
86 | | bicom 212 |
. . . 4
|
87 | 84, 85, 86 | 3imtr4g 285 |
. . 3
|
88 | | notnotb 304 |
. . . . 5
|
89 | | hashcl 13147 |
. . . . . . . . 9
|
90 | 56, 89 | syl 17 |
. . . . . . . 8
|
91 | 90 | nn0zd 11480 |
. . . . . . 7
|
92 | | oddp1even 15068 |
. . . . . . 7
|
93 | 91, 92 | syl 17 |
. . . . . 6
|
94 | 93 | notbid 308 |
. . . . 5
|
95 | 88, 94 | syl5bb 272 |
. . . 4
|
96 | 95 | bibi1d 333 |
. . 3
|
97 | | simprr 796 |
. . . . . . 7
|
98 | | eldifn 3733 |
. . . . . . . . . 10
|
99 | 98 | adantl 482 |
. . . . . . . . 9
|
100 | 99 | adantl 482 |
. . . . . . . 8
|
101 | 56, 100 | jca 554 |
. . . . . . 7
|
102 | | hashunsng 13181 |
. . . . . . 7
|
103 | 97, 101, 102 | sylc 65 |
. . . . . 6
|
104 | 103 | breq2d 4665 |
. . . . 5
|
105 | | vex 3203 |
. . . . . . . 8
|
106 | 105 | a1i 11 |
. . . . . . 7
|
107 | | df-nel 2898 |
. . . . . . . 8
|
108 | 100, 107 | sylibr 224 |
. . . . . . 7
|
109 | | simpll 790 |
. . . . . . . . 9
|
110 | | elun 3753 |
. . . . . . . . . . . . 13
|
111 | 59 | com12 32 |
. . . . . . . . . . . . . 14
|
112 | | elsni 4194 |
. . . . . . . . . . . . . . 15
|
113 | | eleq1w 2684 |
. . . . . . . . . . . . . . . 16
|
114 | 27, 113 | syl5ibr 236 |
. . . . . . . . . . . . . . 15
|
115 | 112, 114 | syl 17 |
. . . . . . . . . . . . . 14
|
116 | 111, 115 | jaoi 394 |
. . . . . . . . . . . . 13
|
117 | 110, 116 | sylbi 207 |
. . . . . . . . . . . 12
|
118 | 117 | com12 32 |
. . . . . . . . . . 11
|
119 | 118 | adantl 482 |
. . . . . . . . . 10
|
120 | 119 | imp 445 |
. . . . . . . . 9
|
121 | 109, 120,
29 | syl2anc 693 |
. . . . . . . 8
|
122 | 121 | ralrimiva 2966 |
. . . . . . 7
|
123 | | fsumsplitsnun 14484 |
. . . . . . 7
|
124 | 56, 106, 108, 122, 123 | syl121anc 1331 |
. . . . . 6
|
125 | 124 | breq2d 4665 |
. . . . 5
|
126 | 104, 125 | bibi12d 335 |
. . . 4
|
127 | | notbi 309 |
. . . 4
|
128 | 126, 127 | syl6bb 276 |
. . 3
|
129 | 87, 96, 128 | 3imtr4d 283 |
. 2
|
130 | 9, 14, 19, 24, 25, 129, 51 | findcard2d 8202 |
1
|