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

Theorem cshwidxmod 12774
Description: The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 13-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
Assertion
Ref Expression
cshwidxmod

Proof of Theorem cshwidxmod
StepHypRef Expression
1 elfzo0 11863 . . . 4
2 nnne0 10593 . . . . . 6
3 eqneqall 2664 . . . . . . 7
43com12 31 . . . . . 6
52, 4syl 16 . . . . 5
653ad2ant2 1018 . . . 4
71, 6sylbi 195 . . 3
873ad2ant3 1019 . 2
9 lencl 12562 . . . . 5
10 elnnne0 10834 . . . . . . . 8
11 simpl 457 . . . . . . . . . . . . . 14
1211adantl 466 . . . . . . . . . . . . 13
13 cshword 12762 . . . . . . . . . . . . 13
1412, 13sylan2 474 . . . . . . . . . . . 12
1514fveq1d 5873 . . . . . . . . . . 11
16 swrdcl 12646 . . . . . . . . . . . . . . . . 17
1716adantr 465 . . . . . . . . . . . . . . . 16
1817adantl 466 . . . . . . . . . . . . . . 15
19 swrdcl 12646 . . . . . . . . . . . . . . . . 17
2019adantr 465 . . . . . . . . . . . . . . . 16
2120adantl 466 . . . . . . . . . . . . . . 15
22 simpl 457 . . . . . . . . . . . . . . . . . . . 20
2311anim2i 569 . . . . . . . . . . . . . . . . . . . . . . 23
2423ancomd 451 . . . . . . . . . . . . . . . . . . . . . 22
25 zmodfzp1 12019 . . . . . . . . . . . . . . . . . . . . . 22
2624, 25syl 16 . . . . . . . . . . . . . . . . . . . . 21
2726adantl 466 . . . . . . . . . . . . . . . . . . . 20
28 nn0fz0 11803 . . . . . . . . . . . . . . . . . . . . . 22
299, 28sylib 196 . . . . . . . . . . . . . . . . . . . . 21
3029adantr 465 . . . . . . . . . . . . . . . . . . . 20
31 swrdlen 12650 . . . . . . . . . . . . . . . . . . . 20
3222, 27, 30, 31syl3anc 1228 . . . . . . . . . . . . . . . . . . 19
3332eqcomd 2465 . . . . . . . . . . . . . . . . . 18
34 swrd0len 12649 . . . . . . . . . . . . . . . . . . . . 21
3526, 34sylan2 474 . . . . . . . . . . . . . . . . . . . 20
3635eqcomd 2465 . . . . . . . . . . . . . . . . . . 19
3733, 36oveq12d 6314 . . . . . . . . . . . . . . . . . 18
3833, 37oveq12d 6314 . . . . . . . . . . . . . . . . 17
3938eleq2d 2527 . . . . . . . . . . . . . . . 16
4039biimpac 486 . . . . . . . . . . . . . . 15
41 ccatval2 12596 . . . . . . . . . . . . . . 15
4218, 21, 40, 41syl3anc 1228 . . . . . . . . . . . . . 14
4322adantl 466 . . . . . . . . . . . . . . . . 17
4427adantl 466 . . . . . . . . . . . . . . . . 17
4530adantl 466 . . . . . . . . . . . . . . . . 17
4643, 44, 45, 31syl3anc 1228 . . . . . . . . . . . . . . . 16
4746oveq2d 6312 . . . . . . . . . . . . . . 15
4847fveq2d 5875 . . . . . . . . . . . . . 14
49 elfzo2 11832 . . . . . . . . . . . . . . . . . . . . . . 23
50 eluz2 11116 . . . . . . . . . . . . . . . . . . . . . . . . . 26
51 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
52 nnz 10911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
5352adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
54 zmodcl 12015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
5554nn0zd 10992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5653, 55zsubcld 10999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5756adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5851, 57zsubcld 10999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5958adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
60 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61 nnre 10568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6261adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6354nn0red 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6462, 63resubcld 10012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
65 subge0 10090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6660, 64, 65syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6766exbiri 622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6867com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6968imp31 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
70 elnn0uz 11147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71 elnn0z 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7270, 71bitr3i 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7359, 69, 72sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7473adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7555adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7660adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7764adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7863adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7976, 77, 783jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
8079adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
81 ltsubadd2 10048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8280, 81syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8382exbiri 622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8483com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8584imp31 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
86 elfzo2 11832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8774, 75, 85, 86syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8887exp31 604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
89883adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9050, 89sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . 25
9190imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24
92913adant2 1015 . . . . . . . . . . . . . . . . . . . . . . 23
9349, 92sylbi 195 . . . . . . . . . . . . . . . . . . . . . 22
9493com12 31 . . . . . . . . . . . . . . . . . . . . 21
9594ex 434 . . . . . . . . . . . . . . . . . . . 20
9695adantr 465 . . . . . . . . . . . . . . . . . . 19
9796impcom 430 . . . . . . . . . . . . . . . . . 18
9897adantl 466 . . . . . . . . . . . . . . . . 17
9998impcom 430 . . . . . . . . . . . . . . . 16
100 swrd0fv 12666 . . . . . . . . . . . . . . . 16
10143, 44, 99, 100syl3anc 1228 . . . . . . . . . . . . . . 15
102 elfzoelz 11829 . . . . . . . . . . . . . . . . . . . . . . . 24
103102zcnd 10995 . . . . . . . . . . . . . . . . . . . . . . 23
104103adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
105104adantl 466 . . . . . . . . . . . . . . . . . . . . 21
106 nncn 10569 . . . . . . . . . . . . . . . . . . . . . 22
107106adantr 465 . . . . . . . . . . . . . . . . . . . . 21
10824, 54syl 16 . . . . . . . . . . . . . . . . . . . . . 22
109108nn0cnd 10879 . . . . . . . . . . . . . . . . . . . . 21
110105, 107, 1093jca 1176 . . . . . . . . . . . . . . . . . . . 20
111110adantl 466 . . . . . . . . . . . . . . . . . . 19
112111adantl 466 . . . . . . . . . . . . . . . . . 18
113 subsub3 9874 . . . . . . . . . . . . . . . . . 18
114112, 113syl 16 . . . . . . . . . . . . . . . . 17
11524adantl 466 . . . . . . . . . . . . . . . . . . 19
116115adantl 466 . . . . . . . . . . . . . . . . . 18
117107, 109jca 532 . . . . . . . . . . . . . . . . . . . . . . 23
118117adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
119 npcan 9852 . . . . . . . . . . . . . . . . . . . . . 22
120118, 119syl 16 . . . . . . . . . . . . . . . . . . . . 21
121120oveq2d 6312 . . . . . . . . . . . . . . . . . . . 20
122121eleq2d 2527 . . . . . . . . . . . . . . . . . . 19
123122biimpac 486 . . . . . . . . . . . . . . . . . 18
124 modaddmodup 12050 . . . . . . . . . . . . . . . . . 18
125116, 123, 124sylc 60 . . . . . . . . . . . . . . . . 17