Step | Hyp | Ref
| Expression |
1 | | f1f 6101 |
. . . . 5
..^
..^ |
2 | | iswrdi 13309 |
. . . . 5
..^ Word |
3 | 1, 2 | syl 17 |
. . . 4
..^
Word |
4 | | cshwf 13546 |
. . . . . . . . 9
Word
cyclShift
..^ |
5 | 4 | 3adant1 1079 |
. . . . . . . 8
..^
Word cyclShift ..^ |
6 | 5 | adantr 481 |
. . . . . . 7
..^
Word cyclShift
cyclShift ..^ |
7 | | feq1 6026 |
. . . . . . . 8
cyclShift ..^
cyclShift ..^ |
8 | 7 | adantl 482 |
. . . . . . 7
..^
Word cyclShift
..^
cyclShift ..^ |
9 | 6, 8 | mpbird 247 |
. . . . . 6
..^
Word cyclShift
..^ |
10 | | dff13 6512 |
. . . . . . . 8
..^
..^ ..^
..^ |
11 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . 18
cyclShift cyclShift
|
12 | 11 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
cyclShift Word cyclShift |
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . . 16
cyclShift Word ..^ ..^
cyclShift
|
14 | | cshwidxmod 13549 |
. . . . . . . . . . . . . . . . . . . . 21
Word
..^ cyclShift |
15 | 14 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^
cyclShift |
16 | 15 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . 19
cyclShift Word ..^
cyclShift |
17 | 16 | com12 32 |
. . . . . . . . . . . . . . . . . 18
..^
cyclShift Word cyclShift |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ ..^ cyclShift Word
cyclShift |
19 | 18 | impcom 446 |
. . . . . . . . . . . . . . . 16
cyclShift Word ..^ ..^
cyclShift |
20 | 13, 19 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
cyclShift Word ..^ ..^
|
21 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . 18
cyclShift cyclShift
|
22 | 21 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
cyclShift Word cyclShift |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
cyclShift Word ..^ ..^
cyclShift
|
24 | | cshwidxmod 13549 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^ cyclShift |
25 | 24 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . 19
Word
..^
cyclShift |
26 | 25 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . 18
cyclShift Word ..^
cyclShift |
27 | 26 | adantld 483 |
. . . . . . . . . . . . . . . . 17
cyclShift Word ..^ ..^ cyclShift |
28 | 27 | imp 445 |
. . . . . . . . . . . . . . . 16
cyclShift Word ..^ ..^
cyclShift |
29 | 23, 28 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
cyclShift Word ..^ ..^
|
30 | 20, 29 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
cyclShift Word ..^ ..^
|
31 | 30 | adantlr 751 |
. . . . . . . . . . . . 13
cyclShift
Word
..^ ..^
..^
..^ |
32 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
33 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
36 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
37 | 35, 36 | zaddcld 11486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
38 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
39 | 38 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
40 | 37, 39 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
41 | 40 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
42 | 41 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . 23
cyclShift Word |
43 | 42 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
cyclShift
Word
|
44 | 43 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . 21
cyclShift Word |
45 | 32, 44 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
..^
cyclShift Word |
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ cyclShift Word
|
47 | 46 | impcom 446 |
. . . . . . . . . . . . . . . . . 18
cyclShift Word ..^ ..^
|
48 | | zmodfzo 12693 |
. . . . . . . . . . . . . . . . . 18
..^ |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
cyclShift Word ..^ ..^
..^ |
50 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
51 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
54 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
55 | 53, 54 | zaddcld 11486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
56 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
57 | 56 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
58 | 55, 57 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
59 | 58 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
60 | 59 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
61 | 50, 60 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
62 | 61 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
63 | 62 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . 20
cyclShift Word ..^ |
64 | 63 | adantld 483 |
. . . . . . . . . . . . . . . . . . 19
cyclShift Word ..^ ..^ |
65 | 64 | imp 445 |
. . . . . . . . . . . . . . . . . 18
cyclShift Word ..^ ..^
|
66 | | zmodfzo 12693 |
. . . . . . . . . . . . . . . . . 18
..^ |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
cyclShift Word ..^ ..^
..^ |
68 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 68 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
|
70 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 69, 70 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
|
72 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
73 | 72 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
|
74 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 73, 74 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
|
76 | 71, 75 | rspc2v 3322 |
. . . . . . . . . . . . . . . . 17
..^
..^ ..^
..^ |
77 | 49, 67, 76 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
cyclShift Word ..^ ..^
..^ ..^
|
78 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
cyclShift
Word
..^ ..^
|
79 | | addmodlteq 12745 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ ..^
|
80 | 79 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ ..^
|
81 | 80 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^
|
82 | 81 | bicomd 213 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
|
83 | 82 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
84 | 83 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . 20
cyclShift Word ..^ ..^
|
85 | 84 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
cyclShift Word ..^ ..^
|
86 | 85 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
cyclShift
Word
..^ ..^
|
87 | 78, 86 | sylibrd 249 |
. . . . . . . . . . . . . . . . 17
cyclShift
Word
..^ ..^
|
88 | 87 | ex 450 |
. . . . . . . . . . . . . . . 16
cyclShift Word ..^ ..^
|
89 | 77, 88 | syld 47 |
. . . . . . . . . . . . . . 15
cyclShift Word ..^ ..^
..^ ..^
|
90 | 89 | impancom 456 |
. . . . . . . . . . . . . 14
cyclShift Word
..^ ..^
..^ ..^
|
91 | 90 | imp 445 |
. . . . . . . . . . . . 13
cyclShift
Word
..^ ..^
..^
..^
|
92 | 31, 91 | sylbid 230 |
. . . . . . . . . . . 12
cyclShift
Word
..^ ..^
..^
..^
|
93 | 92 | ralrimivva 2971 |
. . . . . . . . . . 11
cyclShift Word
..^ ..^
..^
..^ |
94 | 93 | 3exp1 1283 |
. . . . . . . . . 10
cyclShift Word
..^ ..^
..^ ..^ |
95 | 94 | com14 96 |
. . . . . . . . 9
..^ ..^
Word cyclShift ..^
..^ |
96 | 95 | adantl 482 |
. . . . . . . 8
..^ ..^ ..^
Word
cyclShift ..^ ..^ |
97 | 10, 96 | sylbi 207 |
. . . . . . 7
..^
Word
cyclShift ..^
..^ |
98 | 97 | 3imp1 1280 |
. . . . . 6
..^
Word cyclShift
..^
..^ |
99 | 9, 98 | jca 554 |
. . . . 5
..^
Word cyclShift
..^
..^ ..^ |
100 | 99 | 3exp1 1283 |
. . . 4
..^
Word
cyclShift ..^
..^ ..^ |
101 | 3, 100 | mpd 15 |
. . 3
..^
cyclShift
..^
..^ ..^ |
102 | 101 | 3imp 1256 |
. 2
..^
cyclShift
..^
..^ ..^ |
103 | | dff13 6512 |
. 2
..^
..^ ..^
..^ |
104 | 102, 103 | sylibr 224 |
1
..^
cyclShift
..^ |