Metamath Proof Explorer


Theorem crctcshwlkn0lem5

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s φ S 1 ..^ N
crctcshwlkn0lem.q Q = x 0 N if x N S P x + S P x + S - N
crctcshwlkn0lem.h H = F cyclShift S
crctcshwlkn0lem.n N = F
crctcshwlkn0lem.f φ F Word A
crctcshwlkn0lem.p φ i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i
Assertion crctcshwlkn0lem5 φ j N - S + 1 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j

Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s φ S 1 ..^ N
2 crctcshwlkn0lem.q Q = x 0 N if x N S P x + S P x + S - N
3 crctcshwlkn0lem.h H = F cyclShift S
4 crctcshwlkn0lem.n N = F
5 crctcshwlkn0lem.f φ F Word A
6 crctcshwlkn0lem.p φ i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i
7 elfzoelz j N - S + 1 ..^ N j
8 7 zcnd j N - S + 1 ..^ N j
9 8 adantl S 1 ..^ N j N - S + 1 ..^ N j
10 1cnd S 1 ..^ N j N - S + 1 ..^ N 1
11 elfzoelz S 1 ..^ N S
12 11 zcnd S 1 ..^ N S
13 12 adantr S 1 ..^ N j N - S + 1 ..^ N S
14 elfzoel2 S 1 ..^ N N
15 14 zcnd S 1 ..^ N N
16 15 adantr S 1 ..^ N j N - S + 1 ..^ N N
17 9 10 13 16 2addsubd S 1 ..^ N j N - S + 1 ..^ N j + 1 + S - N = j + S - N + 1
18 17 eqcomd S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N
19 elfzo1 S 1 ..^ N S N S < N
20 nnz N N
21 20 3ad2ant2 S N S < N N
22 21 adantr S N S < N j N - S + 1 ..^ N N
23 7 adantl S N S < N j N - S + 1 ..^ N j
24 nnz S S
25 24 3ad2ant1 S N S < N S
26 25 adantr S N S < N j N - S + 1 ..^ N S
27 23 26 zaddcld S N S < N j N - S + 1 ..^ N j + S
28 elfzo2 j N - S + 1 ..^ N j N - S + 1 N j < N
29 eluz2 j N - S + 1 N - S + 1 j N - S + 1 j
30 zre j j
31 nnre S S
32 nnre N N
33 31 32 anim12i S N S N
34 simplr S N j N
35 simpll S N j S
36 34 35 resubcld S N j N S
37 36 lep1d S N j N S N - S + 1
38 1red S N j 1
39 36 38 readdcld S N j N - S + 1
40 simpr S N j j
41 letr N S N - S + 1 j N S N - S + 1 N - S + 1 j N S j
42 36 39 40 41 syl3anc S N j N S N - S + 1 N - S + 1 j N S j
43 37 42 mpand S N j N - S + 1 j N S j
44 34 35 40 lesubaddd S N j N S j N j + S
45 43 44 sylibd S N j N - S + 1 j N j + S
46 45 ex S N j N - S + 1 j N j + S
47 33 46 syl S N j N - S + 1 j N j + S
48 47 3adant3 S N S < N j N - S + 1 j N j + S
49 30 48 syl5com j S N S < N N - S + 1 j N j + S
50 49 com23 j N - S + 1 j S N S < N N j + S
51 50 imp j N - S + 1 j S N S < N N j + S
52 51 3adant1 N - S + 1 j N - S + 1 j S N S < N N j + S
53 29 52 sylbi j N - S + 1 S N S < N N j + S
54 53 3ad2ant1 j N - S + 1 N j < N S N S < N N j + S
55 54 com12 S N S < N j N - S + 1 N j < N N j + S
56 28 55 syl5bi S N S < N j N - S + 1 ..^ N N j + S
57 56 imp S N S < N j N - S + 1 ..^ N N j + S
58 eluz2 j + S N N j + S N j + S
59 22 27 57 58 syl3anbrc S N S < N j N - S + 1 ..^ N j + S N
60 uznn0sub j + S N j + S - N 0
61 59 60 syl S N S < N j N - S + 1 ..^ N j + S - N 0
62 simpl2 S N S < N j N - S + 1 ..^ N N
63 30 adantl S N j j
64 simpll S N j S
65 ax-1 N S N
66 65 imdistanri S N N N
67 66 adantr S N j N N
68 lt2add j S N N j < N S < N j + S < N + N
69 63 64 67 68 syl21anc S N j j < N S < N j + S < N + N
70 63 64 readdcld S N j j + S
71 simplr S N j N
72 70 71 71 ltsubaddd S N j j + S - N < N j + S < N + N
73 69 72 sylibrd S N j j < N S < N j + S - N < N
74 73 ex S N j j < N S < N j + S - N < N
75 74 com23 S N j < N S < N j j + S - N < N
76 75 expcomd S N S < N j < N j j + S - N < N
77 33 76 syl S N S < N j < N j j + S - N < N
78 77 3impia S N S < N j < N j j + S - N < N
79 78 com13 j j < N S N S < N j + S - N < N
80 79 3ad2ant2 N - S + 1 j N - S + 1 j j < N S N S < N j + S - N < N
81 29 80 sylbi j N - S + 1 j < N S N S < N j + S - N < N
82 81 imp j N - S + 1 j < N S N S < N j + S - N < N
83 82 3adant2 j N - S + 1 N j < N S N S < N j + S - N < N
84 28 83 sylbi j N - S + 1 ..^ N S N S < N j + S - N < N
85 84 impcom S N S < N j N - S + 1 ..^ N j + S - N < N
86 61 62 85 3jca S N S < N j N - S + 1 ..^ N j + S - N 0 N j + S - N < N
87 19 86 sylanb S 1 ..^ N j N - S + 1 ..^ N j + S - N 0 N j + S - N < N
88 elfzo0 j + S - N 0 ..^ N j + S - N 0 N j + S - N < N
89 87 88 sylibr S 1 ..^ N j N - S + 1 ..^ N j + S - N 0 ..^ N
90 89 adantr S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N j + S - N 0 ..^ N
91 fveq2 i = j + S - N P i = P j + S - N
92 91 adantl S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N P i = P j + S - N
93 fvoveq1 i = j + S - N P i + 1 = P j + S - N + 1
94 simpr S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N j + S - N + 1 = j + 1 + S - N
95 94 fveq2d S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N P j + S - N + 1 = P j + 1 + S - N
96 93 95 sylan9eqr S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N P i + 1 = P j + 1 + S - N
97 92 96 eqeq12d S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N P i = P i + 1 P j + S - N = P j + 1 + S - N
98 2fveq3 i = j + S - N I F i = I F j + S - N
99 91 sneqd i = j + S - N P i = P j + S - N
100 98 99 eqeq12d i = j + S - N I F i = P i I F j + S - N = P j + S - N
101 100 adantl S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N I F i = P i I F j + S - N = P j + S - N
102 92 96 preq12d S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N P i P i + 1 = P j + S - N P j + 1 + S - N
103 simpr S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N i = j + S - N
104 103 fveq2d S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N F i = F j + S - N
105 104 fveq2d S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N I F i = I F j + S - N
106 102 105 sseq12d S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N P i P i + 1 I F i P j + S - N P j + 1 + S - N I F j + S - N
107 97 101 106 ifpbi123d S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i = j + S - N if- P i = P i + 1 I F i = P i P i P i + 1 I F i if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
108 90 107 rspcdv S 1 ..^ N j N - S + 1 ..^ N j + S - N + 1 = j + 1 + S - N i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
109 18 108 mpdan S 1 ..^ N j N - S + 1 ..^ N i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
110 1 109 sylan φ j N - S + 1 ..^ N i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
111 110 ex φ j N - S + 1 ..^ N i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
112 6 111 mpid φ j N - S + 1 ..^ N if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
113 112 imp φ j N - S + 1 ..^ N if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
114 elfzofz j N - S + 1 ..^ N j N - S + 1 N
115 1 2 crctcshwlkn0lem3 φ j N - S + 1 N Q j = P j + S - N
116 114 115 sylan2 φ j N - S + 1 ..^ N Q j = P j + S - N
117 fzofzp1 j N - S + 1 ..^ N j + 1 N - S + 1 N
118 1 2 crctcshwlkn0lem3 φ j + 1 N - S + 1 N Q j + 1 = P j + 1 + S - N
119 117 118 sylan2 φ j N - S + 1 ..^ N Q j + 1 = P j + 1 + S - N
120 3 fveq1i H j = F cyclShift S j
121 5 adantr φ j N - S + 1 ..^ N F Word A
122 1 11 syl φ S
123 122 adantr φ j N - S + 1 ..^ N S
124 ltle S N S < N S N
125 33 124 syl S N S < N S N
126 125 3impia S N S < N S N
127 nnnn0 S S 0
128 nnnn0 N N 0
129 127 128 anim12i S N S 0 N 0
130 129 3adant3 S N S < N S 0 N 0
131 nn0sub S 0 N 0 S N N S 0
132 130 131 syl S N S < N S N N S 0
133 126 132 mpbid S N S < N N S 0
134 19 133 sylbi S 1 ..^ N N S 0
135 1nn0 1 0
136 135 a1i S 1 ..^ N 1 0
137 134 136 nn0addcld S 1 ..^ N N - S + 1 0
138 elnn0uz N - S + 1 0 N - S + 1 0
139 137 138 sylib S 1 ..^ N N - S + 1 0
140 fzoss1 N - S + 1 0 N - S + 1 ..^ N 0 ..^ N
141 1 139 140 3syl φ N - S + 1 ..^ N 0 ..^ N
142 141 sselda φ j N - S + 1 ..^ N j 0 ..^ N
143 4 oveq2i 0 ..^ N = 0 ..^ F
144 142 143 syl6eleq φ j N - S + 1 ..^ N j 0 ..^ F
145 cshwidxmod F Word A S j 0 ..^ F F cyclShift S j = F j + S mod F
146 121 123 144 145 syl3anc φ j N - S + 1 ..^ N F cyclShift S j = F j + S mod F
147 4 eqcomi F = N
148 147 oveq2i j + S mod F = j + S mod N
149 eluzelre j N - S + 1 j
150 149 3ad2ant1 j N - S + 1 N j < N j
151 150 adantl S N S < N j N - S + 1 N j < N j
152 31 3ad2ant1 S N S < N S
153 152 adantr S N S < N j N - S + 1 N j < N S
154 151 153 readdcld S N S < N j N - S + 1 N j < N j + S
155 nnrp N N +
156 155 3ad2ant2 S N S < N N +
157 156 adantr S N S < N j N - S + 1 N j < N N +
158 54 impcom S N S < N j N - S + 1 N j < N N j + S
159 157 rpred S N S < N j N - S + 1 N j < N N
160 simpr3 S N S < N j N - S + 1 N j < N j < N
161 simpl3 S N S < N j N - S + 1 N j < N S < N
162 151 153 159 160 161 lt2addmuld S N S < N j N - S + 1 N j < N j + S < 2 N
163 158 162 jca S N S < N j N - S + 1 N j < N N j + S j + S < 2 N
164 154 157 163 jca31 S N S < N j N - S + 1 N j < N j + S N + N j + S j + S < 2 N
165 164 ex S N S < N j N - S + 1 N j < N j + S N + N j + S j + S < 2 N
166 28 165 syl5bi S N S < N j N - S + 1 ..^ N j + S N + N j + S j + S < 2 N
167 19 166 sylbi S 1 ..^ N j N - S + 1 ..^ N j + S N + N j + S j + S < 2 N
168 1 167 syl φ j N - S + 1 ..^ N j + S N + N j + S j + S < 2 N
169 168 imp φ j N - S + 1 ..^ N j + S N + N j + S j + S < 2 N
170 2submod j + S N + N j + S j + S < 2 N j + S mod N = j + S - N
171 169 170 syl φ j N - S + 1 ..^ N j + S mod N = j + S - N
172 148 171 syl5eq φ j N - S + 1 ..^ N j + S mod F = j + S - N
173 172 fveq2d φ j N - S + 1 ..^ N F j + S mod F = F j + S - N
174 146 173 eqtrd φ j N - S + 1 ..^ N F cyclShift S j = F j + S - N
175 120 174 syl5eq φ j N - S + 1 ..^ N H j = F j + S - N
176 175 fveq2d φ j N - S + 1 ..^ N I H j = I F j + S - N
177 simp1 Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N Q j = P j + S - N
178 simp2 Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N Q j + 1 = P j + 1 + S - N
179 177 178 eqeq12d Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N Q j = Q j + 1 P j + S - N = P j + 1 + S - N
180 simp3 Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N I H j = I F j + S - N
181 177 sneqd Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N Q j = P j + S - N
182 180 181 eqeq12d Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N I H j = Q j I F j + S - N = P j + S - N
183 177 178 preq12d Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N Q j Q j + 1 = P j + S - N P j + 1 + S - N
184 183 180 sseq12d Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N Q j Q j + 1 I H j P j + S - N P j + 1 + S - N I F j + S - N
185 179 182 184 ifpbi123d Q j = P j + S - N Q j + 1 = P j + 1 + S - N I H j = I F j + S - N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
186 116 119 176 185 syl3anc φ j N - S + 1 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j if- P j + S - N = P j + 1 + S - N I F j + S - N = P j + S - N P j + S - N P j + 1 + S - N I F j + S - N
187 113 186 mpbird φ j N - S + 1 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
188 187 ralrimiva φ j N - S + 1 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j