Proof of Theorem crctcshwlkn0lem5
Step | Hyp | Ref
| Expression |
1 | | crctcshwlkn0lem.p |
. . . . 5
..^if- |
2 | | crctcshwlkn0lem.s |
. . . . . . 7
..^ |
3 | | elfzoelz 12470 |
. . . . . . . . . . . 12
..^
|
4 | 3 | zcnd 11483 |
. . . . . . . . . . 11
..^
|
5 | 4 | adantl 482 |
. . . . . . . . . 10
..^ ..^
|
6 | | 1cnd 10056 |
. . . . . . . . . 10
..^ ..^
|
7 | | elfzoelz 12470 |
. . . . . . . . . . . 12
..^
|
8 | 7 | zcnd 11483 |
. . . . . . . . . . 11
..^
|
9 | 8 | adantr 481 |
. . . . . . . . . 10
..^ ..^
|
10 | | elfzoel2 12469 |
. . . . . . . . . . . 12
..^
|
11 | 10 | zcnd 11483 |
. . . . . . . . . . 11
..^
|
12 | 11 | adantr 481 |
. . . . . . . . . 10
..^ ..^
|
13 | 5, 6, 9, 12 | 2addsubd 10442 |
. . . . . . . . 9
..^ ..^
|
14 | 13 | eqcomd 2628 |
. . . . . . . 8
..^ ..^
|
15 | | elfzo1 12517 |
. . . . . . . . . . . 12
..^ |
16 | | nnz 11399 |
. . . . . . . . . . . . . . . . 17
|
17 | 16 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . 16
|
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . 15
..^
|
19 | 3 | adantl 482 |
. . . . . . . . . . . . . . . 16
..^ |
20 | | nnz 11399 |
. . . . . . . . . . . . . . . . . 18
|
21 | 20 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
|
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^
|
23 | 19, 22 | zaddcld 11486 |
. . . . . . . . . . . . . . 15
..^ |
24 | | elfzo2 12473 |
. . . . . . . . . . . . . . . . 17
..^
|
25 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
27 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
28 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
29 | 27, 28 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
30 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
31 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
32 | 30, 31 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
33 | 32 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
34 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
35 | 32, 34 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
36 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
37 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
38 | 32, 35, 36, 37 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
39 | 33, 38 | mpand 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
40 | 30, 31, 36 | lesubaddd 10624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
41 | 39, 40 | sylibd 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
42 | 41 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
43 | 29, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
44 | 43 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
45 | 26, 44 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
46 | 45 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 46 | imp 445 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 47 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 25, 48 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 49 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
|
51 | 50 | com12 32 |
. . . . . . . . . . . . . . . . 17
|
52 | 24, 51 | syl5bi 232 |
. . . . . . . . . . . . . . . 16
..^ |
53 | 52 | imp 445 |
. . . . . . . . . . . . . . 15
..^ |
54 | | eluz2 11693 |
. . . . . . . . . . . . . . 15
|
55 | 18, 23, 53, 54 | syl3anbrc 1246 |
. . . . . . . . . . . . . 14
..^ |
56 | | uznn0sub 11719 |
. . . . . . . . . . . . . 14
|
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . 13
..^ |
58 | | simpl2 1065 |
. . . . . . . . . . . . 13
..^
|
59 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
60 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
61 | | ax-1 6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
62 | 61 | imdistanri 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
64 | | lt2add 10513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
65 | 59, 60, 63, 64 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
66 | 59, 60 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
67 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
68 | 66, 67, 67 | ltsubaddd 10623 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
69 | 65, 68 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
70 | 69 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
71 | 70 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
72 | 71 | expcomd 454 |
. . . . . . . . . . . . . . . . . . . . . 22
|
73 | 29, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | 73 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . 20
|
75 | 74 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
|
76 | 75 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . 18
|
77 | 25, 76 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
|
78 | 77 | imp 445 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | 3adant2 1080 |
. . . . . . . . . . . . . . 15
|
80 | 24, 79 | sylbi 207 |
. . . . . . . . . . . . . 14
..^
|
81 | 80 | impcom 446 |
. . . . . . . . . . . . 13
..^
|
82 | 57, 58, 81 | 3jca 1242 |
. . . . . . . . . . . 12
..^
|
83 | 15, 82 | sylanb 489 |
. . . . . . . . . . 11
..^ ..^
|
84 | | elfzo0 12508 |
. . . . . . . . . . 11
..^
|
85 | 83, 84 | sylibr 224 |
. . . . . . . . . 10
..^ ..^
..^ |
86 | 85 | adantr 481 |
. . . . . . . . 9
..^
..^ ..^ |
87 | | fveq2 6191 |
. . . . . . . . . . . 12
|
88 | 87 | adantl 482 |
. . . . . . . . . . 11
..^ ..^ |
89 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
90 | 89 | fveq2d 6195 |
. . . . . . . . . . . 12
|
91 | | simpr 477 |
. . . . . . . . . . . . 13
..^
..^ |
92 | 91 | fveq2d 6195 |
. . . . . . . . . . . 12
..^
..^ |
93 | 90, 92 | sylan9eqr 2678 |
. . . . . . . . . . 11
..^ ..^ |
94 | 88, 93 | eqeq12d 2637 |
. . . . . . . . . 10
..^ ..^
|
95 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . 12
|
97 | 87 | sneqd 4189 |
. . . . . . . . . . . 12
|
98 | 96, 97 | eqeq12d 2637 |
. . . . . . . . . . 11
|
99 | 98 | adantl 482 |
. . . . . . . . . 10
..^ ..^ |
100 | 88, 93 | preq12d 4276 |
. . . . . . . . . . 11
..^ ..^ |
101 | | simpr 477 |
. . . . . . . . . . . . 13
..^ ..^ |
102 | 101 | fveq2d 6195 |
. . . . . . . . . . . 12
..^ ..^ |
103 | 102 | fveq2d 6195 |
. . . . . . . . . . 11
..^ ..^ |
104 | 100, 103 | sseq12d 3634 |
. . . . . . . . . 10
..^ ..^
|
105 | 94, 99, 104 | ifpbi123d 1027 |
. . . . . . . . 9
..^ ..^ if-
if- |
106 | 86, 105 | rspcdv 3312 |
. . . . . . . 8
..^
..^ ..^if- if- |
107 | 14, 106 | mpdan 702 |
. . . . . . 7
..^ ..^
..^if- if-
|
108 | 2, 107 | sylan 488 |
. . . . . 6
..^
..^if- if-
|
109 | 108 | ex 450 |
. . . . 5
..^ ..^if- if- |
110 | 1, 109 | mpid 44 |
. . . 4
..^ if- |
111 | 110 | imp 445 |
. . 3
..^
if- |
112 | | elfzofz 12485 |
. . . . 5
..^
|
113 | | crctcshwlkn0lem.q |
. . . . . 6
|
114 | 2, 113 | crctcshwlkn0lem3 26704 |
. . . . 5
|
115 | 112, 114 | sylan2 491 |
. . . 4
..^
|
116 | | fzofzp1 12565 |
. . . . 5
..^
|
117 | 2, 113 | crctcshwlkn0lem3 26704 |
. . . . 5
|
118 | 116, 117 | sylan2 491 |
. . . 4
..^
|
119 | | crctcshwlkn0lem.h |
. . . . . . 7
cyclShift
|
120 | 119 | fveq1i 6192 |
. . . . . 6
cyclShift |
121 | | crctcshwlkn0lem.f |
. . . . . . . . 9
Word |
122 | 121 | adantr 481 |
. . . . . . . 8
..^
Word |
123 | 2, 7 | syl 17 |
. . . . . . . . 9
|
124 | 123 | adantr 481 |
. . . . . . . 8
..^
|
125 | | ltle 10126 |
. . . . . . . . . . . . . . . . 17
|
126 | 29, 125 | syl 17 |
. . . . . . . . . . . . . . . 16
|
127 | 126 | 3impia 1261 |
. . . . . . . . . . . . . . 15
|
128 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . 18
|
129 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . 18
|
130 | 128, 129 | anim12i 590 |
. . . . . . . . . . . . . . . . 17
|
131 | 130 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
|
132 | | nn0sub 11343 |
. . . . . . . . . . . . . . . 16
|
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . 15
|
134 | 127, 133 | mpbid 222 |
. . . . . . . . . . . . . 14
|
135 | 15, 134 | sylbi 207 |
. . . . . . . . . . . . 13
..^
|
136 | | 1nn0 11308 |
. . . . . . . . . . . . . 14
|
137 | 136 | a1i 11 |
. . . . . . . . . . . . 13
..^
|
138 | 135, 137 | nn0addcld 11355 |
. . . . . . . . . . . 12
..^
|
139 | | elnn0uz 11725 |
. . . . . . . . . . . 12
|
140 | 138, 139 | sylib 208 |
. . . . . . . . . . 11
..^
|
141 | | fzoss1 12495 |
. . . . . . . . . . 11
..^ ..^ |
142 | 2, 140, 141 | 3syl 18 |
. . . . . . . . . 10
..^ ..^ |
143 | 142 | sselda 3603 |
. . . . . . . . 9
..^
..^ |
144 | | crctcshwlkn0lem.n |
. . . . . . . . . 10
|
145 | 144 | oveq2i 6661 |
. . . . . . . . 9
..^ ..^ |
146 | 143, 145 | syl6eleq 2711 |
. . . . . . . 8
..^
..^ |
147 | | cshwidxmod 13549 |
. . . . . . . 8
Word
..^ cyclShift |
148 | 122, 124,
146, 147 | syl3anc 1326 |
. . . . . . 7
..^
cyclShift |
149 | 144 | eqcomi 2631 |
. . . . . . . . . 10
|
150 | 149 | oveq2i 6661 |
. . . . . . . . 9
|
151 | | eluzelre 11698 |
. . . . . . . . . . . . . . . . . . 19
|
152 | 151 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
|
153 | 152 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
154 | 27 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
|
155 | 154 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
156 | 153, 155 | readdcld 10069 |
. . . . . . . . . . . . . . . 16
|
157 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . 18
|
158 | 157 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . 17
|
159 | 158 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
160 | 50 | impcom 446 |
. . . . . . . . . . . . . . . . 17
|
161 | 159 | rpred 11872 |
. . . . . . . . . . . . . . . . . 18
|
162 | | simpr3 1069 |
. . . . . . . . . . . . . . . . . 18
|
163 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . 18
|
164 | 153, 155,
161, 162, 163 | lt2addmuld 11282 |
. . . . . . . . . . . . . . . . 17
|
165 | 160, 164 | jca 554 |
. . . . . . . . . . . . . . . 16
|
166 | 156, 159,
165 | jca31 557 |
. . . . . . . . . . . . . . 15
|
167 | 166 | ex 450 |
. . . . . . . . . . . . . 14
|
168 | 24, 167 | syl5bi 232 |
. . . . . . . . . . . . 13
..^ |
169 | 15, 168 | sylbi 207 |
. . . . . . . . . . . 12
..^
..^ |
170 | 2, 169 | syl 17 |
. . . . . . . . . . 11
..^
|
171 | 170 | imp 445 |
. . . . . . . . . 10
..^
|
172 | | 2submod 12731 |
. . . . . . . . . 10
|
173 | 171, 172 | syl 17 |
. . . . . . . . 9
..^
|
174 | 150, 173 | syl5eq 2668 |
. . . . . . . 8
..^
|
175 | 174 | fveq2d 6195 |
. . . . . . 7
..^
|
176 | 148, 175 | eqtrd 2656 |
. . . . . 6
..^
cyclShift |
177 | 120, 176 | syl5eq 2668 |
. . . . 5
..^
|
178 | 177 | fveq2d 6195 |
. . . 4
..^
|
179 | | simp1 1061 |
. . . . . 6
|
180 | | simp2 1062 |
. . . . . 6
|
181 | 179, 180 | eqeq12d 2637 |
. . . . 5
|
182 | | simp3 1063 |
. . . . . 6
|
183 | 179 | sneqd 4189 |
. . . . . 6
|
184 | 182, 183 | eqeq12d 2637 |
. . . . 5
|
185 | 179, 180 | preq12d 4276 |
. . . . . 6
|
186 | 185, 182 | sseq12d 3634 |
. . . . 5
|
187 | 181, 184,
186 | ifpbi123d 1027 |
. . . 4
if-
if- |
188 | 115, 118,
178, 187 | syl3anc 1326 |
. . 3
..^
if-
if- |
189 | 111, 188 | mpbird 247 |
. 2
..^
if- |
190 | 189 | ralrimiva 2966 |
1
..^if- |