Description: The singletons resulting by cyclically shifting a given word of length being a prime number and not consisting of identical symbols is a disjoint collection. (Contributed by Alexander van der Vekens, 19-May-2018) (Revised by Alexander van der Vekens, 8-Jun-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cshwshash.0 | |
|
Assertion | cshwsdisj | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cshwshash.0 | |
|
2 | orc | |
|
3 | 2 | a1d | |
4 | simprl | |
|
5 | simprrl | |
|
6 | simprrr | |
|
7 | necom | |
|
8 | 7 | biimpi | |
9 | 8 | adantr | |
10 | 1 | cshwshashlem3 | |
11 | 10 | imp | |
12 | 4 5 6 9 11 | syl13anc | |
13 | disjsn2 | |
|
14 | 12 13 | syl | |
15 | 14 | olcd | |
16 | 15 | ex | |
17 | 3 16 | pm2.61ine | |
18 | 17 | ralrimivva | |
19 | oveq2 | |
|
20 | 19 | sneqd | |
21 | 20 | disjor | |
22 | 18 21 | sylibr | |