Proof of Theorem crctcshwlkn0lem6
Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . . . . . . 9
|
2 | | 0p1e1 11132 |
. . . . . . . . 9
|
3 | 1, 2 | syl6eq 2672 |
. . . . . . . 8
|
4 | | wkslem2 26504 |
. . . . . . . 8
if- if- |
5 | 3, 4 | mpdan 702 |
. . . . . . 7
if-
if- |
6 | | crctcshwlkn0lem.p |
. . . . . . 7
..^if- |
7 | | crctcshwlkn0lem.s |
. . . . . . . . 9
..^ |
8 | | elfzo1 12517 |
. . . . . . . . . 10
..^ |
9 | | simp2 1062 |
. . . . . . . . . 10
|
10 | 8, 9 | sylbi 207 |
. . . . . . . . 9
..^
|
11 | 7, 10 | syl 17 |
. . . . . . . 8
|
12 | | lbfzo0 12507 |
. . . . . . . 8
..^
|
13 | 11, 12 | sylibr 224 |
. . . . . . 7
..^ |
14 | 5, 6, 13 | rspcdva 3316 |
. . . . . 6
if- |
15 | | crctcshwlkn0lem.e |
. . . . . . 7
|
16 | | eqeq1 2626 |
. . . . . . . 8
|
17 | | sneq 4187 |
. . . . . . . . 9
|
18 | 17 | eqeq2d 2632 |
. . . . . . . 8
|
19 | | preq1 4268 |
. . . . . . . . 9
|
20 | 19 | sseq1d 3632 |
. . . . . . . 8
|
21 | 16, 18, 20 | ifpbi123d 1027 |
. . . . . . 7
if-
if- |
22 | 15, 21 | syl 17 |
. . . . . 6
if-
if- |
23 | 14, 22 | mpbird 247 |
. . . . 5
if- |
24 | | nncn 11028 |
. . . . . . . . . 10
|
25 | | nncn 11028 |
. . . . . . . . . 10
|
26 | | npcan 10290 |
. . . . . . . . . 10
|
27 | 24, 25, 26 | syl2anr 495 |
. . . . . . . . 9
|
28 | | simpr 477 |
. . . . . . . . . 10
|
29 | | oveq1 6657 |
. . . . . . . . . . 11
|
30 | | crctcshwlkn0lem.n |
. . . . . . . . . . . . . . 15
|
31 | 30 | eqcomi 2631 |
. . . . . . . . . . . . . 14
|
32 | 31 | a1i 11 |
. . . . . . . . . . . . 13
|
33 | 32 | oveq2d 6666 |
. . . . . . . . . . . 12
|
34 | | nnrp 11842 |
. . . . . . . . . . . . . 14
|
35 | | modid0 12696 |
. . . . . . . . . . . . . 14
|
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
|
37 | 36 | adantl 482 |
. . . . . . . . . . . 12
|
38 | 33, 37 | eqtrd 2656 |
. . . . . . . . . . 11
|
39 | 29, 38 | sylan9eqr 2678 |
. . . . . . . . . 10
|
40 | | simpl 473 |
. . . . . . . . . 10
|
41 | 28, 39, 40 | 3jca 1242 |
. . . . . . . . 9
|
42 | 27, 41 | mpdan 702 |
. . . . . . . 8
|
43 | 42 | 3adant3 1081 |
. . . . . . 7
|
44 | 8, 43 | sylbi 207 |
. . . . . 6
..^
|
45 | | simp1 1061 |
. . . . . . . . 9
|
46 | 45 | fveq2d 6195 |
. . . . . . . 8
|
47 | 46 | eqeq1d 2624 |
. . . . . . 7
|
48 | | simp2 1062 |
. . . . . . . . . 10
|
49 | 48 | fveq2d 6195 |
. . . . . . . . 9
|
50 | 49 | fveq2d 6195 |
. . . . . . . 8
|
51 | 46 | sneqd 4189 |
. . . . . . . 8
|
52 | 50, 51 | eqeq12d 2637 |
. . . . . . 7
|
53 | 46 | preq1d 4274 |
. . . . . . . 8
|
54 | 53, 50 | sseq12d 3634 |
. . . . . . 7
|
55 | 47, 52, 54 | ifpbi123d 1027 |
. . . . . 6
if- if- |
56 | 7, 44, 55 | 3syl 18 |
. . . . 5
if- if- |
57 | 23, 56 | mpbird 247 |
. . . 4
if- |
58 | | nnsub 11059 |
. . . . . . . . . . 11
|
59 | 58 | biimp3a 1432 |
. . . . . . . . . 10
|
60 | 59 | nnnn0d 11351 |
. . . . . . . . 9
|
61 | 8, 60 | sylbi 207 |
. . . . . . . 8
..^
|
62 | 7, 61 | syl 17 |
. . . . . . 7
|
63 | | nn0fz0 12437 |
. . . . . . 7
|
64 | 62, 63 | sylib 208 |
. . . . . 6
|
65 | | crctcshwlkn0lem.q |
. . . . . . 7
|
66 | 7, 65 | crctcshwlkn0lem2 26703 |
. . . . . 6
|
67 | 64, 66 | mpdan 702 |
. . . . 5
|
68 | | elfzoel2 12469 |
. . . . . . . . . . . . 13
..^
|
69 | | elfzoelz 12470 |
. . . . . . . . . . . . 13
..^
|
70 | 68, 69 | zsubcld 11487 |
. . . . . . . . . . . 12
..^
|
71 | 70 | peano2zd 11485 |
. . . . . . . . . . 11
..^
|
72 | | nnre 11027 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | anim1i 592 |
. . . . . . . . . . . . . . 15
|
74 | 73 | ancoms 469 |
. . . . . . . . . . . . . 14
|
75 | | crctcshwlkn0lem1 26702 |
. . . . . . . . . . . . . 14
|
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
|
77 | 76 | 3adant3 1081 |
. . . . . . . . . . . 12
|
78 | 8, 77 | sylbi 207 |
. . . . . . . . . . 11
..^
|
79 | 71, 68, 78 | 3jca 1242 |
. . . . . . . . . 10
..^
|
80 | 7, 79 | syl 17 |
. . . . . . . . 9
|
81 | | eluz2 11693 |
. . . . . . . . 9
|
82 | 80, 81 | sylibr 224 |
. . . . . . . 8
|
83 | | eluzfz1 12348 |
. . . . . . . 8
|
84 | 82, 83 | syl 17 |
. . . . . . 7
|
85 | 7, 65 | crctcshwlkn0lem3 26704 |
. . . . . . 7
|
86 | 84, 85 | mpdan 702 |
. . . . . 6
|
87 | | subcl 10280 |
. . . . . . . . . . . . . 14
|
88 | 87 | ancoms 469 |
. . . . . . . . . . . . 13
|
89 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
90 | | pncan2 10288 |
. . . . . . . . . . . . . 14
|
91 | 90 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
92 | 88, 89, 91 | sylancl 694 |
. . . . . . . . . . . 12
|
93 | | peano2cn 10208 |
. . . . . . . . . . . . . 14
|
94 | 88, 93 | syl 17 |
. . . . . . . . . . . . 13
|
95 | | simpr 477 |
. . . . . . . . . . . . 13
|
96 | | simpl 473 |
. . . . . . . . . . . . 13
|
97 | 94, 95, 96 | subsub3d 10422 |
. . . . . . . . . . . 12
|
98 | 92, 97 | eqtr2d 2657 |
. . . . . . . . . . 11
|
99 | 25, 24, 98 | syl2an 494 |
. . . . . . . . . 10
|
100 | 99 | 3adant3 1081 |
. . . . . . . . 9
|
101 | 8, 100 | sylbi 207 |
. . . . . . . 8
..^
|
102 | 7, 101 | syl 17 |
. . . . . . 7
|
103 | 102 | fveq2d 6195 |
. . . . . 6
|
104 | 86, 103 | eqtrd 2656 |
. . . . 5
|
105 | | crctcshwlkn0lem.h |
. . . . . . 7
cyclShift
|
106 | 105 | fveq1i 6192 |
. . . . . 6
cyclShift |
107 | | crctcshwlkn0lem.f |
. . . . . . . . 9
Word |
108 | 107 | adantr 481 |
. . . . . . . 8
..^ Word |
109 | 69 | adantl 482 |
. . . . . . . 8
..^ |
110 | | elfzofz 12485 |
. . . . . . . . . . 11
..^
|
111 | | ubmelfzo 12532 |
. . . . . . . . . . 11
..^ |
112 | 110, 111 | syl 17 |
. . . . . . . . . 10
..^
..^ |
113 | 112 | adantl 482 |
. . . . . . . . 9
..^ ..^ |
114 | 31 | oveq2i 6661 |
. . . . . . . . 9
..^ ..^ |
115 | 113, 114 | syl6eleqr 2712 |
. . . . . . . 8
..^ ..^ |
116 | | cshwidxmod 13549 |
. . . . . . . 8
Word
..^ cyclShift
|
117 | 108, 109,
115, 116 | syl3anc 1326 |
. . . . . . 7
..^ cyclShift
|
118 | 7, 117 | mpdan 702 |
. . . . . 6
cyclShift
|
119 | 106, 118 | syl5eq 2668 |
. . . . 5
|
120 | | simp1 1061 |
. . . . . . 7
|
121 | | simp2 1062 |
. . . . . . 7
|
122 | 120, 121 | eqeq12d 2637 |
. . . . . 6
|
123 | | simp3 1063 |
. . . . . . . 8
|
124 | 123 | fveq2d 6195 |
. . . . . . 7
|
125 | 120 | sneqd 4189 |
. . . . . . 7
|
126 | 124, 125 | eqeq12d 2637 |
. . . . . 6
|
127 | 120, 121 | preq12d 4276 |
. . . . . . 7
|
128 | 127, 124 | sseq12d 3634 |
. . . . . 6
|
129 | 122, 126,
128 | ifpbi123d 1027 |
. . . . 5
if- if- |
130 | 67, 104, 119, 129 | syl3anc 1326 |
. . . 4
if-
if-
|
131 | 57, 130 | mpbird 247 |
. . 3
if-
|
132 | 131 | adantr 481 |
. 2
if- |
133 | | wkslem1 26503 |
. . 3
if-
if-
|
134 | 133 | adantl 482 |
. 2
if-
if-
|
135 | 132, 134 | mpbird 247 |
1
if-
|