Proof of Theorem clwwisshclwwslem
Step | Hyp | Ref
| Expression |
1 | | elfzoelz 12470 |
. . . . . . . . 9
..^
|
2 | | cshwlen 13545 |
. . . . . . . . 9
Word
cyclShift |
3 | 1, 2 | sylan2 491 |
. . . . . . . 8
Word
..^ cyclShift |
4 | 3 | oveq1d 6665 |
. . . . . . 7
Word
..^ cyclShift |
5 | 4 | oveq2d 6666 |
. . . . . 6
Word
..^ ..^ cyclShift ..^ |
6 | 5 | eleq2d 2687 |
. . . . 5
Word
..^ ..^ cyclShift
..^ |
7 | 6 | adantr 481 |
. . . 4
Word
..^ ..^ lastS ..^ cyclShift
..^ |
8 | | simpll 790 |
. . . . . . . . 9
Word
..^
..^ Word |
9 | 1 | ad2antlr 763 |
. . . . . . . . 9
Word
..^
..^ |
10 | | lencl 13324 |
. . . . . . . . . . . . 13
Word |
11 | | nn0z 11400 |
. . . . . . . . . . . . . . 15
|
12 | | peano2zm 11420 |
. . . . . . . . . . . . . . 15
|
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
|
14 | | nn0re 11301 |
. . . . . . . . . . . . . . 15
|
15 | 14 | lem1d 10957 |
. . . . . . . . . . . . . 14
|
16 | | eluz2 11693 |
. . . . . . . . . . . . . 14
|
17 | 13, 11, 15, 16 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
|
18 | 10, 17 | syl 17 |
. . . . . . . . . . . 12
Word |
19 | 18 | adantr 481 |
. . . . . . . . . . 11
Word
..^ |
20 | | fzoss2 12496 |
. . . . . . . . . . 11
..^ ..^ |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
Word
..^ ..^ ..^ |
22 | 21 | sselda 3603 |
. . . . . . . . 9
Word
..^
..^ ..^ |
23 | | cshwidxmod 13549 |
. . . . . . . . 9
Word
..^ cyclShift |
24 | 8, 9, 22, 23 | syl3anc 1326 |
. . . . . . . 8
Word
..^
..^
cyclShift |
25 | | elfzo1 12517 |
. . . . . . . . . . . 12
..^ |
26 | 25 | simp2bi 1077 |
. . . . . . . . . . 11
..^
|
27 | 26 | adantl 482 |
. . . . . . . . . 10
Word
..^ |
28 | | elfzom1p1elfzo 12547 |
. . . . . . . . . 10
..^ ..^ |
29 | 27, 28 | sylan 488 |
. . . . . . . . 9
Word
..^
..^ ..^ |
30 | | cshwidxmod 13549 |
. . . . . . . . 9
Word
..^
cyclShift |
31 | 8, 9, 29, 30 | syl3anc 1326 |
. . . . . . . 8
Word
..^
..^
cyclShift |
32 | 24, 31 | preq12d 4276 |
. . . . . . 7
Word
..^
..^ cyclShift
cyclShift
|
33 | 32 | adantlr 751 |
. . . . . 6
Word ..^ ..^ lastS ..^ cyclShift cyclShift
|
34 | | 2z 11409 |
. . . . . . . . . . 11
|
35 | 34 | a1i 11 |
. . . . . . . . . 10
|
36 | | nnz 11399 |
. . . . . . . . . . 11
|
37 | 36 | 3ad2ant2 1083 |
. . . . . . . . . 10
|
38 | | nnnn0 11299 |
. . . . . . . . . . . 12
|
39 | 38 | 3ad2ant2 1083 |
. . . . . . . . . . 11
|
40 | | nnne0 11053 |
. . . . . . . . . . . 12
|
41 | 40 | 3ad2ant2 1083 |
. . . . . . . . . . 11
|
42 | | 1red 10055 |
. . . . . . . . . . . 12
|
43 | | nnre 11027 |
. . . . . . . . . . . . . 14
|
44 | 43 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
45 | | nnre 11027 |
. . . . . . . . . . . . . 14
|
46 | 45 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
|
47 | | nnge1 11046 |
. . . . . . . . . . . . . 14
|
48 | 47 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
49 | | simp3 1063 |
. . . . . . . . . . . . 13
|
50 | 42, 44, 46, 48, 49 | lelttrd 10195 |
. . . . . . . . . . . 12
|
51 | 42, 50 | gtned 10172 |
. . . . . . . . . . 11
|
52 | | nn0n0n1ge2 11358 |
. . . . . . . . . . 11
|
53 | 39, 41, 51, 52 | syl3anc 1326 |
. . . . . . . . . 10
|
54 | | eluz2 11693 |
. . . . . . . . . 10
|
55 | 35, 37, 53, 54 | syl3anbrc 1246 |
. . . . . . . . 9
|
56 | 25, 55 | sylbi 207 |
. . . . . . . 8
..^
|
57 | 56 | ad3antlr 767 |
. . . . . . 7
Word ..^ ..^ lastS ..^ |
58 | | elfzoelz 12470 |
. . . . . . . 8
..^
|
59 | 58 | adantl 482 |
. . . . . . 7
Word ..^ ..^ lastS ..^ |
60 | 1 | ad3antlr 767 |
. . . . . . 7
Word ..^ ..^ lastS ..^
|
61 | | simplrl 800 |
. . . . . . 7
Word ..^ ..^ lastS ..^
..^ |
62 | | lsw 13351 |
. . . . . . . . . . . . . 14
Word lastS |
63 | 62 | adantr 481 |
. . . . . . . . . . . . 13
Word
..^ lastS |
64 | 63 | preq1d 4274 |
. . . . . . . . . . . 12
Word
..^
lastS |
65 | 64 | eleq1d 2686 |
. . . . . . . . . . 11
Word
..^ lastS
|
66 | 65 | biimpcd 239 |
. . . . . . . . . 10
lastS Word ..^ |
67 | 66 | adantl 482 |
. . . . . . . . 9
..^ lastS Word ..^ |
68 | 67 | impcom 446 |
. . . . . . . 8
Word
..^ ..^ lastS |
69 | 68 | adantr 481 |
. . . . . . 7
Word ..^ ..^ lastS ..^ |
70 | | clwwisshclwwslemlem 26926 |
. . . . . . 7
..^ |
71 | 57, 59, 60, 61, 69, 70 | syl311anc 1340 |
. . . . . 6
Word ..^ ..^ lastS ..^ |
72 | 33, 71 | eqeltrd 2701 |
. . . . 5
Word ..^ ..^ lastS ..^ cyclShift cyclShift |
73 | 72 | ex 450 |
. . . 4
Word
..^ ..^ lastS ..^ cyclShift cyclShift |
74 | 7, 73 | sylbid 230 |
. . 3
Word
..^ ..^ lastS ..^ cyclShift cyclShift
cyclShift
|
75 | 74 | ralrimiv 2965 |
. 2
Word
..^ ..^ lastS ..^ cyclShift
cyclShift cyclShift |
76 | 75 | ex 450 |
1
Word
..^ ..^ lastS ..^ cyclShift cyclShift
cyclShift
|