Proof of Theorem cshweqdif2
Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . . . 9
Word
Word Word |
2 | 1 | adantr 481 |
. . . . . . . 8
Word
Word
Word |
3 | | zsubcl 11419 |
. . . . . . . . . 10
|
4 | 3 | ancoms 469 |
. . . . . . . . 9
|
5 | 4 | adantl 482 |
. . . . . . . 8
Word
Word |
6 | | simpr 477 |
. . . . . . . . 9
|
7 | 6 | adantl 482 |
. . . . . . . 8
Word
Word
|
8 | 2, 5, 7 | 3jca 1242 |
. . . . . . 7
Word
Word Word
|
9 | 8 | adantr 481 |
. . . . . 6
Word Word
cyclShift cyclShift
Word |
10 | | 3cshw 13564 |
. . . . . 6
Word
cyclShift
cyclShift
cyclShift cyclShift |
11 | 9, 10 | syl 17 |
. . . . 5
Word Word
cyclShift cyclShift
cyclShift cyclShift
cyclShift cyclShift |
12 | | simpl 473 |
. . . . . . . . . 10
Word
Word Word
Word |
13 | 12 | ancomd 467 |
. . . . . . . . 9
Word
Word Word
Word |
14 | 13 | adantr 481 |
. . . . . . . 8
Word Word
cyclShift cyclShift
Word Word |
15 | | simpr 477 |
. . . . . . . . . 10
Word
Word |
16 | 15 | ancomd 467 |
. . . . . . . . 9
Word
Word |
17 | 16 | adantr 481 |
. . . . . . . 8
Word Word
cyclShift cyclShift
|
18 | | simpr 477 |
. . . . . . . . 9
Word Word
cyclShift cyclShift
cyclShift cyclShift |
19 | 18 | eqcomd 2628 |
. . . . . . . 8
Word Word
cyclShift cyclShift
cyclShift cyclShift |
20 | | cshwleneq 13563 |
. . . . . . . 8
Word
Word cyclShift cyclShift |
21 | 14, 17, 19, 20 | syl3anc 1326 |
. . . . . . 7
Word Word
cyclShift cyclShift
|
22 | 21 | oveq1d 6665 |
. . . . . 6
Word Word
cyclShift cyclShift
|
23 | 22 | oveq2d 6666 |
. . . . 5
Word Word
cyclShift cyclShift
cyclShift cyclShift
cyclShift cyclShift
cyclShift cyclShift |
24 | 11, 23 | eqtrd 2656 |
. . . 4
Word Word
cyclShift cyclShift
cyclShift cyclShift
cyclShift cyclShift |
25 | 19 | oveq1d 6665 |
. . . . . 6
Word Word
cyclShift cyclShift
cyclShift cyclShift
cyclShift cyclShift
|
26 | | simpl 473 |
. . . . . . . . . 10
Word
Word Word |
27 | 26 | adantr 481 |
. . . . . . . . 9
Word
Word
Word |
28 | | simpl 473 |
. . . . . . . . . 10
|
29 | 28 | adantl 482 |
. . . . . . . . 9
Word
Word
|
30 | 27, 29, 5 | 3jca 1242 |
. . . . . . . 8
Word
Word Word
|
31 | 30 | adantr 481 |
. . . . . . 7
Word Word
cyclShift cyclShift
Word |
32 | | 2cshw 13559 |
. . . . . . 7
Word
cyclShift cyclShift
cyclShift
|
33 | 31, 32 | syl 17 |
. . . . . 6
Word Word
cyclShift cyclShift
cyclShift cyclShift
cyclShift
|
34 | | zcn 11382 |
. . . . . . . . . . 11
|
35 | | zcn 11382 |
. . . . . . . . . . 11
|
36 | 34, 35 | anim12i 590 |
. . . . . . . . . 10
|
37 | 36 | adantl 482 |
. . . . . . . . 9
Word
Word |
38 | 37 | adantr 481 |
. . . . . . . 8
Word Word
cyclShift cyclShift
|
39 | | pncan3 10289 |
. . . . . . . 8
|
40 | 38, 39 | syl 17 |
. . . . . . 7
Word Word
cyclShift cyclShift
|
41 | 40 | oveq2d 6666 |
. . . . . 6
Word Word
cyclShift cyclShift
cyclShift cyclShift |
42 | 25, 33, 41 | 3eqtrd 2660 |
. . . . 5
Word Word
cyclShift cyclShift
cyclShift cyclShift
cyclShift
|
43 | 42 | oveq1d 6665 |
. . . 4
Word Word
cyclShift cyclShift
cyclShift cyclShift
cyclShift cyclShift cyclShift
|
44 | | lencl 13324 |
. . . . . . . . . 10
Word |
45 | 44 | nn0zd 11480 |
. . . . . . . . 9
Word |
46 | 45 | adantr 481 |
. . . . . . . 8
Word
Word |
47 | | zsubcl 11419 |
. . . . . . . 8
|
48 | 46, 6, 47 | syl2an 494 |
. . . . . . 7
Word
Word |
49 | 27, 7, 48 | 3jca 1242 |
. . . . . 6
Word
Word Word
|
50 | 49 | adantr 481 |
. . . . 5
Word Word
cyclShift cyclShift
Word |
51 | | 2cshw 13559 |
. . . . 5
Word
cyclShift cyclShift cyclShift |
52 | 50, 51 | syl 17 |
. . . 4
Word Word
cyclShift cyclShift
cyclShift cyclShift
cyclShift
|
53 | 24, 43, 52 | 3eqtrd 2660 |
. . 3
Word Word
cyclShift cyclShift
cyclShift cyclShift
|
54 | 44 | nn0cnd 11353 |
. . . . . . . . 9
Word |
55 | 54 | adantr 481 |
. . . . . . . 8
Word
Word |
56 | 35 | adantl 482 |
. . . . . . . 8
|
57 | 55, 56 | anim12i 590 |
. . . . . . 7
Word
Word
|
58 | 57 | ancomd 467 |
. . . . . 6
Word
Word |
59 | 58 | adantr 481 |
. . . . 5
Word Word
cyclShift cyclShift
|
60 | | pncan3 10289 |
. . . . 5
|
61 | 59, 60 | syl 17 |
. . . 4
Word Word
cyclShift cyclShift
|
62 | 61 | oveq2d 6666 |
. . 3
Word Word
cyclShift cyclShift
cyclShift cyclShift |
63 | | cshwn 13543 |
. . . . 5
Word cyclShift |
64 | 27, 63 | syl 17 |
. . . 4
Word
Word
cyclShift |
65 | 64 | adantr 481 |
. . 3
Word Word
cyclShift cyclShift
cyclShift |
66 | 53, 62, 65 | 3eqtrd 2660 |
. 2
Word Word
cyclShift cyclShift
cyclShift |
67 | 66 | ex 450 |
1
Word
Word cyclShift cyclShift cyclShift |