Proof of Theorem cshwshashlem1
Step | Hyp | Ref
| Expression |
1 | | df-ne 2795 |
. . . . . . 7
|
2 | 1 | rexbii 3041 |
. . . . . 6
..^ ..^ |
3 | | rexnal 2995 |
. . . . . 6
..^
..^ |
4 | 2, 3 | bitri 264 |
. . . . 5
..^
..^ |
5 | | simpll 790 |
. . . . . . . . . . 11
..^ cyclShift |
6 | | fzo0ss1 12498 |
. . . . . . . . . . . . . 14
..^ ..^ |
7 | | fzossfz 12488 |
. . . . . . . . . . . . . 14
..^ |
8 | 6, 7 | sstri 3612 |
. . . . . . . . . . . . 13
..^ |
9 | 8 | sseli 3599 |
. . . . . . . . . . . 12
..^
|
10 | 9 | ad2antlr 763 |
. . . . . . . . . . 11
..^ cyclShift
|
11 | | simpr 477 |
. . . . . . . . . . 11
..^ cyclShift
cyclShift |
12 | | cshwshash.0 |
. . . . . . . . . . . . 13
Word |
13 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
Word
Word |
14 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
Word |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
|
16 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . 18
|
17 | 16 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word
|
18 | | cshwsidrepswmod0 15801 |
. . . . . . . . . . . . . . . . 17
Word
cyclShift
repeatS |
19 | 13, 15, 17, 18 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Word
cyclShift repeatS |
20 | 19 | ex 450 |
. . . . . . . . . . . . . . 15
Word
cyclShift
repeatS |
21 | 20 | 3imp 1256 |
. . . . . . . . . . . . . 14
Word
cyclShift
repeatS |
22 | | olc 399 |
. . . . . . . . . . . . . . . . . . . 20
|
23 | 22 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
Word
cyclShift
|
24 | | fzofzim 12514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ |
25 | | zmodidfzoimp 12700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
|
26 | | eqtr2 2642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
27 | 26 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Word
|
28 | 27 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Word
|
29 | 25, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
Word
|
30 | 24, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word
|
31 | 30 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Word
|
32 | 31 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
|
33 | 32 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word
|
34 | 33 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word
cyclShift
|
35 | 34 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . 22
Word
cyclShift
|
36 | 35 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
Word
cyclShift
|
37 | 36 | orcd 407 |
. . . . . . . . . . . . . . . . . . . 20
Word
cyclShift |
38 | 37 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
Word
cyclShift
|
39 | 23, 38 | pm2.61ine 2877 |
. . . . . . . . . . . . . . . . . 18
Word
cyclShift
|
40 | 39 | orcd 407 |
. . . . . . . . . . . . . . . . 17
Word
cyclShift repeatS
|
41 | | df-3or 1038 |
. . . . . . . . . . . . . . . . 17
repeatS repeatS |
42 | 40, 41 | sylibr 224 |
. . . . . . . . . . . . . . . 16
Word
cyclShift
repeatS
|
43 | 42 | ex 450 |
. . . . . . . . . . . . . . 15
Word
cyclShift
repeatS
|
44 | | 3mix3 1232 |
. . . . . . . . . . . . . . . 16
repeatS repeatS
|
45 | 44 | a1d 25 |
. . . . . . . . . . . . . . 15
repeatS Word cyclShift
repeatS |
46 | 43, 45 | jaoi 394 |
. . . . . . . . . . . . . 14
repeatS
Word
cyclShift
repeatS
|
47 | 21, 46 | mpcom 38 |
. . . . . . . . . . . . 13
Word
cyclShift
repeatS
|
48 | 12, 47 | syl3an1 1359 |
. . . . . . . . . . . 12
cyclShift
repeatS |
49 | | 3mix1 1230 |
. . . . . . . . . . . . . 14
..^ |
50 | 49 | a1d 25 |
. . . . . . . . . . . . 13
cyclShift ..^ |
51 | | 3mix2 1231 |
. . . . . . . . . . . . . 14
..^ |
52 | 51 | a1d 25 |
. . . . . . . . . . . . 13
cyclShift
..^ |
53 | | repswsymballbi 13527 |
. . . . . . . . . . . . . . . . . . 19
Word
repeatS ..^ |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Word
repeatS ..^ |
55 | 12, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
repeatS
..^ |
56 | 55 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
cyclShift repeatS
..^ |
57 | 56 | biimpa 501 |
. . . . . . . . . . . . . . 15
cyclShift
repeatS ..^ |
58 | 57 | 3mix3d 1238 |
. . . . . . . . . . . . . 14
cyclShift
repeatS
..^ |
59 | 58 | expcom 451 |
. . . . . . . . . . . . 13
repeatS cyclShift
..^ |
60 | 50, 52, 59 | 3jaoi 1391 |
. . . . . . . . . . . 12
repeatS
cyclShift
..^ |
61 | 48, 60 | mpcom 38 |
. . . . . . . . . . 11
cyclShift ..^ |
62 | 5, 10, 11, 61 | syl3anc 1326 |
. . . . . . . . . 10
..^ cyclShift ..^ |
63 | | elfzo1 12517 |
. . . . . . . . . . . . . 14
..^ |
64 | | nnne0 11053 |
. . . . . . . . . . . . . . . 16
|
65 | | df-ne 2795 |
. . . . . . . . . . . . . . . . 17
|
66 | | pm2.21 120 |
. . . . . . . . . . . . . . . . 17
..^ |
67 | 65, 66 | sylbi 207 |
. . . . . . . . . . . . . . . 16
..^ |
68 | 64, 67 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
69 | 68 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
..^ |
70 | 63, 69 | sylbi 207 |
. . . . . . . . . . . . 13
..^
..^ |
71 | 70 | ad2antlr 763 |
. . . . . . . . . . . 12
..^ cyclShift ..^ |
72 | 71 | com12 32 |
. . . . . . . . . . 11
..^
cyclShift ..^ |
73 | | nnre 11027 |
. . . . . . . . . . . . . . . . 17
|
74 | | ltne 10134 |
. . . . . . . . . . . . . . . . 17
|
75 | 73, 74 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
76 | | df-ne 2795 |
. . . . . . . . . . . . . . . . 17
|
77 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . 18
|
78 | | pm2.21 120 |
. . . . . . . . . . . . . . . . . 18
..^ |
79 | 77, 78 | syl5bi 232 |
. . . . . . . . . . . . . . . . 17
..^ |
80 | 76, 79 | sylbi 207 |
. . . . . . . . . . . . . . . 16
..^ |
81 | 75, 80 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
82 | 81 | 3adant2 1080 |
. . . . . . . . . . . . . 14
..^ |
83 | 63, 82 | sylbi 207 |
. . . . . . . . . . . . 13
..^
..^ |
84 | 83 | ad2antlr 763 |
. . . . . . . . . . . 12
..^ cyclShift ..^ |
85 | 84 | com12 32 |
. . . . . . . . . . 11
..^ cyclShift
..^ |
86 | | ax-1 6 |
. . . . . . . . . . 11
..^
..^ cyclShift
..^ |
87 | 72, 85, 86 | 3jaoi 1391 |
. . . . . . . . . 10
..^
..^
cyclShift ..^ |
88 | 62, 87 | mpcom 38 |
. . . . . . . . 9
..^ cyclShift
..^ |
89 | 88 | pm2.24d 147 |
. . . . . . . 8
..^ cyclShift ..^ cyclShift |
90 | 89 | exp31 630 |
. . . . . . 7
..^
cyclShift
..^
cyclShift |
91 | 90 | com34 91 |
. . . . . 6
..^ ..^
cyclShift cyclShift |
92 | 91 | com23 86 |
. . . . 5
..^
..^
cyclShift
cyclShift |
93 | 4, 92 | syl5bi 232 |
. . . 4
..^
..^
cyclShift
cyclShift |
94 | 93 | 3imp 1256 |
. . 3
..^ ..^ cyclShift cyclShift |
95 | 94 | com12 32 |
. 2
cyclShift ..^
..^
cyclShift |
96 | | ax-1 6 |
. 2
cyclShift ..^
..^
cyclShift |
97 | 95, 96 | pm2.61ine 2877 |
1
..^ ..^ cyclShift |