Proof of Theorem repswcshw
Step | Hyp | Ref
| Expression |
1 | | 0csh0 13539 |
. . . . 5
cyclShift |
2 | | repsw0 13524 |
. . . . . 6
repeatS |
3 | 2 | oveq1d 6665 |
. . . . 5
repeatS
cyclShift cyclShift |
4 | 1, 3, 2 | 3eqtr4a 2682 |
. . . 4
repeatS
cyclShift repeatS |
5 | 4 | 3ad2ant1 1082 |
. . 3
repeatS
cyclShift repeatS |
6 | | oveq2 6658 |
. . . . 5
repeatS repeatS |
7 | 6 | oveq1d 6665 |
. . . 4
repeatS
cyclShift repeatS cyclShift |
8 | 7, 6 | eqeq12d 2637 |
. . 3
repeatS cyclShift repeatS
repeatS cyclShift
repeatS |
9 | 5, 8 | syl5ibr 236 |
. 2
repeatS
cyclShift repeatS
|
10 | | idd 24 |
. . . 4
|
11 | | df-ne 2795 |
. . . . 5
|
12 | | elnnne0 11306 |
. . . . . 6
|
13 | 12 | simplbi2com 657 |
. . . . 5
|
14 | 11, 13 | sylbir 225 |
. . . 4
|
15 | | idd 24 |
. . . 4
|
16 | 10, 14, 15 | 3anim123d 1406 |
. . 3
|
17 | | nnnn0 11299 |
. . . . . . 7
|
18 | 17 | anim2i 593 |
. . . . . 6
|
19 | | repsw 13522 |
. . . . . 6
repeatS
Word |
20 | 18, 19 | syl 17 |
. . . . 5
repeatS
Word |
21 | | cshword 13537 |
. . . . 5
repeatS
Word repeatS
cyclShift repeatS
substr repeatS repeatS ++ repeatS
substr repeatS |
22 | 20, 21 | stoic3 1701 |
. . . 4
repeatS
cyclShift repeatS
substr repeatS repeatS ++ repeatS
substr repeatS |
23 | | repswlen 13523 |
. . . . . . . . . 10
repeatS |
24 | 18, 23 | syl 17 |
. . . . . . . . 9
repeatS |
25 | 24 | oveq2d 6666 |
. . . . . . . 8
repeatS |
26 | 25, 24 | opeq12d 4410 |
. . . . . . 7
repeatS repeatS |
27 | 26 | oveq2d 6666 |
. . . . . 6
repeatS substr repeatS repeatS repeatS substr
|
28 | 25 | opeq2d 4409 |
. . . . . . 7
repeatS
|
29 | 28 | oveq2d 6666 |
. . . . . 6
repeatS substr repeatS
repeatS
substr |
30 | 27, 29 | oveq12d 6668 |
. . . . 5
repeatS
substr repeatS repeatS ++ repeatS
substr repeatS repeatS substr ++ repeatS substr |
31 | 30 | 3adant3 1081 |
. . . 4
repeatS substr repeatS repeatS ++ repeatS
substr repeatS repeatS substr ++ repeatS substr |
32 | 18 | 3adant3 1081 |
. . . . . . 7
|
33 | | zmodcl 12690 |
. . . . . . . . . 10
|
34 | 33 | ancoms 469 |
. . . . . . . . 9
|
35 | 17 | adantr 481 |
. . . . . . . . 9
|
36 | 34, 35 | jca 554 |
. . . . . . . 8
|
37 | 36 | 3adant1 1079 |
. . . . . . 7
|
38 | | nnre 11027 |
. . . . . . . . 9
|
39 | 38 | leidd 10594 |
. . . . . . . 8
|
40 | 39 | 3ad2ant2 1083 |
. . . . . . 7
|
41 | | repswswrd 13531 |
. . . . . . 7
repeatS
substr repeatS
|
42 | 32, 37, 40, 41 | syl3anc 1326 |
. . . . . 6
repeatS
substr repeatS
|
43 | | 0nn0 11307 |
. . . . . . . . 9
|
44 | 34, 43 | jctil 560 |
. . . . . . . 8
|
45 | 44 | 3adant1 1079 |
. . . . . . 7
|
46 | | zre 11381 |
. . . . . . . . . 10
|
47 | | nnrp 11842 |
. . . . . . . . . 10
|
48 | | modcl 12672 |
. . . . . . . . . 10
|
49 | 46, 47, 48 | syl2anr 495 |
. . . . . . . . 9
|
50 | 38 | adantr 481 |
. . . . . . . . 9
|
51 | | modlt 12679 |
. . . . . . . . . 10
|
52 | 46, 47, 51 | syl2anr 495 |
. . . . . . . . 9
|
53 | 49, 50, 52 | ltled 10185 |
. . . . . . . 8
|
54 | 53 | 3adant1 1079 |
. . . . . . 7
|
55 | | repswswrd 13531 |
. . . . . . 7
repeatS substr
repeatS |
56 | 32, 45, 54, 55 | syl3anc 1326 |
. . . . . 6
repeatS
substr repeatS |
57 | 42, 56 | oveq12d 6668 |
. . . . 5
repeatS substr ++ repeatS substr repeatS
++ repeatS |
58 | | simp1 1061 |
. . . . . 6
|
59 | 33 | nn0red 11352 |
. . . . . . . . . 10
|
60 | 59 | ancoms 469 |
. . . . . . . . 9
|
61 | 60, 50, 52 | ltled 10185 |
. . . . . . . 8
|
62 | 61 | 3adant1 1079 |
. . . . . . 7
|
63 | 34 | 3adant1 1079 |
. . . . . . . 8
|
64 | 17 | 3ad2ant2 1083 |
. . . . . . . 8
|
65 | | nn0sub 11343 |
. . . . . . . 8
|
66 | 63, 64, 65 | syl2anc 693 |
. . . . . . 7
|
67 | 62, 66 | mpbid 222 |
. . . . . 6
|
68 | 33 | nn0ge0d 11354 |
. . . . . . . . 9
|
69 | 68 | ancoms 469 |
. . . . . . . 8
|
70 | 69 | 3adant1 1079 |
. . . . . . 7
|
71 | 63, 43 | jctil 560 |
. . . . . . . 8
|
72 | | nn0sub 11343 |
. . . . . . . 8
|
73 | 71, 72 | syl 17 |
. . . . . . 7
|
74 | 70, 73 | mpbid 222 |
. . . . . 6
|
75 | | repswccat 13532 |
. . . . . 6
repeatS
++ repeatS
repeatS
|
76 | 58, 67, 74, 75 | syl3anc 1326 |
. . . . 5
repeatS
++ repeatS repeatS
|
77 | | nncn 11028 |
. . . . . . . . . . 11
|
78 | 77 | adantl 482 |
. . . . . . . . . 10
|
79 | 33 | nn0cnd 11353 |
. . . . . . . . . 10
|
80 | | 0cnd 10033 |
. . . . . . . . . 10
|
81 | 78, 79, 80 | npncand 10416 |
. . . . . . . . 9
|
82 | 77 | subid1d 10381 |
. . . . . . . . . 10
|
83 | 82 | adantl 482 |
. . . . . . . . 9
|
84 | 81, 83 | eqtrd 2656 |
. . . . . . . 8
|
85 | 84 | ancoms 469 |
. . . . . . 7
|
86 | 85 | 3adant1 1079 |
. . . . . 6
|
87 | 86 | oveq2d 6666 |
. . . . 5
repeatS
repeatS |
88 | 57, 76, 87 | 3eqtrd 2660 |
. . . 4
repeatS substr ++ repeatS substr repeatS |
89 | 22, 31, 88 | 3eqtrd 2660 |
. . 3
repeatS
cyclShift repeatS |
90 | 16, 89 | syl6 35 |
. 2
repeatS cyclShift
repeatS |
91 | 9, 90 | pm2.61i 176 |
1
repeatS
cyclShift repeatS |