Metamath Proof Explorer


Theorem crctcshwlkn0lem7

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
crctcshwlkn0lem.e φ P N = P 0
Assertion crctcshwlkn0lem7 φ j 0 ..^ 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 crctcshwlkn0lem.e φ P N = P 0
8 1 2 3 4 5 6 crctcshwlkn0lem4 φ j 0 ..^ N S if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
9 eqidd φ N S = N S
10 1 2 3 4 5 6 7 crctcshwlkn0lem6 φ N S = N S if- Q N S = Q N - S + 1 I H N S = Q N S Q N S Q N - S + 1 I H N S
11 9 10 mpdan φ if- Q N S = Q N - S + 1 I H N S = Q N S Q N S Q N - S + 1 I H N S
12 ovex N S V
13 wkslem1 j = N S if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j if- Q N S = Q N - S + 1 I H N S = Q N S Q N S Q N - S + 1 I H N S
14 12 13 ralsn j N S if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j if- Q N S = Q N - S + 1 I H N S = Q N S Q N S Q N - S + 1 I H N S
15 11 14 sylibr φ j N S if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
16 ralunb j 0 ..^ N S N S if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j j 0 ..^ N S if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j j N S if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
17 8 15 16 sylanbrc φ j 0 ..^ N S N S if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
18 elfzo1 S 1 ..^ N S N S < N
19 nnz N N
20 nnz S S
21 zsubcl N S N S
22 19 20 21 syl2anr S N N S
23 22 3adant3 S N S < N N S
24 nnre S S
25 nnre N N
26 posdif S N S < N 0 < N S
27 0re 0
28 resubcl N S N S
29 28 ancoms S N N S
30 ltle 0 N S 0 < N S 0 N S
31 27 29 30 sylancr S N 0 < N S 0 N S
32 26 31 sylbid S N S < N 0 N S
33 24 25 32 syl2an S N S < N 0 N S
34 33 3impia S N S < N 0 N S
35 elnn0z N S 0 N S 0 N S
36 23 34 35 sylanbrc S N S < N N S 0
37 elnn0uz N S 0 N S 0
38 36 37 sylib S N S < N N S 0
39 fzosplitsn N S 0 0 ..^ N - S + 1 = 0 ..^ N S N S
40 38 39 syl S N S < N 0 ..^ N - S + 1 = 0 ..^ N S N S
41 18 40 sylbi S 1 ..^ N 0 ..^ N - S + 1 = 0 ..^ N S N S
42 1 41 syl φ 0 ..^ N - S + 1 = 0 ..^ N S N S
43 17 42 raleqtrrdv φ j 0 ..^ N - S + 1 if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
44 1 2 3 4 5 6 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
45 ralunb j 0 ..^ N - S + 1 N - S + 1 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j j 0 ..^ N - S + 1 if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j j N - S + 1 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
46 43 44 45 sylanbrc φ j 0 ..^ N - S + 1 N - S + 1 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
47 nnsub S N S < N N S
48 47 biimp3a S N S < N N S
49 nnnn0 N S N S 0
50 peano2nn0 N S 0 N - S + 1 0
51 48 49 50 3syl S N S < N N - S + 1 0
52 nnnn0 N N 0
53 52 3ad2ant2 S N S < N N 0
54 25 anim1i N S N S
55 54 ancoms S N N S
56 crctcshwlkn0lem1 N S N - S + 1 N
57 55 56 syl S N N - S + 1 N
58 57 3adant3 S N S < N N - S + 1 N
59 elfz2nn0 N - S + 1 0 N N - S + 1 0 N 0 N - S + 1 N
60 51 53 58 59 syl3anbrc S N S < N N - S + 1 0 N
61 18 60 sylbi S 1 ..^ N N - S + 1 0 N
62 fzosplit N - S + 1 0 N 0 ..^ N = 0 ..^ N - S + 1 N - S + 1 ..^ N
63 1 61 62 3syl φ 0 ..^ N = 0 ..^ N - S + 1 N - S + 1 ..^ N
64 46 63 raleqtrrdv φ j 0 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j