Step | Hyp | Ref
| Expression |
1 | | crctcsh.h |
. . . . 5
cyclShift
|
2 | | crctcsh.d |
. . . . . . 7
Circuits |
3 | | crctiswlk 26691 |
. . . . . . 7
Circuits Walks |
4 | | crctcsh.i |
. . . . . . . 8
iEdg |
5 | 4 | wlkf 26510 |
. . . . . . 7
Walks Word |
6 | 2, 3, 5 | 3syl 18 |
. . . . . 6
Word |
7 | | cshwcl 13544 |
. . . . . 6
Word
cyclShift Word |
8 | 6, 7 | syl 17 |
. . . . 5
cyclShift
Word |
9 | 1, 8 | syl5eqel 2705 |
. . . 4
Word |
10 | 9 | adantr 481 |
. . 3
Word |
11 | 2, 3 | syl 17 |
. . . . . . . 8
Walks |
12 | | crctcsh.v |
. . . . . . . . . 10
Vtx |
13 | 12 | wlkp 26512 |
. . . . . . . . 9
Walks |
14 | | simpll 790 |
. . . . . . . . . . . 12
|
15 | | crctcsh.s |
. . . . . . . . . . . . . . 15
..^ |
16 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 16 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
..^ |
18 | | elfzonn0 12512 |
. . . . . . . . . . . . . . . . . . 19
..^
|
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
..^ |
20 | 17, 19 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . 17
..^ |
21 | 20 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^
|
22 | | crctcsh.n |
. . . . . . . . . . . . . . . . . 18
|
23 | | elfz3nn0 12434 |
. . . . . . . . . . . . . . . . . 18
|
24 | 22, 23 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . . 17
|
25 | 24 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
..^
|
26 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . 21
|
27 | 26 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | 27 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
..^ |
29 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
30 | 29 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ |
32 | | elfzel2 12340 |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | 32 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | 33 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
..^ |
35 | | leaddsub 10504 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 28, 31, 34, 35 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
..^
|
37 | 36 | biimpar 502 |
. . . . . . . . . . . . . . . . 17
..^
|
38 | 37, 22 | syl6breq 4694 |
. . . . . . . . . . . . . . . 16
..^
|
39 | 21, 25, 38 | 3jca 1242 |
. . . . . . . . . . . . . . 15
..^
|
40 | 15, 39 | sylanl1 682 |
. . . . . . . . . . . . . 14
|
41 | | elfz2nn0 12431 |
. . . . . . . . . . . . . 14
|
42 | 40, 41 | sylibr 224 |
. . . . . . . . . . . . 13
|
43 | 42 | adantll 750 |
. . . . . . . . . . . 12
|
44 | 14, 43 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
45 | | simpll 790 |
. . . . . . . . . . . 12
|
46 | | elfzoel2 12469 |
. . . . . . . . . . . . . . . . . . 19
..^
|
47 | | zaddcl 11417 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
48 | 47 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
49 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
50 | 48, 49 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
52 | | zsubcl 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
53 | 52 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
54 | 53 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
55 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
56 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
57 | 54, 55, 56 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
58 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
60 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
62 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
63 | | ltsubadd 10498 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
64 | 59, 61, 62, 63 | syl2an23an 1387 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
65 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
66 | 48 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
67 | 65, 66 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
68 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
69 | 50 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
70 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
71 | 68, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
72 | 67, 71 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
73 | 64, 72 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
74 | 57, 73 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
75 | 74 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . 22
|
76 | 51, 75 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
|
77 | 76 | exp31 630 |
. . . . . . . . . . . . . . . . . . . 20
|
78 | 77, 26 | syl11 33 |
. . . . . . . . . . . . . . . . . . 19
|
79 | 29, 46, 78 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
..^
|
80 | 79 | imp31 448 |
. . . . . . . . . . . . . . . . 17
..^
|
81 | | elnn0z 11390 |
. . . . . . . . . . . . . . . . 17
|
82 | 80, 81 | sylibr 224 |
. . . . . . . . . . . . . . . 16
..^
|
83 | 24 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
..^
|
84 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
85 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . 21
|
86 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
87 | 86 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
88 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
89 | 88 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
90 | 87, 89 | anim12ci 591 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
91 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
92 | 91, 91 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
93 | 92 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
95 | 90, 94 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . 22
|
96 | | simpr3 1069 |
. . . . . . . . . . . . . . . . . . . . . 22
|
97 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
98 | 86, 91, 97 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | 98 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 99 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | 95, 96, 100 | jca32 558 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | 84, 85, 101 | syl2anb 496 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
103 | | le2add 10510 |
. . . . . . . . . . . . . . . . . . . . 21
|
104 | 103 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | 102, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
..^ |
106 | 66, 65, 65 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
107 | 106 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
108 | 107, 26 | syl11 33 |
. . . . . . . . . . . . . . . . . . . . . 22
|
109 | 29, 46, 108 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
110 | 109 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
111 | | lesubadd 10500 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
..^
|
113 | 105, 112 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
..^ |
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^
|
115 | 114, 22 | syl6breq 4694 |
. . . . . . . . . . . . . . . 16
..^
|
116 | 82, 83, 115 | 3jca 1242 |
. . . . . . . . . . . . . . 15
..^
|
117 | 15, 116 | sylanl1 682 |
. . . . . . . . . . . . . 14
|
118 | | elfz2nn0 12431 |
. . . . . . . . . . . . . 14
|
119 | 117, 118 | sylibr 224 |
. . . . . . . . . . . . 13
|
120 | 119 | adantll 750 |
. . . . . . . . . . . 12
|
121 | 45, 120 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
122 | 44, 121 | ifclda 4120 |
. . . . . . . . . 10
|
123 | 122 | exp32 631 |
. . . . . . . . 9
|
124 | 13, 123 | syl 17 |
. . . . . . . 8
Walks
|
125 | 11, 124 | mpcom 38 |
. . . . . . 7
|
126 | 125 | imp 445 |
. . . . . 6
|
127 | | crctcsh.q |
. . . . . 6
|
128 | 126, 127 | fmptd 6385 |
. . . . 5
|
129 | 12, 4, 2, 22, 15, 1 | crctcshlem2 26710 |
. . . . . . 7
|
130 | 129 | oveq2d 6666 |
. . . . . 6
|
131 | 130 | feq2d 6031 |
. . . . 5
|
132 | 128, 131 | mpbird 247 |
. . . 4
|
133 | 132 | adantr 481 |
. . 3
|
134 | 12, 4 | wlkprop 26507 |
. . . . . 6
Walks Word ..^if- |
135 | 2, 3, 134 | 3syl 18 |
. . . . 5
Word ..^if- |
136 | 135 | adantr 481 |
. . . 4
Word ..^if- |
137 | 22 | eqcomi 2631 |
. . . . . . . . . 10
|
138 | 137 | oveq2i 6661 |
. . . . . . . . 9
..^ ..^ |
139 | 138 | raleqi 3142 |
. . . . . . . 8
..^if-
..^if- |
140 | | fzo1fzo0n0 12518 |
. . . . . . . . . . . . . . 15
..^ ..^ |
141 | 140 | simplbi2 655 |
. . . . . . . . . . . . . 14
..^
..^ |
142 | 15, 141 | syl 17 |
. . . . . . . . . . . . 13
..^ |
143 | 142 | imp 445 |
. . . . . . . . . . . 12
..^ |
144 | 143 | ad2antlr 763 |
. . . . . . . . . . 11
Word
..^if-
..^ |
145 | | simplll 798 |
. . . . . . . . . . 11
Word
..^if-
Word |
146 | | wkslem1 26503 |
. . . . . . . . . . . . . 14
if-
if- |
147 | 146 | cbvralv 3171 |
. . . . . . . . . . . . 13
..^if-
..^if- |
148 | 147 | biimpi 206 |
. . . . . . . . . . . 12
..^if- ..^if- |
149 | 148 | adantl 482 |
. . . . . . . . . . 11
Word
..^if-
..^if- |
150 | | crctprop 26687 |
. . . . . . . . . . . . . 14
Circuits Trails |
151 | 137 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . 18
|
152 | 151 | eqeq2i 2634 |
. . . . . . . . . . . . . . . . 17
|
153 | 152 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
154 | 153 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
|
155 | 154 | adantl 482 |
. . . . . . . . . . . . . 14
Trails |
156 | 2, 150, 155 | 3syl 18 |
. . . . . . . . . . . . 13
|
157 | 156 | ad2antrl 764 |
. . . . . . . . . . . 12
Word
|
158 | 157 | adantr 481 |
. . . . . . . . . . 11
Word
..^if-
|
159 | 144, 127,
1, 22, 145, 149, 158 | crctcshwlkn0lem7 26708 |
. . . . . . . . . 10
Word
..^if-
..^if- |
160 | 129 | oveq2d 6666 |
. . . . . . . . . . . . 13
..^ ..^ |
161 | 160 | raleqdv 3144 |
. . . . . . . . . . . 12
..^if-
..^if- |
162 | 161 | ad2antrl 764 |
. . . . . . . . . . 11
Word
..^if-
..^if- |
163 | 162 | adantr 481 |
. . . . . . . . . 10
Word
..^if-
..^if-
..^if- |
164 | 159, 163 | mpbird 247 |
. . . . . . . . 9
Word
..^if-
..^if- |
165 | 164 | ex 450 |
. . . . . . . 8
Word
..^if- ..^if- |
166 | 139, 165 | syl5bi 232 |
. . . . . . 7
Word
..^if- ..^if- |
167 | 166 | ex 450 |
. . . . . 6
Word ..^if- ..^if- |
168 | 167 | com23 86 |
. . . . 5
Word ..^if-
..^if- |
169 | 168 | 3impia 1261 |
. . . 4
Word ..^if-
..^if- |
170 | 136, 169 | mpcom 38 |
. . 3
..^if- |
171 | 10, 133, 170 | 3jca 1242 |
. 2
Word ..^if- |
172 | 12, 4, 2, 22, 15, 1, 127 | crctcshlem3 26711 |
. . . 4
|
173 | 172 | adantr 481 |
. . 3
|
174 | 12, 4 | iswlk 26506 |
. . 3
Walks Word ..^if- |
175 | 173, 174 | syl 17 |
. 2
Walks Word ..^if- |
176 | 171, 175 | mpbird 247 |
1
Walks |