Metamath Proof Explorer

Theorem cshwshashlem2

Description: If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018) (Revised by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Hypothesis cshwshash.0 
|- ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )
Assertion cshwshashlem2 
|- ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )

Proof

Step Hyp Ref Expression
1 cshwshash.0 
 |-  ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )
2 oveq1 
 |-  ( ( W cyclShift L ) = ( W cyclShift K ) -> ( ( W cyclShift L ) cyclShift ( ( # ` W ) - L ) ) = ( ( W cyclShift K ) cyclShift ( ( # ` W ) - L ) ) )
3 2 eqcomd 
 |-  ( ( W cyclShift L ) = ( W cyclShift K ) -> ( ( W cyclShift K ) cyclShift ( ( # ` W ) - L ) ) = ( ( W cyclShift L ) cyclShift ( ( # ` W ) - L ) ) )
4 3 ad2antrr 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( ( W cyclShift K ) cyclShift ( ( # ` W ) - L ) ) = ( ( W cyclShift L ) cyclShift ( ( # ` W ) - L ) ) )
5 1 simpld 
 |-  ( ph -> W e. Word V )
6 5 adantr 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> W e. Word V )
7 6 adantl 
 |-  ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) -> W e. Word V )
8 7 adantr 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> W e. Word V )
9 elfzofz 
 |-  ( K e. ( 0 ..^ ( # ` W ) ) -> K e. ( 0 ... ( # ` W ) ) )
10 9 3ad2ant2 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> K e. ( 0 ... ( # ` W ) ) )
11 10 adantl 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> K e. ( 0 ... ( # ` W ) ) )
12 elfzofz 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) -> L e. ( 0 ... ( # ` W ) ) )
13 fznn0sub2 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) )
14 12 13 syl 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) -> ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) )
15 14 3ad2ant1 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) )
16 15 adantl 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) )
17 elfzo0 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) <-> ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) )
18 zre 
 |-  ( K e. ZZ -> K e. RR )
19 18 adantr 
 |-  ( ( K e. ZZ /\ ( L e. NN0 /\ ( # ` W ) e. NN ) ) -> K e. RR )
20 nnre 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR )
21 nn0re 
 |-  ( L e. NN0 -> L e. RR )
22 resubcl 
 |-  ( ( ( # ` W ) e. RR /\ L e. RR ) -> ( ( # ` W ) - L ) e. RR )
23 20 21 22 syl2anr 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN ) -> ( ( # ` W ) - L ) e. RR )
24 23 adantl 
 |-  ( ( K e. ZZ /\ ( L e. NN0 /\ ( # ` W ) e. NN ) ) -> ( ( # ` W ) - L ) e. RR )
25 19 24 readdcld 
 |-  ( ( K e. ZZ /\ ( L e. NN0 /\ ( # ` W ) e. NN ) ) -> ( K + ( ( # ` W ) - L ) ) e. RR )
26 20 adantl 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN ) -> ( # ` W ) e. RR )
27 26 adantl 
 |-  ( ( K e. ZZ /\ ( L e. NN0 /\ ( # ` W ) e. NN ) ) -> ( # ` W ) e. RR )
28 25 27 jca 
 |-  ( ( K e. ZZ /\ ( L e. NN0 /\ ( # ` W ) e. NN ) ) -> ( ( K + ( ( # ` W ) - L ) ) e. RR /\ ( # ` W ) e. RR ) )
29 28 ex 
 |-  ( K e. ZZ -> ( ( L e. NN0 /\ ( # ` W ) e. NN ) -> ( ( K + ( ( # ` W ) - L ) ) e. RR /\ ( # ` W ) e. RR ) ) )
30 elfzoelz 
 |-  ( K e. ( 0 ..^ ( # ` W ) ) -> K e. ZZ )
31 29 30 syl11 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN ) -> ( K e. ( 0 ..^ ( # ` W ) ) -> ( ( K + ( ( # ` W ) - L ) ) e. RR /\ ( # ` W ) e. RR ) ) )
32 31 3adant3 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> ( K e. ( 0 ..^ ( # ` W ) ) -> ( ( K + ( ( # ` W ) - L ) ) e. RR /\ ( # ` W ) e. RR ) ) )
33 17 32 sylbi 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) -> ( K e. ( 0 ..^ ( # ` W ) ) -> ( ( K + ( ( # ` W ) - L ) ) e. RR /\ ( # ` W ) e. RR ) ) )
34 33 imp 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) ) -> ( ( K + ( ( # ` W ) - L ) ) e. RR /\ ( # ` W ) e. RR ) )
35 34 3adant3 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( ( K + ( ( # ` W ) - L ) ) e. RR /\ ( # ` W ) e. RR ) )
36 fzonmapblen 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( K + ( ( # ` W ) - L ) ) < ( # ` W ) )
37 ltle 
 |-  ( ( ( K + ( ( # ` W ) - L ) ) e. RR /\ ( # ` W ) e. RR ) -> ( ( K + ( ( # ` W ) - L ) ) < ( # ` W ) -> ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) )
38 35 36 37 sylc 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) )
39 38 adantl 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) )
40 simpl 
 |-  ( ( W e. Word V /\ ( K e. ( 0 ... ( # ` W ) ) /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) ) -> W e. Word V )
41 elfzelz 
 |-  ( K e. ( 0 ... ( # ` W ) ) -> K e. ZZ )
42 41 3ad2ant1 
 |-  ( ( K e. ( 0 ... ( # ` W ) ) /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) -> K e. ZZ )
43 42 adantl 
 |-  ( ( W e. Word V /\ ( K e. ( 0 ... ( # ` W ) ) /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) ) -> K e. ZZ )
44 elfzelz 
 |-  ( ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) -> ( ( # ` W ) - L ) e. ZZ )
45 44 3ad2ant2 
 |-  ( ( K e. ( 0 ... ( # ` W ) ) /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) -> ( ( # ` W ) - L ) e. ZZ )
46 45 adantl 
 |-  ( ( W e. Word V /\ ( K e. ( 0 ... ( # ` W ) ) /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) ) -> ( ( # ` W ) - L ) e. ZZ )
47 2cshw 
 |-  ( ( W e. Word V /\ K e. ZZ /\ ( ( # ` W ) - L ) e. ZZ ) -> ( ( W cyclShift K ) cyclShift ( ( # ` W ) - L ) ) = ( W cyclShift ( K + ( ( # ` W ) - L ) ) ) )
48 40 43 46 47 syl3anc 
 |-  ( ( W e. Word V /\ ( K e. ( 0 ... ( # ` W ) ) /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) ) -> ( ( W cyclShift K ) cyclShift ( ( # ` W ) - L ) ) = ( W cyclShift ( K + ( ( # ` W ) - L ) ) ) )
49 8 11 16 39 48 syl13anc 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( ( W cyclShift K ) cyclShift ( ( # ` W ) - L ) ) = ( W cyclShift ( K + ( ( # ` W ) - L ) ) ) )
50 12 3ad2ant1 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> L e. ( 0 ... ( # ` W ) ) )
51 elfzelz 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> L e. ZZ )
52 2cshwid 
 |-  ( ( W e. Word V /\ L e. ZZ ) -> ( ( W cyclShift L ) cyclShift ( ( # ` W ) - L ) ) = W )
53 51 52 sylan2 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W cyclShift L ) cyclShift ( ( # ` W ) - L ) ) = W )
54 7 50 53 syl2an 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( ( W cyclShift L ) cyclShift ( ( # ` W ) - L ) ) = W )
55 4 49 54 3eqtr3d 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( W cyclShift ( K + ( ( # ` W ) - L ) ) ) = W )
56 simplrl 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ph )
57 simplrr 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) )
58 3simpa 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> ( L e. NN0 /\ ( # ` W ) e. NN ) )
59 17 58 sylbi 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) -> ( L e. NN0 /\ ( # ` W ) e. NN ) )
60 nnz 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. ZZ )
61 nn0z 
 |-  ( L e. NN0 -> L e. ZZ )
62 zsubcl 
 |-  ( ( ( # ` W ) e. ZZ /\ L e. ZZ ) -> ( ( # ` W ) - L ) e. ZZ )
63 60 61 62 syl2anr 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN ) -> ( ( # ` W ) - L ) e. ZZ )
64 63 anim1ci 
 |-  ( ( ( L e. NN0 /\ ( # ` W ) e. NN ) /\ K e. ZZ ) -> ( K e. ZZ /\ ( ( # ` W ) - L ) e. ZZ ) )
65 zaddcl 
 |-  ( ( K e. ZZ /\ ( ( # ` W ) - L ) e. ZZ ) -> ( K + ( ( # ` W ) - L ) ) e. ZZ )
66 64 65 syl 
 |-  ( ( ( L e. NN0 /\ ( # ` W ) e. NN ) /\ K e. ZZ ) -> ( K + ( ( # ` W ) - L ) ) e. ZZ )
67 59 30 66 syl2an 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) ) -> ( K + ( ( # ` W ) - L ) ) e. ZZ )
68 67 3adant3 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( K + ( ( # ` W ) - L ) ) e. ZZ )
69 elfzo0 
 |-  ( K e. ( 0 ..^ ( # ` W ) ) <-> ( K e. NN0 /\ ( # ` W ) e. NN /\ K < ( # ` W ) ) )
70 elnn0z 
 |-  ( K e. NN0 <-> ( K e. ZZ /\ 0 <_ K ) )
71 18 ad2antrr 
 |-  ( ( ( K e. ZZ /\ 0 <_ K ) /\ ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) ) -> K e. RR )
72 23 3adant3 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> ( ( # ` W ) - L ) e. RR )
73 72 adantl 
 |-  ( ( ( K e. ZZ /\ 0 <_ K ) /\ ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) ) -> ( ( # ` W ) - L ) e. RR )
74 simplr 
 |-  ( ( ( K e. ZZ /\ 0 <_ K ) /\ ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) ) -> 0 <_ K )
75 posdif 
 |-  ( ( L e. RR /\ ( # ` W ) e. RR ) -> ( L < ( # ` W ) <-> 0 < ( ( # ` W ) - L ) ) )
76 21 20 75 syl2an 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN ) -> ( L < ( # ` W ) <-> 0 < ( ( # ` W ) - L ) ) )
77 76 biimp3a 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> 0 < ( ( # ` W ) - L ) )
78 77 adantl 
 |-  ( ( ( K e. ZZ /\ 0 <_ K ) /\ ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) ) -> 0 < ( ( # ` W ) - L ) )
79 71 73 74 78 addgegt0d 
 |-  ( ( ( K e. ZZ /\ 0 <_ K ) /\ ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) ) -> 0 < ( K + ( ( # ` W ) - L ) ) )
80 79 ex 
 |-  ( ( K e. ZZ /\ 0 <_ K ) -> ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> 0 < ( K + ( ( # ` W ) - L ) ) ) )
81 70 80 sylbi 
 |-  ( K e. NN0 -> ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> 0 < ( K + ( ( # ` W ) - L ) ) ) )
82 81 3ad2ant1 
 |-  ( ( K e. NN0 /\ ( # ` W ) e. NN /\ K < ( # ` W ) ) -> ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> 0 < ( K + ( ( # ` W ) - L ) ) ) )
83 69 82 sylbi 
 |-  ( K e. ( 0 ..^ ( # ` W ) ) -> ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> 0 < ( K + ( ( # ` W ) - L ) ) ) )
84 83 com12 
 |-  ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> ( K e. ( 0 ..^ ( # ` W ) ) -> 0 < ( K + ( ( # ` W ) - L ) ) ) )
85 17 84 sylbi 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) -> ( K e. ( 0 ..^ ( # ` W ) ) -> 0 < ( K + ( ( # ` W ) - L ) ) ) )
86 85 imp 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) ) -> 0 < ( K + ( ( # ` W ) - L ) ) )
87 86 3adant3 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> 0 < ( K + ( ( # ` W ) - L ) ) )
88 elnnz 
 |-  ( ( K + ( ( # ` W ) - L ) ) e. NN <-> ( ( K + ( ( # ` W ) - L ) ) e. ZZ /\ 0 < ( K + ( ( # ` W ) - L ) ) ) )
89 68 87 88 sylanbrc 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( K + ( ( # ` W ) - L ) ) e. NN )
90 17 simp2bi 
 |-  ( L e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. NN )
91 90 3ad2ant1 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( # ` W ) e. NN )
92 elfzo1 
 |-  ( ( K + ( ( # ` W ) - L ) ) e. ( 1 ..^ ( # ` W ) ) <-> ( ( K + ( ( # ` W ) - L ) ) e. NN /\ ( # ` W ) e. NN /\ ( K + ( ( # ` W ) - L ) ) < ( # ` W ) ) )
93 89 91 36 92 syl3anbrc 
 |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( K + ( ( # ` W ) - L ) ) e. ( 1 ..^ ( # ` W ) ) )
94 93 adantl 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( K + ( ( # ` W ) - L ) ) e. ( 1 ..^ ( # ` W ) ) )
95 1 cshwshashlem1 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) /\ ( K + ( ( # ` W ) - L ) ) e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift ( K + ( ( # ` W ) - L ) ) ) =/= W )
96 56 57 94 95 syl3anc 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( W cyclShift ( K + ( ( # ` W ) - L ) ) ) =/= W )
97 55 96 pm2.21ddne 
 |-  ( ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) /\ ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) ) -> ( W cyclShift L ) =/= ( W cyclShift K ) )
98 97 exp31 
 |-  ( ( W cyclShift L ) = ( W cyclShift K ) -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) ) )
99 2a1 
 |-  ( ( W cyclShift L ) =/= ( W cyclShift K ) -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) ) )
100 98 99 pm2.61ine 
 |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )