This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )
11 10 ad2antlr 
 |-  ( ( ( 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 )
15 14 adantr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` W ) e. Prime )
16 elfzelz 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> L e. ZZ )
17 16 adantl 
 |-  ( ( ( 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 ) ) )
34 33 3adant3 
 |-  ( ( ( 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 ) ) )
54 53 adantr 
 |-  ( ( 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 ) ) )
56 55 3ad2ant1 
 |-  ( ( 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 ) ) )
69 68 3ad2ant1 
 |-  ( ( 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 ) ) )
71 70 ad2antlr 
 |-  ( ( ( 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 biimtrid 
 |-  ( -. ( # ` 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 ) ) )
82 81 3adant2 
 |-  ( ( 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 ) ) )
84 83 ad2antlr 
 |-  ( ( ( 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 biimtrid 
 |-  ( 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 )