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

Theorem cshwidxmod 12756
 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 Word ..^ cyclShift

Proof of Theorem cshwidxmod
StepHypRef Expression
1 elfzo0 11845 . . . 4 ..^
2 nnne0 10575 . . . . . 6
3 eqneqall 2650 . . . . . . 7 cyclShift
43com12 31 . . . . . 6 cyclShift
52, 4syl 16 . . . . 5 cyclShift
653ad2ant2 1019 . . . 4 cyclShift
71, 6sylbi 195 . . 3 ..^ cyclShift
873ad2ant3 1020 . 2 Word ..^ cyclShift
9 lencl 12544 . . . . 5 Word
10 elnnne0 10816 . . . . . . . 8
11 simpl 457 . . . . . . . . . . . . . 14 ..^
1211adantl 466 . . . . . . . . . . . . 13 ..^
13 cshword 12744 . . . . . . . . . . . . 13 Word cyclShift substr concat substr
1412, 13sylan2 474 . . . . . . . . . . . 12 Word ..^ cyclShift substr concat substr
1514fveq1d 5858 . . . . . . . . . . 11 Word ..^ cyclShift substr concat substr
16 swrdcl 12628 . . . . . . . . . . . . . . . . 17 Word substr Word
1716adantr 465 . . . . . . . . . . . . . . . 16 Word ..^ substr Word
1817adantl 466 . . . . . . . . . . . . . . 15 ..^ Word ..^ substr Word
19 swrdcl 12628 . . . . . . . . . . . . . . . . 17 Word substr Word
2019adantr 465 . . . . . . . . . . . . . . . 16 Word ..^ substr Word
2120adantl 466 . . . . . . . . . . . . . . 15 ..^ Word ..^ substr Word
22 simpl 457 . . . . . . . . . . . . . . . . . . . 20 Word ..^ Word
2311anim2i 569 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
2423ancomd 451 . . . . . . . . . . . . . . . . . . . . . 22 ..^
25 zmodfzp1 12001 . . . . . . . . . . . . . . . . . . . . . 22
2624, 25syl 16 . . . . . . . . . . . . . . . . . . . . 21 ..^
2726adantl 466 . . . . . . . . . . . . . . . . . . . 20 Word ..^
28 nn0fz0 11785 . . . . . . . . . . . . . . . . . . . . . 22
299, 28sylib 196 . . . . . . . . . . . . . . . . . . . . 21 Word
3029adantr 465 . . . . . . . . . . . . . . . . . . . 20 Word ..^
31 swrdlen 12632 . . . . . . . . . . . . . . . . . . . 20 Word substr
3222, 27, 30, 31syl3anc 1229 . . . . . . . . . . . . . . . . . . 19 Word ..^ substr
3332eqcomd 2451 . . . . . . . . . . . . . . . . . 18 Word ..^ substr
34 swrd0len 12631 . . . . . . . . . . . . . . . . . . . . 21 Word substr
3526, 34sylan2 474 . . . . . . . . . . . . . . . . . . . 20 Word ..^ substr
3635eqcomd 2451 . . . . . . . . . . . . . . . . . . 19 Word ..^ substr
3733, 36oveq12d 6299 . . . . . . . . . . . . . . . . . 18 Word ..^ substr substr
3833, 37oveq12d 6299 . . . . . . . . . . . . . . . . 17 Word ..^ ..^ substr ..^ substr substr
3938eleq2d 2513 . . . . . . . . . . . . . . . 16 Word ..^ ..^ substr ..^ substr substr
4039biimpac 486 . . . . . . . . . . . . . . 15 ..^ Word ..^ substr ..^ substr substr
41 ccatval2 12578 . . . . . . . . . . . . . . 15 substr Word substr Word substr ..^ substr substr substr concat substr substr substr
4218, 21, 40, 41syl3anc 1229 . . . . . . . . . . . . . 14 ..^ Word ..^ substr concat substr substr substr
4322adantl 466 . . . . . . . . . . . . . . . . 17 ..^ Word ..^ Word
4427adantl 466 . . . . . . . . . . . . . . . . 17 ..^ Word ..^
4530adantl 466 . . . . . . . . . . . . . . . . 17 ..^ Word ..^
4643, 44, 45, 31syl3anc 1229 . . . . . . . . . . . . . . . 16 ..^ Word ..^ substr
4746oveq2d 6297 . . . . . . . . . . . . . . 15 ..^ Word ..^ substr
4847fveq2d 5860 . . . . . . . . . . . . . 14 ..^ Word ..^ substr substr substr
49 elfzo2 11814 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
50 eluz2 11098 . . . . . . . . . . . . . . . . . . . . . . . . . 26
51 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
52 nnz 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
5352adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
54 zmodcl 11997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
5554nn0zd 10974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5653, 55zsubcld 10981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5756adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5851, 57zsubcld 10981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5958adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
60 zre 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61 nnre 10550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6261adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6354nn0red 10860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6462, 63resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
65 subge0 10072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6660, 64, 65syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6766exbiri 622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6867com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6968imp31 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
70 elnn0uz 11129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71 elnn0z 10884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
8079adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
81 ltsubadd2 10030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8280, 81syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8382exbiri 622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8483com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8584imp31 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
86 elfzo2 11814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
8774, 75, 85, 86syl3anbrc 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
8887exp31 604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
89883adant1 1015 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
9050, 89sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
9190imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
92913adant2 1016 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
9349, 92sylbi 195 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
9493com12 31 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
9594ex 434 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
9695adantr 465 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^
9796impcom 430 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^
9897adantl 466 . . . . . . . . . . . . . . . . 17 Word ..^ ..^ ..^
9998impcom 430 . . . . . . . . . . . . . . . 16 ..^ Word ..^ ..^
100 swrd0fv 12648 . . . . . . . . . . . . . . . 16 Word ..^ substr
10143, 44, 99, 100syl3anc 1229 . . . . . . . . . . . . . . 15 ..^ Word ..^ substr
102 elfzoelz 11811 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
103102zcnd 10977 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
104103adantl 466 . . . . . . . . . . . . . . . . . . . . . 22 ..^
105104adantl 466 . . . . . . . . . . . . . . . . . . . . 21 ..^
106 nncn 10551 . . . . . . . . . . . . . . . . . . . . . 22
107106adantr 465 . . . . . . . . . . . . . . . . . . . . 21 ..^
10824, 54syl 16 . . . . . . . . . . . . . . . . . . . . . 22 ..^
109108nn0cnd 10861 . . . . . . . . . . . . . . . . . . . . 21 ..^
110105, 107, 1093jca 1177 . . . . . . . . . . . . . . . . . . . 20 ..^
111110adantl 466 . . . . . . . . . . . . . . . . . . 19 Word ..^
112111adantl 466 . . . . . . . . . . . . . . . . . 18 ..^ Word ..^
113 subsub3 9856 . . . . . . . . . . . . . . . . . 18
114112, 113syl 16 . . . . . . . . . . . . . . . . 17 ..^ Word ..^
11524adantl 466 . . . . . . . . . . . . . . . . . . 19 Word ..^
116115adantl 466 . . . . . . . . . . . . . . . . . 18 ..^ Word ..^
117107, 109jca 532 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
118117adantl 466 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^
119 npcan 9834 . . . . . . . . . . . . . . . . . . . . . 22
120118, 119syl 16 . . . . . . . . . . . . . . . . . . . . 21 Word ..^
121120oveq2d 6297 . . . . . . . . . . . . . . . . . . . 20 Word ..^ ..^ ..^
122121eleq2d 2513 . . . . . . . . . . . . . . . . . . 19 Word ..^ ..^ ..^
123122biimpac 486 . . . . . . . . . . . . . . . . . 18 ..^ Word ..^ ..^
124 modaddmodup 12032 . . . . . . . . . . . . . . . . . 18 ..^
125116, 123, 124sylc 60 . . . . . . . . . . . . . . . . 17 ..^ Word ..^
126114, 125eqtrd 2484 . . . . . . . . . . . . . . . 16 ..^ Word ..^
127126fveq2d 5860 . . . . . . . . . . . . . . 15 ..^ Word ..^
128101, 127eqtrd 2484 . . . . . . . . . . . . . 14 ..^ Word ..^ substr
12942, 48, 1283eqtrd 2488 . . . . . . . . . . . . 13 ..^ Word ..^ substr concat substr
130129ex 434 . . . . . . . . . . . 12 ..^ Word ..^ substr concat substr
131106adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
13254nn0cnd 10861 . . . . . . . . . . . . . . . . . . . . . 22
133131, 132npcand 9940 . . . . . . . . . . . . . . . . . . . . 21
134133ex 434 . . . . . . . . . . . . . . . . . . . 20
135134adantr 465 . . . . . . . . . . . . . . . . . . 19 ..^
136135impcom 430 . . . . . . . . . . . . . . . . . 18 ..^
137136adantl 466 . . . . . . . . . . . . . . . . 17 Word ..^
138137oveq2d 6297 . . . . . . . . . . . . . . . 16 Word ..^ ..^ ..^
139138eleq2d 2513 . . . . . . . . . . . . . . 15 Word ..^ ..^ ..^
140139notbid 294 . . . . . . . . . . . . . 14 Word ..^ ..^ ..^
14117adantr 465 . . . . . . . . . . . . . . . . 17 Word ..^ ..^ substr Word
14220adantr 465 . . . . . . . . . . . . . . . . 17 Word ..^ ..^ substr Word
143108nn0zd 10974 . . . . . . . . . . . . . . . . . . . . 21 ..^
144143adantl 466 . . . . . . . . . . . . . . . . . . . 20 Word ..^
145 zre 10875 . . . . . . . . . . . . . . . . . . . . . . 23
146145adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
147 nnrp 11240 . . . . . . . . . . . . . . . . . . . . . 22
148 modlt 11988 . . . . . . . . . . . . . . . . . . . . . 22
149146, 147, 148syl2anr 478 . . . . . . . . . . . . . . . . . . . . 21 ..^
150149adantl 466 . . . . . . . . . . . . . . . . . . . 20 Word ..^
151 simprrr 766 . . . . . . . . . . . . . . . . . . . 20 Word ..^ ..^
152 fzonfzoufzol 11895 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^
153144, 150, 151, 152syl3anc 1229 . . . . . . . . . . . . . . . . . . 19 Word ..^ ..^ ..^
154153imp 429 . . . . . . . . . . . . . . . . . 18 Word ..^ ..^ ..^
15522adantr 465 . . . . . . . . . . . . . . . . . . . 20 Word ..^ ..^ Word
15627adantr 465 . . . . . . . . . . . . . . . . . . . 20 Word ..^ ..^
15730adantr 465 . . . . . . . . . . . . . . . . . . . 20 Word ..^ ..^
158155, 156, 157, 31syl3anc 1229 . . . . . . . . . . . . . . . . . . 19 Word ..^ ..^ substr
159158oveq2d 6297 . . . . . . . . . . . . . . . . . 18 Word ..^ ..^ ..^ substr ..^
160154, 159eleqtrrd 2534 . . . . . . . . . . . . . . . . 17 Word ..^ ..^ ..^ substr
161 ccatval1 12577 . . . . . . . . . . . . . . . . 17 substr Word substr Word ..^ substr substr concat substr substr
162141, 142, 160, 161syl3anc 1229 . . . . . . . . . . . . . . . 16 Word ..^ ..^ substr concat substr substr
16323adantl 466 . . . . . . . . . . . . . . . . . . . 20 Word ..^
164163ancomd 451 . . . . . . . . . . . . . . . . . . 19 Word ..^
165164, 25syl 16 . . . . . . . . . . . . . . . . . 18 Word ..^
166165adantr 465 . . . . . . . . . . . . . . . . 17 Word ..^ ..^
167 swrdfv 12633 . . . . . . . . . . . . . . . . 17 Word ..^ substr
168155, 166, 157, 154, 167syl31anc 1232 . . . . . . . . . . . . . . . 16 Word ..^ ..^ substr
169115adantr 465 . . . . . . . . . . . . . . . . . 18 Word ..^ ..^
17054ancoms 453 . . . . . . . . . . . . . . . . . . . . . . 23
171170nn0zd 10974 . . . . . . . . . . . . . . . . . . . . . 22
172171adantrr 716 . . . . . . . . . . . . . . . . . . . . 21 ..^
173172adantl 466 . . . . . . . . . . . . . . . . . . . 20 Word ..^
174173, 150, 151, 152syl3anc 1229 . . . . . . . . . . . . . . . . . . 19 Word ..^ ..^ ..^
175174imp 429 . . . . . . . . . . . . . . . . . 18 Word ..^ ..^ ..^
176 modaddmodlo 12033 . . . . . . . . . . . . . . . . . 18 ..^
177169, 175, 176sylc 60 . . . . . . . . . . . . . . . . 17 Word ..^ ..^
178177fveq2d 5860 . . . . . . . . . . . . . . . 16 Word ..^ ..^
179162, 168, 1783eqtrd 2488 . . . . . . . . . . . . . . 15 Word ..^ ..^ substr concat substr
180179ex 434 . . . . . . . . . . . . . 14 Word ..^ ..^ substr concat substr
181140, 180sylbid 215 . . . . . . . . . . . . 13 Word ..^ ..^ substr concat substr
182181com12 31 . . . . . . . . . . . 12 ..^ Word ..^ substr concat substr
183130, 182pm2.61i 164 . . . . . . . . . . 11 Word ..^ substr concat substr
18415, 183eqtrd 2484 . . . . . . . . . 10 Word ..^ cyclShift
185184exp32 605 . . . . . . . . 9 Word ..^ cyclShift
186185com12 31 . . . . . . . 8 Word ..^ cyclShift
18710, 186sylbir 213 . . . . . . 7 Word ..^ cyclShift
188187ex 434 . . . . . 6 Word ..^ cyclShift
189188com23 78 . . . . 5 Word ..^ cyclShift
1909, 189mpcom 36 . . . 4 Word ..^ cyclShift
191190com23 78 . . 3 Word ..^ cyclShift
1921913impib 1195 . 2 Word ..^ cyclShift
1938, 192pm2.61dne 2760 1 Word ..^ cyclShift
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   w3a 974   wceq 1383   wcel 1804   wne 2638  cop 4020   class class class wbr 4437  cfv 5578  (class class class)co 6281  cc 9493  cr 9494  cc0 9495   caddc 9498   clt 9631   cle 9632   cmin 9810  cn 10543  cn0 10802  cz 10871  cuz 11092  crp 11231  cfz 11683  ..^cfzo 11806   cmo 11978  chash 12387  Word cword 12516   concat cconcat 12518   substr csubstr 12520   cyclShift ccsh 12741 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572  ax-pre-sup 9573 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-sup 7903  df-card 8323  df-cda 8551  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-div 10214  df-nn 10544  df-2 10601  df-n0 10803  df-z 10872  df-uz 11093  df-rp 11232  df-fz 11684  df-fzo 11807  df-fl 11911  df-mod 11979  df-hash 12388  df-word 12524  df-concat 12526  df-substr 12528  df-csh 12742 This theorem is referenced by:  cshwidx0mod  12757  cshwidxm1  12759  cshwidxm  12760  cshwidxn  12761  2cshw  12763  cshweqrep  12771  cshco  12784  clwwisshclwwlem  24784
 Copyright terms: Public domain W3C validator