# Metamath Proof Explorer

## Theorem cshwshashlem1

Description: If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by AV, 19-May-2018) (Revised by AV, 8-Jun-2018) (Revised by AV, 10-Nov-2018)

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

### Proof

Step Hyp Ref Expression
1 cshwshash.0
` |-  ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )`
2 df-ne
` |-  ( ( W ` i ) =/= ( W ` 0 ) <-> -. ( W ` i ) = ( W ` 0 ) )`
3 2 rexbii
` |-  ( E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) <-> E. i e. ( 0 ..^ ( # ` W ) ) -. ( W ` i ) = ( W ` 0 ) )`
4 rexnal
` |-  ( E. i e. ( 0 ..^ ( # ` W ) ) -. ( W ` i ) = ( W ` 0 ) <-> -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )`
5 3 4 bitri
` |-  ( E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) <-> -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )`
6 simpll
` |-  ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> ph )`
7 fzo0ss1
` |-  ( 1 ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) )`
8 fzossfz
` |-  ( 0 ..^ ( # ` W ) ) C_ ( 0 ... ( # ` W ) )`
9 7 8 sstri
` |-  ( 1 ..^ ( # ` W ) ) C_ ( 0 ... ( # ` W ) )`
10 9 sseli
` |-  ( L e. ( 1 ..^ ( # ` W ) ) -> L e. ( 0 ... ( # ` W ) ) )`
` |-  ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> L e. ( 0 ... ( # ` W ) ) )`
12 simpr
` |-  ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> ( W cyclShift L ) = W )`
13 simpll
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) ) -> W e. Word V )`
14 simpr
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( # ` W ) e. Prime )`
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` W ) e. Prime )`
16 elfzelz
` |-  ( L e. ( 0 ... ( # ` W ) ) -> L e. ZZ )`
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) ) -> L e. ZZ )`
18 cshwsidrepswmod0
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) -> ( ( W cyclShift L ) = W -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) )`
19 13 15 17 18 syl3anc
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W cyclShift L ) = W -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) )`
20 19 ex
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( L e. ( 0 ... ( # ` W ) ) -> ( ( W cyclShift L ) = W -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) ) )`
21 20 3imp
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
22 olc
` |-  ( L = ( # ` W ) -> ( L = 0 \/ L = ( # ` W ) ) )`
23 22 a1d
` |-  ( L = ( # ` W ) -> ( ( ( L mod ( # ` W ) ) = 0 /\ ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) ) -> ( L = 0 \/ L = ( # ` W ) ) ) )`
24 fzofzim
` |-  ( ( L =/= ( # ` W ) /\ L e. ( 0 ... ( # ` W ) ) ) -> L e. ( 0 ..^ ( # ` W ) ) )`
25 zmodidfzoimp
` |-  ( L e. ( 0 ..^ ( # ` W ) ) -> ( L mod ( # ` W ) ) = L )`
26 eqtr2
` |-  ( ( ( L mod ( # ` W ) ) = L /\ ( L mod ( # ` W ) ) = 0 ) -> L = 0 )`
27 26 a1d
` |-  ( ( ( L mod ( # ` W ) ) = L /\ ( L mod ( # ` W ) ) = 0 ) -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> L = 0 ) )`
28 27 ex
` |-  ( ( L mod ( # ` W ) ) = L -> ( ( L mod ( # ` W ) ) = 0 -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> L = 0 ) ) )`
29 25 28 syl
` |-  ( L e. ( 0 ..^ ( # ` W ) ) -> ( ( L mod ( # ` W ) ) = 0 -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> L = 0 ) ) )`
30 24 29 syl
` |-  ( ( L =/= ( # ` W ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( L mod ( # ` W ) ) = 0 -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> L = 0 ) ) )`
31 30 expcom
` |-  ( L e. ( 0 ... ( # ` W ) ) -> ( L =/= ( # ` W ) -> ( ( L mod ( # ` W ) ) = 0 -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> L = 0 ) ) ) )`
32 31 com24
` |-  ( L e. ( 0 ... ( # ` W ) ) -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( L mod ( # ` W ) ) = 0 -> ( L =/= ( # ` W ) -> L = 0 ) ) ) )`
33 32 impcom
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( L mod ( # ` W ) ) = 0 -> ( L =/= ( # ` W ) -> L = 0 ) ) )`
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( ( L mod ( # ` W ) ) = 0 -> ( L =/= ( # ` W ) -> L = 0 ) ) )`
35 34 impcom
` |-  ( ( ( L mod ( # ` W ) ) = 0 /\ ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) ) -> ( L =/= ( # ` W ) -> L = 0 ) )`
36 35 impcom
` |-  ( ( L =/= ( # ` W ) /\ ( ( L mod ( # ` W ) ) = 0 /\ ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) ) ) -> L = 0 )`
37 36 orcd
` |-  ( ( L =/= ( # ` W ) /\ ( ( L mod ( # ` W ) ) = 0 /\ ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) ) ) -> ( L = 0 \/ L = ( # ` W ) ) )`
38 37 ex
` |-  ( L =/= ( # ` W ) -> ( ( ( L mod ( # ` W ) ) = 0 /\ ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) ) -> ( L = 0 \/ L = ( # ` W ) ) ) )`
39 23 38 pm2.61ine
` |-  ( ( ( L mod ( # ` W ) ) = 0 /\ ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) ) -> ( L = 0 \/ L = ( # ` W ) ) )`
40 39 orcd
` |-  ( ( ( L mod ( # ` W ) ) = 0 /\ ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) ) -> ( ( L = 0 \/ L = ( # ` W ) ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
41 df-3or
` |-  ( ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) <-> ( ( L = 0 \/ L = ( # ` W ) ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
42 40 41 sylibr
` |-  ( ( ( L mod ( # ` W ) ) = 0 /\ ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) ) -> ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
43 42 ex
` |-  ( ( L mod ( # ` W ) ) = 0 -> ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) )`
44 3mix3
` |-  ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) -> ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
45 44 a1d
` |-  ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) -> ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) )`
46 43 45 jaoi
` |-  ( ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) )`
47 21 46 mpcom
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
48 1 47 syl3an1
` |-  ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
49 3mix1
` |-  ( L = 0 -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
50 49 a1d
` |-  ( L = 0 -> ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )`
51 3mix2
` |-  ( L = ( # ` W ) -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
52 51 a1d
` |-  ( L = ( # ` W ) -> ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )`
53 repswsymballbi
` |-  ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
55 1 54 syl
` |-  ( ph -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
` |-  ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
57 56 biimpa
` |-  ( ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) /\ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )`
58 57 3mix3d
` |-  ( ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) /\ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
59 58 expcom
` |-  ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) -> ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )`
60 50 52 59 3jaoi
` |-  ( ( L = 0 \/ L = ( # ` W ) \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )`
61 48 60 mpcom
` |-  ( ( ph /\ L e. ( 0 ... ( # ` W ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
62 6 11 12 61 syl3anc
` |-  ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
63 elfzo1
` |-  ( L e. ( 1 ..^ ( # ` W ) ) <-> ( L e. NN /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) )`
64 nnne0
` |-  ( L e. NN -> L =/= 0 )`
65 df-ne
` |-  ( L =/= 0 <-> -. L = 0 )`
66 pm2.21
` |-  ( -. L = 0 -> ( L = 0 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
67 65 66 sylbi
` |-  ( L =/= 0 -> ( L = 0 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
68 64 67 syl
` |-  ( L e. NN -> ( L = 0 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
` |-  ( ( L e. NN /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> ( L = 0 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
70 63 69 sylbi
` |-  ( L e. ( 1 ..^ ( # ` W ) ) -> ( L = 0 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
` |-  ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> ( L = 0 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
72 71 com12
` |-  ( L = 0 -> ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
73 nnre
` |-  ( L e. NN -> L e. RR )`
74 ltne
` |-  ( ( L e. RR /\ L < ( # ` W ) ) -> ( # ` W ) =/= L )`
75 73 74 sylan
` |-  ( ( L e. NN /\ L < ( # ` W ) ) -> ( # ` W ) =/= L )`
76 df-ne
` |-  ( ( # ` W ) =/= L <-> -. ( # ` W ) = L )`
77 eqcom
` |-  ( L = ( # ` W ) <-> ( # ` W ) = L )`
78 pm2.21
` |-  ( -. ( # ` W ) = L -> ( ( # ` W ) = L -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
79 77 78 syl5bi
` |-  ( -. ( # ` W ) = L -> ( L = ( # ` W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
80 76 79 sylbi
` |-  ( ( # ` W ) =/= L -> ( L = ( # ` W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
81 75 80 syl
` |-  ( ( L e. NN /\ L < ( # ` W ) ) -> ( L = ( # ` W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
` |-  ( ( L e. NN /\ ( # ` W ) e. NN /\ L < ( # ` W ) ) -> ( L = ( # ` W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
83 63 82 sylbi
` |-  ( L e. ( 1 ..^ ( # ` W ) ) -> ( L = ( # ` W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
` |-  ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> ( L = ( # ` W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
85 84 com12
` |-  ( L = ( # ` W ) -> ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
86 ax-1
` |-  ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) -> ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
87 72 85 86 3jaoi
` |-  ( ( L = 0 \/ L = ( # ` W ) \/ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) -> ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
88 62 87 mpcom
` |-  ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )`
89 88 pm2.24d
` |-  ( ( ( ph /\ L e. ( 1 ..^ ( # ` W ) ) ) /\ ( W cyclShift L ) = W ) -> ( -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) -> ( W cyclShift L ) =/= W ) )`
90 89 exp31
` |-  ( ph -> ( L e. ( 1 ..^ ( # ` W ) ) -> ( ( W cyclShift L ) = W -> ( -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) -> ( W cyclShift L ) =/= W ) ) ) )`
91 90 com34
` |-  ( ph -> ( L e. ( 1 ..^ ( # ` W ) ) -> ( -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) -> ( ( W cyclShift L ) = W -> ( W cyclShift L ) =/= W ) ) ) )`
92 91 com23
` |-  ( ph -> ( -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) -> ( L e. ( 1 ..^ ( # ` W ) ) -> ( ( W cyclShift L ) = W -> ( W cyclShift L ) =/= W ) ) ) )`
93 5 92 syl5bi
` |-  ( ph -> ( E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) -> ( L e. ( 1 ..^ ( # ` W ) ) -> ( ( W cyclShift L ) = W -> ( W cyclShift L ) =/= W ) ) ) )`
94 93 3imp
` |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) /\ L e. ( 1 ..^ ( # ` W ) ) ) -> ( ( W cyclShift L ) = W -> ( W cyclShift L ) =/= W ) )`
95 94 com12
` |-  ( ( W cyclShift L ) = W -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) /\ L e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift L ) =/= W ) )`
96 ax-1
` |-  ( ( W cyclShift L ) =/= W -> ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) /\ L e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift L ) =/= W ) )`
97 95 96 pm2.61ine
` |-  ( ( ph /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) /\ L e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift L ) =/= W )`