Proof of Theorem scshwfzeqfzo
Step | Hyp | Ref
| Expression |
1 | | lencl 13324 |
. . . . . . . . . . . 12
Word |
2 | | elnn0uz 11725 |
. . . . . . . . . . . 12
|
3 | 1, 2 | sylib 208 |
. . . . . . . . . . 11
Word |
4 | 3 | adantr 481 |
. . . . . . . . . 10
Word
|
5 | | eleq1 2689 |
. . . . . . . . . . 11
|
6 | 5 | adantl 482 |
. . . . . . . . . 10
Word
|
7 | 4, 6 | mpbird 247 |
. . . . . . . . 9
Word
|
8 | 7 | 3adant2 1080 |
. . . . . . . 8
Word |
9 | 8 | adantr 481 |
. . . . . . 7
Word
Word |
10 | | fzisfzounsn 12580 |
. . . . . . 7
..^ |
11 | 9, 10 | syl 17 |
. . . . . 6
Word
Word ..^ |
12 | 11 | rexeqdv 3145 |
. . . . 5
Word
Word
cyclShift
..^ cyclShift |
13 | | rexun 3793 |
. . . . 5
..^ cyclShift
..^ cyclShift
cyclShift |
14 | 12, 13 | syl6bb 276 |
. . . 4
Word
Word
cyclShift ..^ cyclShift
cyclShift |
15 | | ax-1 6 |
. . . . . 6
..^ cyclShift
Word Word ..^ cyclShift |
16 | | fvex 6201 |
. . . . . . . . . . . 12
|
17 | | eleq1 2689 |
. . . . . . . . . . . 12
|
18 | 16, 17 | mpbiri 248 |
. . . . . . . . . . 11
|
19 | | oveq2 6658 |
. . . . . . . . . . . . 13
cyclShift cyclShift |
20 | 19 | eqeq2d 2632 |
. . . . . . . . . . . 12
cyclShift
cyclShift |
21 | 20 | rexsng 4219 |
. . . . . . . . . . 11
cyclShift
cyclShift |
22 | 18, 21 | syl 17 |
. . . . . . . . . 10
cyclShift
cyclShift |
23 | 22 | 3ad2ant3 1084 |
. . . . . . . . 9
Word
cyclShift
cyclShift |
24 | 23 | adantr 481 |
. . . . . . . 8
Word
Word
cyclShift
cyclShift |
25 | | oveq2 6658 |
. . . . . . . . . . . . 13
cyclShift cyclShift |
26 | 25 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
Word cyclShift cyclShift |
27 | | cshwn 13543 |
. . . . . . . . . . . . 13
Word cyclShift |
28 | 27 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
Word cyclShift |
29 | 26, 28 | eqtrd 2656 |
. . . . . . . . . . 11
Word cyclShift |
30 | 29 | eqeq2d 2632 |
. . . . . . . . . 10
Word cyclShift
|
31 | 30 | adantr 481 |
. . . . . . . . 9
Word
Word cyclShift
|
32 | | cshw0 13540 |
. . . . . . . . . . . . . . 15
Word cyclShift |
33 | 32 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
Word cyclShift |
34 | | lennncl 13325 |
. . . . . . . . . . . . . . . . . 18
Word |
35 | 34 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
Word |
36 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . 17
Word
|
38 | 35, 37 | mpbird 247 |
. . . . . . . . . . . . . . . 16
Word |
39 | | lbfzo0 12507 |
. . . . . . . . . . . . . . . 16
..^
|
40 | 38, 39 | sylibr 224 |
. . . . . . . . . . . . . . 15
Word ..^ |
41 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
cyclShift cyclShift |
42 | 41 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
cyclShift cyclShift |
43 | 42 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . 18
cyclShift cyclShift |
44 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . 18
cyclShift cyclShift |
45 | 43, 44 | syl6bb 276 |
. . . . . . . . . . . . . . . . 17
cyclShift
cyclShift |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . 16
Word
cyclShift
cyclShift |
47 | 46 | biimpd 219 |
. . . . . . . . . . . . . . 15
Word
cyclShift
cyclShift |
48 | 40, 47 | rspcimedv 3311 |
. . . . . . . . . . . . . 14
Word
cyclShift
..^ cyclShift |
49 | 33, 48 | mpd 15 |
. . . . . . . . . . . . 13
Word ..^ cyclShift |
50 | 49 | adantr 481 |
. . . . . . . . . . . 12
Word
Word ..^ cyclShift |
51 | 50 | adantr 481 |
. . . . . . . . . . 11
Word Word ..^ cyclShift |
52 | | eqeq1 2626 |
. . . . . . . . . . . . 13
cyclShift
cyclShift |
53 | 52 | adantl 482 |
. . . . . . . . . . . 12
Word Word cyclShift
cyclShift |
54 | 53 | rexbidv 3052 |
. . . . . . . . . . 11
Word Word
..^ cyclShift
..^ cyclShift |
55 | 51, 54 | mpbird 247 |
. . . . . . . . . 10
Word Word ..^ cyclShift |
56 | 55 | ex 450 |
. . . . . . . . 9
Word
Word
..^ cyclShift |
57 | 31, 56 | sylbid 230 |
. . . . . . . 8
Word
Word cyclShift ..^ cyclShift |
58 | 24, 57 | sylbid 230 |
. . . . . . 7
Word
Word
cyclShift ..^ cyclShift |
59 | 58 | com12 32 |
. . . . . 6
cyclShift Word Word ..^ cyclShift |
60 | 15, 59 | jaoi 394 |
. . . . 5
..^ cyclShift cyclShift
Word
Word ..^ cyclShift |
61 | 60 | com12 32 |
. . . 4
Word
Word ..^ cyclShift
cyclShift
..^ cyclShift |
62 | 14, 61 | sylbid 230 |
. . 3
Word
Word
cyclShift ..^ cyclShift |
63 | | fzossfz 12488 |
. . . 4
..^ |
64 | | ssrexv 3667 |
. . . 4
..^
..^ cyclShift
cyclShift |
65 | 63, 64 | mp1i 13 |
. . 3
Word
Word
..^ cyclShift cyclShift |
66 | 62, 65 | impbid 202 |
. 2
Word
Word
cyclShift
..^ cyclShift |
67 | 66 | rabbidva 3188 |
1
Word Word
cyclShift Word
..^ cyclShift
|