Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cshwidxn Unicode version

Theorem cshwidxn 12779
 Description: The symbol at index (n-1) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index (N-1) of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
Assertion
Ref Expression
cshwidxn

Proof of Theorem cshwidxn
StepHypRef Expression
1 simpl 457 . . 3
2 elfzelz 11717 . . . 4
4 elfz1b 11777 . . . . . 6
5 simp2 997 . . . . . 6
64, 5sylbi 195 . . . . 5
76adantl 466 . . . 4
8 fzo0end 11904 . . . 4
97, 8syl 16 . . 3
10 cshwidxmod 12774 . . 3
111, 3, 9, 10syl3anc 1228 . 2
12 nncn 10569 . . . . . . . . . . 11
1312adantl 466 . . . . . . . . . 10
14 1cnd 9633 . . . . . . . . . 10
15 nncn 10569 . . . . . . . . . . 11
1615adantr 465 . . . . . . . . . 10
1713, 14, 163jca 1176 . . . . . . . . 9
18173adant3 1016 . . . . . . . 8
194, 18sylbi 195 . . . . . . 7
20 subadd23 9855 . . . . . . 7
2119, 20syl 16 . . . . . 6
2221oveq1d 6311 . . . . 5
23 nnm1nn0 10862 . . . . . . . . 9
24233ad2ant1 1017 . . . . . . . 8
25 simp3 998 . . . . . . . . 9
26 nnz 10911 . . . . . . . . . . . 12
27 nnz 10911 . . . . . . . . . . . 12
2826, 27anim12i 566 . . . . . . . . . . 11
29283adant3 1016 . . . . . . . . . 10
30 zlem1lt 10940 . . . . . . . . . 10
3129, 30syl 16 . . . . . . . . 9
3225, 31mpbid 210 . . . . . . . 8
3324, 5, 323jca 1176 . . . . . . 7
344, 33sylbi 195 . . . . . 6
35 addmodid 12036 . . . . . 6
3634, 35syl 16 . . . . 5
3722, 36eqtrd 2498 . . . 4
3837fveq2d 5875 . . 3