# 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 ) ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> W e. Word V )`
` |-  ( ( ( W cyclShift L ) = ( W cyclShift K ) /\ ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) ) -> W e. Word V )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> K e. ( 0 ... ( # ` W ) ) )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( L e. ( 0 ..^ ( # ` W ) ) /\ K e. ( 0 ..^ ( # ` W ) ) /\ K < L ) -> ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( K e. ZZ /\ ( L e. NN0 /\ ( # ` W ) e. NN ) ) -> ( ( # ` W ) - L ) e. RR )`
` |-  ( ( K e. ZZ /\ ( L e. NN0 /\ ( # ` W ) e. NN ) ) -> ( K + ( ( # ` W ) - L ) ) e. RR )`
` |-  ( ( L e. NN0 /\ ( # ` W ) e. NN ) -> ( # ` W ) e. RR )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( K e. ( 0 ... ( # ` W ) ) /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) -> K e. ZZ )`
` |-  ( ( 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 )`
` |-  ( ( K e. ( 0 ... ( # ` W ) ) /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( K + ( ( # ` W ) - L ) ) <_ ( # ` W ) ) -> ( ( # ` W ) - L ) e. ZZ )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( ( K e. ZZ /\ 0 <_ K ) /\ ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) ) -> K e. RR )`
` |-  ( ( L e. NN0 /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> ( ( # ` W ) - L ) e. RR )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) /\ ( K + ( ( # ` W ) - L ) ) e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift ( K + ( ( # ` W ) - L ) ) ) =/= W )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) )`