Step | Hyp | Ref
| Expression |
1 | | wrdfn 13319 |
. . . . . 6
Word ..^ |
2 | | fnfun 5988 |
. . . . . 6
..^
|
3 | 1, 2 | syl 17 |
. . . . 5
Word |
4 | 3 | 3ad2ant1 1082 |
. . . 4
Word
..^
|
5 | | wrddm 13312 |
. . . . . 6
Word ..^ |
6 | | difssd 3738 |
. . . . . . . . 9
..^ ..^ ..^ |
7 | | oveq2 6658 |
. . . . . . . . . . 11
..^ ..^ |
8 | 7 | difeq1d 3727 |
. . . . . . . . . 10
..^ ..^
|
9 | 8 | adantl 482 |
. . . . . . . . 9
..^ ..^ ..^ |
10 | | simpl 473 |
. . . . . . . . 9
..^ ..^ |
11 | 6, 9, 10 | 3sstr4d 3648 |
. . . . . . . 8
..^ ..^
|
12 | 11 | a1d 25 |
. . . . . . 7
..^
..^ ..^
|
13 | 12 | ex 450 |
. . . . . 6
..^
..^ ..^ |
14 | 5, 13 | syl 17 |
. . . . 5
Word
..^ ..^ |
15 | 14 | 3imp 1256 |
. . . 4
Word
..^ ..^ |
16 | 4, 15 | jca 554 |
. . 3
Word
..^ ..^ |
17 | | dfimafn 6245 |
. . 3
..^
..^
..^ |
18 | 16, 17 | syl 17 |
. 2
Word
..^ ..^
..^ |
19 | | modsumfzodifsn 12743 |
. . . . . . 7
..^ ..^
..^ |
20 | 19 | 3ad2antl3 1225 |
. . . . . 6
Word
..^
..^ ..^ |
21 | | oveq2 6658 |
. . . . . . . . . 10
|
22 | 21 | eqcoms 2630 |
. . . . . . . . 9
|
23 | 22 | eleq1d 2686 |
. . . . . . . 8
..^ ..^ |
24 | 23 | 3ad2ant2 1083 |
. . . . . . 7
Word
..^ ..^ ..^ |
25 | 24 | adantr 481 |
. . . . . 6
Word
..^
..^ ..^ ..^ |
26 | 20, 25 | mpbird 247 |
. . . . 5
Word
..^
..^ ..^ |
27 | | modfzo0difsn 12742 |
. . . . . . 7
..^ ..^
..^ |
28 | 27 | 3ad2antl3 1225 |
. . . . . 6
Word
..^
..^ ..^ |
29 | | oveq2 6658 |
. . . . . . . . . . 11
|
30 | 29 | eqcomd 2628 |
. . . . . . . . . 10
|
31 | 30 | eqeq2d 2632 |
. . . . . . . . 9
|
32 | 31 | rexbidv 3052 |
. . . . . . . 8
..^
..^ |
33 | 32 | 3ad2ant2 1083 |
. . . . . . 7
Word
..^ ..^
..^ |
34 | 33 | adantr 481 |
. . . . . 6
Word
..^
..^ ..^
..^ |
35 | 28, 34 | mpbird 247 |
. . . . 5
Word
..^
..^ ..^ |
36 | | fveq2 6191 |
. . . . . . . 8
|
37 | 36 | 3ad2ant3 1084 |
. . . . . . 7
Word
..^
..^ |
38 | | simpl1 1064 |
. . . . . . . . 9
Word
..^
..^
Word |
39 | | elfzoelz 12470 |
. . . . . . . . . . 11
..^
|
40 | 39 | 3ad2ant3 1084 |
. . . . . . . . . 10
Word
..^ |
41 | 40 | adantr 481 |
. . . . . . . . 9
Word
..^
..^
|
42 | | oveq2 6658 |
. . . . . . . . . . . . 13
..^ ..^ |
43 | 42 | eleq2d 2687 |
. . . . . . . . . . . 12
..^ ..^ |
44 | | fzo0ss1 12498 |
. . . . . . . . . . . . 13
..^ ..^ |
45 | 44 | sseli 3599 |
. . . . . . . . . . . 12
..^
..^ |
46 | 43, 45 | syl6bi 243 |
. . . . . . . . . . 11
..^ ..^ |
47 | 46 | 3ad2ant2 1083 |
. . . . . . . . . 10
Word
..^ ..^ ..^ |
48 | 47 | imp 445 |
. . . . . . . . 9
Word
..^
..^ ..^ |
49 | | cshwidxmod 13549 |
. . . . . . . . . 10
Word
..^ cyclShift |
50 | 49 | eqcomd 2628 |
. . . . . . . . 9
Word
..^ cyclShift |
51 | 38, 41, 48, 50 | syl3anc 1326 |
. . . . . . . 8
Word
..^
..^
cyclShift |
52 | 51 | 3adant3 1081 |
. . . . . . 7
Word
..^
..^
cyclShift |
53 | 37, 52 | eqtrd 2656 |
. . . . . 6
Word
..^
..^ cyclShift |
54 | 53 | eqeq1d 2624 |
. . . . 5
Word
..^
..^ cyclShift |
55 | 26, 35, 54 | rexxfrd2 4885 |
. . . 4
Word
..^ ..^ ..^ cyclShift
|
56 | 55 | abbidv 2741 |
. . 3
Word
..^ ..^ ..^ cyclShift |
57 | 39 | anim2i 593 |
. . . . . . . 8
Word
..^ Word
|
58 | 57 | 3adant2 1080 |
. . . . . . 7
Word
..^ Word |
59 | | cshwfn 13547 |
. . . . . . 7
Word
cyclShift
..^ |
60 | 58, 59 | syl 17 |
. . . . . 6
Word
..^ cyclShift ..^ |
61 | | fnfun 5988 |
. . . . . . . 8
cyclShift ..^
cyclShift |
62 | 61 | adantl 482 |
. . . . . . 7
Word
..^
cyclShift ..^
cyclShift |
63 | 42, 44 | syl6eqss 3655 |
. . . . . . . . . 10
..^ ..^ |
64 | 63 | 3ad2ant2 1083 |
. . . . . . . . 9
Word
..^ ..^
..^ |
65 | 64 | adantr 481 |
. . . . . . . 8
Word
..^
cyclShift ..^ ..^
..^ |
66 | | fndm 5990 |
. . . . . . . . 9
cyclShift ..^
cyclShift ..^ |
67 | 66 | adantl 482 |
. . . . . . . 8
Word
..^
cyclShift ..^
cyclShift ..^ |
68 | 65, 67 | sseqtr4d 3642 |
. . . . . . 7
Word
..^
cyclShift ..^ ..^
cyclShift |
69 | 62, 68 | jca 554 |
. . . . . 6
Word
..^
cyclShift ..^ cyclShift ..^ cyclShift
|
70 | 60, 69 | mpdan 702 |
. . . . 5
Word
..^ cyclShift ..^ cyclShift
|
71 | | dfimafn 6245 |
. . . . 5
cyclShift ..^
cyclShift cyclShift ..^ ..^ cyclShift |
72 | 70, 71 | syl 17 |
. . . 4
Word
..^ cyclShift ..^ ..^ cyclShift
|
73 | 72 | eqcomd 2628 |
. . 3
Word
..^ ..^ cyclShift
cyclShift ..^ |
74 | 56, 73 | eqtrd 2656 |
. 2
Word
..^ ..^ cyclShift ..^ |
75 | 18, 74 | eqtrd 2656 |
1
Word
..^ ..^ cyclShift ..^ |