Step |
Hyp |
Ref |
Expression |
1 |
|
lcdlss.h |
|
2 |
|
lcdlss.o |
|
3 |
|
lcdlss.c |
|
4 |
|
lcdlss.s |
|
5 |
|
lcdlss.u |
|
6 |
|
lcdlss.f |
|
7 |
|
lcdlss.l |
|
8 |
|
lcdlss.d |
|
9 |
|
lcdlss.t |
|
10 |
|
lcdlss.b |
|
11 |
|
lcdlss.k |
|
12 |
1 2 3 5 6 7 8 11 10
|
lcdval2 |
|
13 |
12
|
fveq2d |
|
14 |
4 13
|
syl5eq |
|
15 |
14
|
eleq2d |
|
16 |
1 5 11
|
dvhlmod |
|
17 |
8 16
|
lduallmod |
|
18 |
1 5 2 6 7 8 9 10 11
|
lclkr |
|
19 |
|
eqid |
|
20 |
|
eqid |
|
21 |
19 9 20
|
lsslss |
|
22 |
17 18 21
|
syl2anc |
|
23 |
15 22
|
bitrd |
|
24 |
|
elin |
|
25 |
|
velpw |
|
26 |
25
|
anbi2i |
|
27 |
24 26
|
bitr2i |
|
28 |
23 27
|
bitrdi |
|
29 |
28
|
eqrdv |
|