Metamath Proof Explorer

Theorem cshwidxm1

Description: The symbol at index ((n-N)-1) of a word of length n (not 0) cyclically shifted by N positions is the symbol at index (n-1) of the original word. (Contributed by AV, 23-Mar-2018) (Revised by AV, 21-May-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion cshwidxm1 
|- ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( ( # ` W ) - N ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> W e. Word V )
2 elfzoelz 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> N e. ZZ )
3 2 adantl 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> N e. ZZ )
4 ubmelm1fzo 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( # ` W ) - N ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
5 4 adantl 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - N ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
6 cshwidxmod 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( ( ( # ` W ) - N ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( ( # ` W ) - N ) - 1 ) ) = ( W ` ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) ) )
7 1 3 5 6 syl3anc 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( ( # ` W ) - N ) - 1 ) ) = ( W ` ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) ) )
8 elfzoel2 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. ZZ )
9 8 zcnd 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. CC )
10 2 zcnd 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> N e. CC )
11 1cnd 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> 1 e. CC )
12 nnpcan 
 |-  ( ( ( # ` W ) e. CC /\ N e. CC /\ 1 e. CC ) -> ( ( ( ( # ` W ) - N ) - 1 ) + N ) = ( ( # ` W ) - 1 ) )
13 9 10 11 12 syl3anc 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( ( # ` W ) - N ) - 1 ) + N ) = ( ( # ` W ) - 1 ) )
14 13 oveq1d 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) = ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) )
15 14 adantl 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) = ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) )
16 elfzo0 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) <-> ( N e. NN0 /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) )
17 nnre 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR )
18 peano2rem 
 |-  ( ( # ` W ) e. RR -> ( ( # ` W ) - 1 ) e. RR )
19 17 18 syl 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. RR )
20 nnrp 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
21 19 20 jca 
 |-  ( ( # ` W ) e. NN -> ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) )
22 21 3ad2ant2 
 |-  ( ( N e. NN0 /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) )
23 16 22 sylbi 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) )
24 nnm1ge0 
 |-  ( ( # ` W ) e. NN -> 0 <_ ( ( # ` W ) - 1 ) )
25 24 3ad2ant2 
 |-  ( ( N e. NN0 /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> 0 <_ ( ( # ` W ) - 1 ) )
26 16 25 sylbi 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> 0 <_ ( ( # ` W ) - 1 ) )
27 zre 
 |-  ( ( # ` W ) e. ZZ -> ( # ` W ) e. RR )
28 27 ltm1d 
 |-  ( ( # ` W ) e. ZZ -> ( ( # ` W ) - 1 ) < ( # ` W ) )
29 8 28 syl 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( # ` W ) - 1 ) < ( # ` W ) )
30 23 26 29 jca32 
 |-  ( N e. ( 0 ..^ ( # ` W ) ) -> ( ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) /\ ( 0 <_ ( ( # ` W ) - 1 ) /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) )
31 30 adantl 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) /\ ( 0 <_ ( ( # ` W ) - 1 ) /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) )
32 modid 
 |-  ( ( ( ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR+ ) /\ ( 0 <_ ( ( # ` W ) - 1 ) /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
33 31 32 syl 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
34 15 33 eqtrd 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) = ( ( # ` W ) - 1 ) )
35 34 fveq2d 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( ( ( ( ( # ` W ) - N ) - 1 ) + N ) mod ( # ` W ) ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
36 7 35 eqtrd 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( ( # ` W ) - N ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )