Proof of Theorem cshwidxmod
Step | Hyp | Ref
| Expression |
1 | | elfzo0 12508 |
. . . 4
..^
|
2 | | nnne0 11053 |
. . . . . 6
|
3 | | eqneqall 2805 |
. . . . . . 7
cyclShift |
4 | 3 | com12 32 |
. . . . . 6
cyclShift |
5 | 2, 4 | syl 17 |
. . . . 5
cyclShift |
6 | 5 | 3ad2ant2 1083 |
. . . 4
cyclShift |
7 | 1, 6 | sylbi 207 |
. . 3
..^
cyclShift |
8 | 7 | 3ad2ant3 1084 |
. 2
Word
..^ cyclShift |
9 | | lencl 13324 |
. . . . 5
Word |
10 | | elnnne0 11306 |
. . . . . . . 8
|
11 | | simpl 473 |
. . . . . . . . . . . . . 14
..^
|
12 | 11 | adantl 482 |
. . . . . . . . . . . . 13
..^ |
13 | | cshword 13537 |
. . . . . . . . . . . . 13
Word
cyclShift
substr ++ substr |
14 | 12, 13 | sylan2 491 |
. . . . . . . . . . . 12
Word
..^
cyclShift substr ++
substr |
15 | 14 | fveq1d 6193 |
. . . . . . . . . . 11
Word
..^
cyclShift substr ++ substr |
16 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . 17
Word substr Word |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word
..^
substr Word |
18 | 17 | adantl 482 |
. . . . . . . . . . . . . . 15
..^
Word
..^ substr
Word |
19 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . 17
Word substr Word
|
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word
..^
substr Word |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . 15
..^
Word
..^ substr
Word |
22 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
Word |
23 | 11 | anim2i 593 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
24 | 23 | ancomd 467 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
25 | | zmodfzp1 12694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
|
28 | | nn0fz0 12437 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | 9, 28 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
Word |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
|
31 | | swrdlen 13423 |
. . . . . . . . . . . . . . . . . . . 20
Word
substr |
32 | 22, 27, 30, 31 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
substr |
33 | 32 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
Word
..^
substr |
34 | | swrd0len 13422 |
. . . . . . . . . . . . . . . . . . . . 21
Word
substr |
35 | 26, 34 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
substr |
36 | 35 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
substr |
37 | 33, 36 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
Word
..^
substr substr |
38 | 33, 37 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
Word
..^
..^ substr ..^ substr substr |
39 | 38 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
Word
..^
..^
substr ..^ substr substr |
40 | 39 | biimpac 503 |
. . . . . . . . . . . . . . 15
..^
Word
..^
substr ..^ substr substr |
41 | | ccatval2 13362 |
. . . . . . . . . . . . . . 15
substr Word
substr
Word
substr ..^ substr substr
substr
++ substr substr substr |
42 | 18, 21, 40, 41 | syl3anc 1326 |
. . . . . . . . . . . . . 14
..^
Word
..^ substr ++ substr substr substr |
43 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . 17
..^
Word
..^
Word |
44 | 27 | adantl 482 |
. . . . . . . . . . . . . . . . 17
..^
Word
..^ |
45 | 30 | adantl 482 |
. . . . . . . . . . . . . . . . 17
..^
Word
..^ |
46 | 43, 44, 45, 31 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
..^
Word
..^ substr |
47 | 46 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
..^
Word
..^ substr |
48 | 47 | fveq2d 6195 |
. . . . . . . . . . . . . 14
..^
Word
..^ substr substr substr |
49 | | elfzo2 12473 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
50 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
51 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
52 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
54 | | zmodcl 12690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
55 | 54 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
56 | 53, 55 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
57 | 56 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
58 | 51, 57 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
59 | 58 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
60 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
61 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
62 | 61 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
63 | 54 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
64 | 62, 63 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
65 | | subge0 10541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
66 | 60, 64, 65 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
67 | 66 | exbiri 652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
68 | 67 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
69 | 68 | imp31 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
70 | | elnn0uz 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
71 | | elnn0z 11390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
72 | 70, 71 | bitr3i 266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
73 | 59, 69, 72 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
74 | 73 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
75 | 55 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
76 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
77 | 64 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
78 | 63 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
79 | 76, 77, 78 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
80 | 79 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
81 | | ltsubadd2 10499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
83 | 82 | exbiri 652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
84 | 83 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
85 | 84 | imp31 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
86 | | elfzo2 12473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
|
87 | 74, 75, 85, 86 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ |
88 | 87 | exp31 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^ |
89 | 88 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ |
90 | 50, 89 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ |
91 | 90 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ |
92 | 91 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
93 | 49, 92 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ |
94 | 93 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
95 | 94 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
96 | 95 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ ..^ |
97 | 96 | impcom 446 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ ..^ |
98 | 97 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word
..^
..^ ..^ |
99 | 98 | impcom 446 |
. . . . . . . . . . . . . . . 16
..^
Word
..^ ..^ |
100 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . 16
Word
..^
substr |
101 | 43, 44, 99, 100 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
..^
Word
..^ substr
|
102 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
103 | 102 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
104 | 103 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
105 | 104 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
106 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . 22
|
107 | 106 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
108 | 24, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
109 | 108 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
110 | 105, 107,
109 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
111 | 110 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
|
112 | 111 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
..^
Word
..^
|
113 | | subsub3 10313 |
. . . . . . . . . . . . . . . . . 18
|
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^
Word
..^
|
115 | 24 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
|
116 | 115 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
..^
Word
..^ |
117 | 107, 109 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
118 | 117 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
Word
..^
|
119 | | npcan 10290 |
. . . . . . . . . . . . . . . . . . . . . 22
|
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
Word
..^
|
121 | 120 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
..^ ..^ |
122 | 121 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
..^
..^ |
123 | 122 | biimpac 503 |
. . . . . . . . . . . . . . . . . 18
..^
Word
..^
..^ |
124 | | modaddmodup 12733 |
. . . . . . . . . . . . . . . . . 18
..^
|
125 | 116, 123,
124 | sylc 65 |
. . . . . . . . . . . . . . . . 17
..^
Word
..^
|
126 | 114, 125 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
..^
Word
..^ |
127 | 126 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
..^
Word
..^ |
128 | 101, 127 | eqtrd 2656 |
. . . . . . . . . . . . . 14
..^
Word
..^ substr |
129 | 42, 48, 128 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
..^
Word
..^ substr ++ substr |
130 | 129 | ex 450 |
. . . . . . . . . . . 12
..^ Word
..^
substr
++ substr |
131 | 106 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
132 | 54 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . . 22
|
133 | 131, 132 | npcand 10396 |
. . . . . . . . . . . . . . . . . . . . 21
|
134 | 133 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
|
135 | 134 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ |
136 | 135 | impcom 446 |
. . . . . . . . . . . . . . . . . 18
..^ |
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word
..^
|
138 | 137 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
Word
..^
..^ ..^ |
139 | 138 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
Word
..^
..^
..^ |
140 | 139 | notbid 308 |
. . . . . . . . . . . . . 14
Word
..^
..^
..^ |
141 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
..^ ..^ substr Word |
142 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
..^ ..^ substr Word
|
143 | 108 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
144 | 143 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
|
145 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
146 | 145 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
147 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . . 22
|
148 | | modlt 12679 |
. . . . . . . . . . . . . . . . . . . . . 22
|
149 | 146, 147,
148 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
150 | 149 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
|
151 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
..^ |
152 | | fzonfzoufzol 12571 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
..^ |
153 | 144, 150,
151, 152 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
..^
..^ |
154 | 153 | imp 445 |
. . . . . . . . . . . . . . . . . 18
Word
..^ ..^ ..^ |
155 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^ ..^ Word |
156 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^ ..^ |
157 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^ ..^ |
158 | 155, 156,
157, 31 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
Word
..^ ..^ substr |
159 | 158 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
Word
..^ ..^ ..^ substr ..^ |
160 | 154, 159 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . 17
Word
..^ ..^ ..^ substr |
161 | | ccatval1 13361 |
. . . . . . . . . . . . . . . . 17
substr Word
substr
Word
..^ substr substr ++ substr substr |
162 | 141, 142,
160, 161 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Word
..^ ..^ substr ++ substr substr |
163 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
|
164 | 163 | ancomd 467 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
|
165 | 164, 25 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Word
..^
|
166 | 165 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
..^ ..^ |
167 | | swrdfv 13424 |
. . . . . . . . . . . . . . . . 17
Word ..^ substr
|
168 | 155, 166,
157, 154, 167 | syl31anc 1329 |
. . . . . . . . . . . . . . . 16
Word
..^ ..^ substr
|
169 | 115 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Word
..^ ..^
|
170 | 54 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
171 | 170 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . 22
|
172 | 171 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
173 | 172 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
|
174 | 173, 150,
151, 152 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
..^
..^ |
175 | 174 | imp 445 |
. . . . . . . . . . . . . . . . . 18
Word
..^ ..^ ..^ |
176 | | modaddmodlo 12734 |
. . . . . . . . . . . . . . . . . 18
..^
|
177 | 169, 175,
176 | sylc 65 |
. . . . . . . . . . . . . . . . 17
Word
..^ ..^ |
178 | 177 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
Word
..^ ..^
|
179 | 162, 168,
178 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
Word
..^ ..^ substr ++ substr |
180 | 179 | ex 450 |
. . . . . . . . . . . . . 14
Word
..^
..^ substr ++ substr |
181 | 140, 180 | sylbid 230 |
. . . . . . . . . . . . 13
Word
..^
..^ substr ++ substr |
182 | 181 | com12 32 |
. . . . . . . . . . . 12
..^ Word
..^
substr
++ substr |
183 | 130, 182 | pm2.61i 176 |
. . . . . . . . . . 11
Word
..^
substr
++ substr |
184 | 15, 183 | eqtrd 2656 |
. . . . . . . . . 10
Word
..^
cyclShift |
185 | 184 | exp32 631 |
. . . . . . . . 9
Word ..^ cyclShift
|
186 | 185 | com12 32 |
. . . . . . . 8
Word
..^ cyclShift |
187 | 10, 186 | sylbir 225 |
. . . . . . 7
Word ..^ cyclShift |
188 | 187 | ex 450 |
. . . . . 6
Word
..^ cyclShift |
189 | 188 | com23 86 |
. . . . 5
Word
..^ cyclShift |
190 | 9, 189 | mpcom 38 |
. . . 4
Word ..^ cyclShift
|
191 | 190 | com23 86 |
. . 3
Word ..^ cyclShift
|
192 | 191 | 3impib 1262 |
. 2
Word
..^ cyclShift
|
193 | 8, 192 | pm2.61dne 2880 |
1
Word
..^ cyclShift |