Proof of Theorem eucrct2eupth
Step | Hyp | Ref
| Expression |
1 | | eucrct2eupth1.v |
. . . 4
Vtx |
2 | | eucrct2eupth1.i |
. . . 4
iEdg |
3 | | eucrct2eupth1.d |
. . . . . 6
EulerPaths |
4 | 3 | adantl 482 |
. . . . 5
EulerPaths |
5 | | eucrct2eupth.k |
. . . . . . . 8
|
6 | 5 | eqcomi 2631 |
. . . . . . 7
|
7 | 6 | oveq2i 6661 |
. . . . . 6
cyclShift
cyclShift |
8 | | oveq1 6657 |
. . . . . . . . 9
|
9 | | eucrct2eupth.j |
. . . . . . . . . 10
..^ |
10 | | elfzo0 12508 |
. . . . . . . . . . 11
..^
|
11 | | nncn 11028 |
. . . . . . . . . . . 12
|
12 | 11 | 3ad2ant2 1083 |
. . . . . . . . . . 11
|
13 | 10, 12 | sylbi 207 |
. . . . . . . . . 10
..^
|
14 | | npcan1 10455 |
. . . . . . . . . 10
|
15 | 9, 13, 14 | 3syl 18 |
. . . . . . . . 9
|
16 | 8, 15 | sylan9eq 2676 |
. . . . . . . 8
|
17 | 16 | oveq2d 6666 |
. . . . . . 7
cyclShift cyclShift |
18 | | eucrct2eupth.n |
. . . . . . . . . 10
|
19 | 18 | oveq2d 6666 |
. . . . . . . . 9
cyclShift
cyclShift |
20 | | eucrct2eupth1.c |
. . . . . . . . . . 11
Circuits |
21 | | crctiswlk 26691 |
. . . . . . . . . . . 12
Circuits Walks |
22 | 2 | wlkf 26510 |
. . . . . . . . . . . 12
Walks Word |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
Circuits Word |
24 | 20, 23 | syl 17 |
. . . . . . . . . 10
Word |
25 | | cshwn 13543 |
. . . . . . . . . 10
Word
cyclShift |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
cyclShift
|
27 | 19, 26 | eqtrd 2656 |
. . . . . . . 8
cyclShift
|
28 | 27 | adantl 482 |
. . . . . . 7
cyclShift |
29 | 17, 28 | eqtrd 2656 |
. . . . . 6
cyclShift |
30 | 7, 29 | syl5eqr 2670 |
. . . . 5
cyclShift |
31 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
32 | 1, 2, 20, 31 | crctcshlem1 26709 |
. . . . . . . . . . . . 13
|
33 | | fz0sn0fz1 12456 |
. . . . . . . . . . . . 13
|
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
|
35 | 34 | eleq2d 2687 |
. . . . . . . . . . 11
|
36 | | elun 3753 |
. . . . . . . . . . 11
|
37 | 35, 36 | syl6bb 276 |
. . . . . . . . . 10
|
38 | | elsni 4194 |
. . . . . . . . . . . . . . . 16
|
39 | | 0le0 11110 |
. . . . . . . . . . . . . . . 16
|
40 | 38, 39 | syl6eqbr 4692 |
. . . . . . . . . . . . . . 15
|
41 | 40 | adantl 482 |
. . . . . . . . . . . . . 14
|
42 | 41 | iftrued 4094 |
. . . . . . . . . . . . 13
|
43 | 18 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
44 | | crctprop 26687 |
. . . . . . . . . . . . . . . . . 18
Circuits Trails |
45 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
Trails |
46 | 45 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
Trails |
47 | 20, 44, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
48 | 43, 47 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . 15
|
50 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
51 | 9, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
52 | 51 | addid2d 10237 |
. . . . . . . . . . . . . . . . 17
|
53 | 50, 52 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
55 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . 15
|
57 | 49, 54, 56 | 3eqtr4d 2666 |
. . . . . . . . . . . . . 14
|
58 | 38, 57 | sylan2 491 |
. . . . . . . . . . . . 13
|
59 | 42, 58 | eqtrd 2656 |
. . . . . . . . . . . 12
|
60 | 59 | ex 450 |
. . . . . . . . . . 11
|
61 | | elfznn 12370 |
. . . . . . . . . . . . . . . 16
|
62 | | nnnle0 11051 |
. . . . . . . . . . . . . . . 16
|
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
|
64 | 63 | adantl 482 |
. . . . . . . . . . . . . 14
|
65 | 64 | iffalsed 4097 |
. . . . . . . . . . . . 13
|
66 | 61 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | adantl 482 |
. . . . . . . . . . . . . . 15
|
68 | 51 | adantr 481 |
. . . . . . . . . . . . . . 15
|
69 | 67, 68 | pncand 10393 |
. . . . . . . . . . . . . 14
|
70 | 69 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
71 | 65, 70 | eqtrd 2656 |
. . . . . . . . . . . 12
|
72 | 71 | ex 450 |
. . . . . . . . . . 11
|
73 | 60, 72 | jaod 395 |
. . . . . . . . . 10
|
74 | 37, 73 | sylbid 230 |
. . . . . . . . 9
|
75 | 74 | imp 445 |
. . . . . . . 8
|
76 | 75 | mpteq2dva 4744 |
. . . . . . 7
|
77 | 76 | adantl 482 |
. . . . . 6
|
78 | 5 | oveq2i 6661 |
. . . . . . . . . 10
|
79 | 8 | oveq2d 6666 |
. . . . . . . . . . 11
|
80 | 15 | oveq2d 6666 |
. . . . . . . . . . . 12
|
81 | 51 | subidd 10380 |
. . . . . . . . . . . 12
|
82 | 80, 81 | eqtrd 2656 |
. . . . . . . . . . 11
|
83 | 79, 82 | sylan9eq 2676 |
. . . . . . . . . 10
|
84 | 78, 83 | syl5eq 2668 |
. . . . . . . . 9
|
85 | 84 | breq2d 4665 |
. . . . . . . 8
|
86 | 5 | oveq2i 6661 |
. . . . . . . . . 10
|
87 | 86 | fveq2i 6194 |
. . . . . . . . 9
|
88 | 8 | oveq2d 6666 |
. . . . . . . . . . 11
|
89 | 15 | oveq2d 6666 |
. . . . . . . . . . 11
|
90 | 88, 89 | sylan9eq 2676 |
. . . . . . . . . 10
|
91 | 90 | fveq2d 6195 |
. . . . . . . . 9
|
92 | 87, 91 | syl5eq 2668 |
. . . . . . . 8
|
93 | 86 | oveq1i 6660 |
. . . . . . . . . 10
|
94 | 93 | fveq2i 6194 |
. . . . . . . . 9
|
95 | 88 | oveq1d 6665 |
. . . . . . . . . . 11
|
96 | 89 | oveq1d 6665 |
. . . . . . . . . . 11
|
97 | 95, 96 | sylan9eq 2676 |
. . . . . . . . . 10
|
98 | 97 | fveq2d 6195 |
. . . . . . . . 9
|
99 | 94, 98 | syl5eq 2668 |
. . . . . . . 8
|
100 | 85, 92, 99 | ifbieq12d 4113 |
. . . . . . 7
|
101 | 100 | mpteq2dv 4745 |
. . . . . 6
|
102 | 20, 21 | syl 17 |
. . . . . . . . 9
Walks |
103 | 1 | wlkp 26512 |
. . . . . . . . 9
Walks |
104 | | ffn 6045 |
. . . . . . . . 9
|
105 | 102, 103,
104 | 3syl 18 |
. . . . . . . 8
|
106 | 105 | adantl 482 |
. . . . . . 7
|
107 | | dffn5 6241 |
. . . . . . 7
|
108 | 106, 107 | sylib 208 |
. . . . . 6
|
109 | 77, 101, 108 | 3eqtr4d 2666 |
. . . . 5
|
110 | 4, 30, 109 | 3brtr4d 4685 |
. . . 4
cyclShift EulerPaths |
111 | 20 | adantl 482 |
. . . . 5
Circuits |
112 | 111, 30, 109 | 3brtr4d 4685 |
. . . 4
cyclShift Circuits |
113 | | eucrct2eupth1.s |
. . . 4
Vtx |
114 | | elfzolt3 12480 |
. . . . . . 7
..^
|
115 | 9, 114 | syl 17 |
. . . . . 6
|
116 | | elfzoelz 12470 |
. . . . . . . . . . 11
..^
|
117 | 9, 116 | syl 17 |
. . . . . . . . . 10
|
118 | 117 | peano2zd 11485 |
. . . . . . . . 9
|
119 | 5, 118 | syl5eqel 2705 |
. . . . . . . 8
|
120 | | cshwlen 13545 |
. . . . . . . . 9
Word
cyclShift |
121 | 120 | eqcomd 2628 |
. . . . . . . 8
Word
cyclShift
|
122 | 24, 119, 121 | syl2anc 693 |
. . . . . . 7
cyclShift
|
123 | 18, 122 | eqtrd 2656 |
. . . . . 6
cyclShift
|
124 | 115, 123 | breqtrd 4679 |
. . . . 5
cyclShift
|
125 | 124 | adantl 482 |
. . . 4
cyclShift |
126 | 123 | adantl 482 |
. . . . 5
cyclShift |
127 | 126 | oveq1d 6665 |
. . . 4
cyclShift |
128 | | eucrct2eupth.e |
. . . . . 6
iEdg ..^ |
129 | 128 | adantl 482 |
. . . . 5
iEdg ..^ |
130 | 24, 18, 9 | 3jca 1242 |
. . . . . . . . 9
Word
..^ |
131 | 130 | adantl 482 |
. . . . . . . 8
Word
..^ |
132 | | cshimadifsn0 13576 |
. . . . . . . 8
Word
..^ ..^ cyclShift
..^ |
133 | 131, 132 | syl 17 |
. . . . . . 7
..^ cyclShift ..^ |
134 | 7 | imaeq1i 5463 |
. . . . . . 7
cyclShift ..^ cyclShift ..^ |
135 | 133, 134 | syl6eq 2672 |
. . . . . 6
..^ cyclShift ..^ |
136 | 135 | reseq2d 5396 |
. . . . 5
..^
cyclShift ..^ |
137 | 129, 136 | eqtrd 2656 |
. . . 4
iEdg cyclShift ..^ |
138 | | eqid 2622 |
. . . 4
cyclShift ..^ cyclShift ..^ |
139 | | eqid 2622 |
. . . 4
|
140 | 1, 2, 110, 112, 113, 125, 127, 137, 138, 139 | eucrct2eupth1 27104 |
. . 3
cyclShift ..^ EulerPaths
|
141 | | eucrct2eupth.h |
. . . 4
cyclShift ..^ |
142 | 141 | a1i 11 |
. . 3
cyclShift ..^ |
143 | | eucrct2eupth.q |
. . . . 5
..^
|
144 | | fzossfz 12488 |
. . . . . . . 8
..^ |
145 | 18 | oveq2d 6666 |
. . . . . . . 8
|
146 | 144, 145 | syl5sseq 3653 |
. . . . . . 7
..^ |
147 | 146 | resmptd 5452 |
. . . . . 6
..^ ..^ |
148 | | elfzoel2 12469 |
. . . . . . . 8
..^
|
149 | | fzoval 12471 |
. . . . . . . 8
..^
|
150 | 9, 148, 149 | 3syl 18 |
. . . . . . 7
..^ |
151 | 150 | reseq2d 5396 |
. . . . . 6
..^
|
152 | 147, 151 | eqtr3d 2658 |
. . . . 5
..^
|
153 | 143, 152 | syl5eq 2668 |
. . . 4
|
154 | 153 | adantl 482 |
. . 3
|
155 | 140, 142,
154 | 3brtr4d 4685 |
. 2
EulerPaths |
156 | 20 | adantl 482 |
. . . 4
Circuits |
157 | | peano2nn0 11333 |
. . . . . . . . . . . . 13
|
158 | 157 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
|
159 | 158 | adantr 481 |
. . . . . . . . . . 11
|
160 | | simpl2 1065 |
. . . . . . . . . . 11
|
161 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
|
162 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . 17
|
163 | 162 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
164 | 12, 161, 163 | subadd2d 10411 |
. . . . . . . . . . . . . . 15
|
165 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
|
166 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
|
167 | 164, 165,
166 | 3bitr4g 303 |
. . . . . . . . . . . . . 14
|
168 | 167 | necon3bbid 2831 |
. . . . . . . . . . . . 13
|
169 | 157 | nn0red 11352 |
. . . . . . . . . . . . . . . 16
|
170 | 169 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
171 | | nnre 11027 |
. . . . . . . . . . . . . . . 16
|
172 | 171 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
|
173 | | nn0z 11400 |
. . . . . . . . . . . . . . . . 17
|
174 | | nnz 11399 |
. . . . . . . . . . . . . . . . 17
|
175 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . 17
|
176 | 173, 174,
175 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
177 | 176 | biimp3a 1432 |
. . . . . . . . . . . . . . 15
|
178 | 170, 172,
177 | leltned 10190 |
. . . . . . . . . . . . . 14
|
179 | 178 | biimprd 238 |
. . . . . . . . . . . . 13
|
180 | 168, 179 | sylbid 230 |
. . . . . . . . . . . 12
|
181 | 180 | imp 445 |
. . . . . . . . . . 11
|
182 | 159, 160,
181 | 3jca 1242 |
. . . . . . . . . 10
|
183 | 182 | ex 450 |
. . . . . . . . 9
|
184 | 10, 183 | sylbi 207 |
. . . . . . . 8
..^
|
185 | | elfzo0 12508 |
. . . . . . . 8
..^
|
186 | 184, 185 | syl6ibr 242 |
. . . . . . 7
..^
..^ |
187 | 9, 186 | syl 17 |
. . . . . 6
..^ |
188 | 187 | impcom 446 |
. . . . 5
..^ |
189 | 5 | a1i 11 |
. . . . 5
|
190 | 18 | eqcomd 2628 |
. . . . . . 7
|
191 | 190 | oveq2d 6666 |
. . . . . 6
..^ ..^ |
192 | 191 | adantl 482 |
. . . . 5
..^ ..^ |
193 | 188, 189,
192 | 3eltr4d 2716 |
. . . 4
..^ |
194 | | eqid 2622 |
. . . 4
cyclShift cyclShift |
195 | | eqid 2622 |
. . . 4
|
196 | 3 | adantl 482 |
. . . 4
EulerPaths |
197 | 1, 2, 156, 31, 193, 194, 195, 196 | eucrctshift 27103 |
. . 3
cyclShift EulerPaths
cyclShift Circuits
|
198 | | simprl 794 |
. . . . 5
cyclShift EulerPaths
cyclShift Circuits
cyclShift EulerPaths
|
199 | | simprr 796 |
. . . . 5
cyclShift EulerPaths
cyclShift Circuits
cyclShift Circuits
|
200 | 124 | ad2antlr 763 |
. . . . 5
cyclShift EulerPaths
cyclShift Circuits
cyclShift |
201 | 123 | oveq1d 6665 |
. . . . . 6
cyclShift |
202 | 201 | ad2antlr 763 |
. . . . 5
cyclShift EulerPaths
cyclShift Circuits
cyclShift |
203 | 128 | adantl 482 |
. . . . . . 7
iEdg ..^ |
204 | 130 | adantl 482 |
. . . . . . . . . 10
Word
..^ |
205 | 204, 132 | syl 17 |
. . . . . . . . 9
..^ cyclShift
..^ |
206 | 205, 134 | syl6eq 2672 |
. . . . . . . 8
..^ cyclShift
..^ |
207 | 206 | reseq2d 5396 |
. . . . . . 7
..^ cyclShift ..^ |
208 | 203, 207 | eqtrd 2656 |
. . . . . 6
iEdg cyclShift ..^ |
209 | 208 | adantr 481 |
. . . . 5
cyclShift EulerPaths
cyclShift Circuits
iEdg cyclShift ..^ |
210 | | eqid 2622 |
. . . . 5
|
211 | 1, 2, 198, 199, 113, 200, 202, 209, 138, 210 | eucrct2eupth1 27104 |
. . . 4
cyclShift EulerPaths
cyclShift Circuits
cyclShift ..^ EulerPaths
|
212 | 141 | a1i 11 |
. . . 4
cyclShift EulerPaths
cyclShift Circuits
cyclShift ..^ |
213 | 190 | oveq1d 6665 |
. . . . . . . . . . . 12
|
214 | 213 | breq2d 4665 |
. . . . . . . . . . 11
|
215 | 214 | adantl 482 |
. . . . . . . . . 10
|
216 | 190 | oveq2d 6666 |
. . . . . . . . . . . 12
|
217 | 216 | fveq2d 6195 |
. . . . . . . . . . 11
|
218 | 217 | adantl 482 |
. . . . . . . . . 10
|
219 | 215, 218 | ifbieq2d 4111 |
. . . . . . . . 9
|
220 | 219 | mpteq2dv 4745 |
. . . . . . . 8
|
221 | 150 | eqcomd 2628 |
. . . . . . . . 9
..^ |
222 | 221 | adantl 482 |
. . . . . . . 8
..^ |
223 | 220, 222 | reseq12d 5397 |
. . . . . . 7
..^ |
224 | 18 | adantl 482 |
. . . . . . . . . 10
|
225 | 224 | oveq2d 6666 |
. . . . . . . . 9
|
226 | 144, 225 | syl5sseq 3653 |
. . . . . . . 8
..^ |
227 | 226 | resmptd 5452 |
. . . . . . 7
..^ ..^ |
228 | 223, 227 | eqtrd 2656 |
. . . . . 6
..^ |
229 | 228, 143 | syl6reqr 2675 |
. . . . 5
|
230 | 229 | adantr 481 |
. . . 4
cyclShift EulerPaths
cyclShift Circuits
|
231 | 211, 212,
230 | 3brtr4d 4685 |
. . 3
cyclShift EulerPaths
cyclShift Circuits
EulerPaths |
232 | 197, 231 | mpdan 702 |
. 2
EulerPaths |
233 | 155, 232 | pm2.61ian 831 |
1
EulerPaths |