Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . 3
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | | eqid 2736 |
. . 3
β’
(EdgβπΊ) =
(EdgβπΊ) |
3 | 1, 2 | wwlknp 28257 |
. 2
β’ (π β (π WWalksN πΊ) β (π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
4 | | pfxcl 14439 |
. . . . . . . . . . . 12
β’ (π β Word (VtxβπΊ) β (π prefix π) β Word (VtxβπΊ)) |
5 | 4 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β (π prefix π) β Word (VtxβπΊ)) |
6 | 5 | adantr 482 |
. . . . . . . . . 10
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (π prefix π) β Word (VtxβπΊ)) |
7 | | simpll 765 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β Word (VtxβπΊ)) |
8 | | simprl 769 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β β) |
9 | | eluz2 12638 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β (π β β€ β§ π β β€ β§ π β€ π)) |
10 | | zre 12373 |
. . . . . . . . . . . . . . . . 17
β’ (π β β€ β π β
β) |
11 | | zre 12373 |
. . . . . . . . . . . . . . . . 17
β’ (π β β€ β π β
β) |
12 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π β€ π β π β€ π) |
13 | 10, 11, 12 | 3anim123i 1151 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β€ β§ π β€ π) β (π β β β§ π β β β§ π β€ π)) |
14 | 9, 13 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (π β β β§ π β β β§ π β€ π)) |
15 | | letrp1 11869 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β β§ π β€ π) β π β€ (π + 1)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β π β€ (π + 1)) |
17 | 16 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β
(β€β₯βπ)) β π β€ (π + 1)) |
18 | 17 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β€ (π + 1)) |
19 | | breq2 5085 |
. . . . . . . . . . . . 13
β’
((β―βπ) =
(π + 1) β (π β€ (β―βπ) β π β€ (π + 1))) |
20 | 19 | ad2antlr 725 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (π β€ (β―βπ) β π β€ (π + 1))) |
21 | 18, 20 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β€ (β―βπ)) |
22 | | pfxn0 14448 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ π β β β§ π β€ (β―βπ)) β (π prefix π) β β
) |
23 | 7, 8, 21, 22 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (π prefix π) β β
) |
24 | 6, 23 | jca 513 |
. . . . . . . . 9
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β ((π prefix π) β Word (VtxβπΊ) β§ (π prefix π) β β
)) |
25 | 24 | 3adantl3 1168 |
. . . . . . . 8
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β ((π prefix π) β Word (VtxβπΊ) β§ (π prefix π) β β
)) |
26 | 25 | adantr 482 |
. . . . . . 7
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β ((π prefix π) β Word (VtxβπΊ) β§ (π prefix π) β β
)) |
27 | | nnz 12392 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β€) |
28 | | 1nn0 12299 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β0 |
29 | | eluzmn 12639 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ 1 β
β0) β π β (β€β₯β(π β 1))) |
30 | 27, 28, 29 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
(β€β₯β(π β 1))) |
31 | | uzss 12655 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β(π β 1)) β
(β€β₯βπ) β
(β€β₯β(π β 1))) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(β€β₯βπ) β
(β€β₯β(π β 1))) |
33 | 32 | sselda 3926 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β
(β€β₯βπ)) β π β (β€β₯β(π β 1))) |
34 | | fzoss2 13465 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β(π β 1)) β (0..^(π β 1)) β (0..^π)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β
(β€β₯βπ)) β (0..^(π β 1)) β (0..^π)) |
36 | 35 | 3ad2ant3 1135 |
. . . . . . . . . . . . 13
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ (π β β β§ π β (β€β₯βπ))) β (0..^(π β 1)) β (0..^π)) |
37 | | ssralv 3992 |
. . . . . . . . . . . . 13
β’
((0..^(π β 1))
β (0..^π) β
(βπ β
(0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ (π β β β§ π β (β€β₯βπ))) β (βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
39 | 38 | 3exp 1119 |
. . . . . . . . . . 11
β’ (π β Word (VtxβπΊ) β ((β―βπ) = (π + 1) β ((π β β β§ π β (β€β₯βπ)) β (βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))))) |
40 | 39 | com34 91 |
. . . . . . . . . 10
β’ (π β Word (VtxβπΊ) β ((β―βπ) = (π + 1) β (βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β ((π β β β§ π β (β€β₯βπ)) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))))) |
41 | 40 | 3imp1 1347 |
. . . . . . . . 9
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) |
42 | 41 | adantr 482 |
. . . . . . . 8
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) |
43 | | nnnn0 12290 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β0) |
44 | | elnn0uz 12673 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β π β
(β€β₯β0)) |
45 | 43, 44 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
(β€β₯β0)) |
46 | | eluzfz 13301 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β
(β€β₯β0) β§ π β (β€β₯βπ)) β π β (0...π)) |
47 | 45, 46 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β
(β€β₯βπ)) β π β (0...π)) |
48 | | fzelp1 13358 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β π β (0...(π + 1))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β
(β€β₯βπ)) β π β (0...(π + 1))) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β (0...(π + 1))) |
51 | | oveq2 7315 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ) =
(π + 1) β
(0...(β―βπ)) =
(0...(π +
1))) |
52 | 51 | eleq2d 2822 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
(π + 1) β (π β
(0...(β―βπ))
β π β (0...(π + 1)))) |
53 | 52 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (π β (0...(β―βπ)) β π β (0...(π + 1)))) |
54 | 50, 53 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β (0...(β―βπ))) |
55 | | pfxlen 14445 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ π β (0...(β―βπ))) β (β―β(π prefix π)) = π) |
56 | 7, 54, 55 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (β―β(π prefix π)) = π) |
57 | 56 | oveq1d 7322 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β
((β―β(π prefix
π)) β 1) = (π β 1)) |
58 | 57 | oveq2d 7323 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β
(0..^((β―β(π
prefix π)) β 1)) =
(0..^(π β
1))) |
59 | 58 | raleqdv 3367 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (βπ β
(0..^((β―β(π
prefix π)) β
1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ))) |
60 | 7 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β§ π β (0..^(π β 1))) β π β Word (VtxβπΊ)) |
61 | 54 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β§ π β (0..^(π β 1))) β π β (0...(β―βπ))) |
62 | 30 | ad2antrl 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β (β€β₯β(π β 1))) |
63 | | fzoss2 13465 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β(π β 1)) β (0..^(π β 1)) β (0..^π)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (0..^(π β 1)) β (0..^π)) |
65 | 64 | sselda 3926 |
. . . . . . . . . . . . . . 15
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β§ π β (0..^(π β 1))) β π β (0..^π)) |
66 | | pfxfv 14444 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ π β (0...(β―βπ)) β§ π β (0..^π)) β ((π prefix π)βπ) = (πβπ)) |
67 | 60, 61, 65, 66 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β§ π β (0..^(π β 1))) β ((π prefix π)βπ) = (πβπ)) |
68 | 27 | ad2antrl 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β β€) |
69 | | elfzom1elp1fzo 13504 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β (0..^(π β 1))) β (π + 1) β (0..^π)) |
70 | 68, 69 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β§ π β (0..^(π β 1))) β (π + 1) β (0..^π)) |
71 | | pfxfv 14444 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ π β (0...(β―βπ)) β§ (π + 1) β (0..^π)) β ((π prefix π)β(π + 1)) = (πβ(π + 1))) |
72 | 60, 61, 70, 71 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β§ π β (0..^(π β 1))) β ((π prefix π)β(π + 1)) = (πβ(π + 1))) |
73 | 67, 72 | preq12d 4681 |
. . . . . . . . . . . . 13
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β§ π β (0..^(π β 1))) β {((π prefix π)βπ), ((π prefix π)β(π + 1))} = {(πβπ), (πβ(π + 1))}) |
74 | 73 | eleq1d 2821 |
. . . . . . . . . . . 12
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β§ π β (0..^(π β 1))) β ({((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β {(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
75 | 74 | ralbidva 3169 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (βπ β (0..^(π β 1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
76 | 59, 75 | bitrd 279 |
. . . . . . . . . 10
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (βπ β
(0..^((β―β(π
prefix π)) β
1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
77 | 76 | 3adantl3 1168 |
. . . . . . . . 9
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β (βπ β
(0..^((β―β(π
prefix π)) β
1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
78 | 77 | adantr 482 |
. . . . . . . 8
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β (βπ β
(0..^((β―β(π
prefix π)) β
1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
79 | 42, 78 | mpbird 257 |
. . . . . . 7
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β βπ β (0..^((β―β(π prefix π)) β 1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ)) |
80 | | elfz1uz 13376 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β
(β€β₯βπ)) β π β (1...π)) |
81 | | fzelp1 13358 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β π β (1...(π + 1))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β
(β€β₯βπ)) β π β (1...(π + 1))) |
83 | 82 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β (1...(π + 1))) |
84 | | oveq2 7315 |
. . . . . . . . . . . . . 14
β’
((β―βπ) =
(π + 1) β
(1...(β―βπ)) =
(1...(π +
1))) |
85 | 84 | eleq2d 2822 |
. . . . . . . . . . . . 13
β’
((β―βπ) =
(π + 1) β (π β
(1...(β―βπ))
β π β (1...(π + 1)))) |
86 | 85 | ad2antlr 725 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (π β (1...(β―βπ)) β π β (1...(π + 1)))) |
87 | 83, 86 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β (1...(β―βπ))) |
88 | | pfxfvlsw 14457 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ π β (1...(β―βπ))) β (lastSβ(π prefix π)) = (πβ(π β 1))) |
89 | | pfxfv0 14454 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ π β (1...(β―βπ))) β ((π prefix π)β0) = (πβ0)) |
90 | 88, 89 | preq12d 4681 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ π β (1...(β―βπ))) β {(lastSβ(π prefix π)), ((π prefix π)β0)} = {(πβ(π β 1)), (πβ0)}) |
91 | 7, 87, 90 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β {(lastSβ(π prefix π)), ((π prefix π)β0)} = {(πβ(π β 1)), (πβ0)}) |
92 | 91 | 3adantl3 1168 |
. . . . . . . . 9
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β {(lastSβ(π prefix π)), ((π prefix π)β0)} = {(πβ(π β 1)), (πβ0)}) |
93 | 92 | adantr 482 |
. . . . . . . 8
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β {(lastSβ(π prefix π)), ((π prefix π)β0)} = {(πβ(π β 1)), (πβ0)}) |
94 | | fz1fzo0m1 13485 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β (π β 1) β (0..^π)) |
95 | 80, 94 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β
(β€β₯βπ)) β (π β 1) β (0..^π)) |
96 | 95 | 3ad2ant3 1135 |
. . . . . . . . . . . . . 14
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ (π β β β§ π β (β€β₯βπ))) β (π β 1) β (0..^π)) |
97 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π = (π β 1)) β π = (π β 1)) |
98 | 97 | fveq2d 6808 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π = (π β 1)) β (πβπ) = (πβ(π β 1))) |
99 | | oveq1 7314 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π β 1) β (π + 1) = ((π β 1) + 1)) |
100 | | nncn 12031 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β π β
β) |
101 | | npcan1 11450 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β ((π β 1) + 1) = π) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β ((π β 1) + 1) = π) |
103 | 99, 102 | sylan9eqr 2798 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π = (π β 1)) β (π + 1) = π) |
104 | 103 | fveq2d 6808 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π = (π β 1)) β (πβ(π + 1)) = (πβπ)) |
105 | 98, 104 | preq12d 4681 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π = (π β 1)) β {(πβπ), (πβ(π + 1))} = {(πβ(π β 1)), (πβπ)}) |
106 | 105 | eleq1d 2821 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π = (π β 1)) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ))) |
107 | 106 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π = (π β 1) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ)))) |
108 | 107 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β
(β€β₯βπ)) β (π = (π β 1) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ)))) |
109 | 108 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ (π β β β§ π β (β€β₯βπ))) β (π = (π β 1) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ)))) |
110 | 109 | imp 408 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ (π β β β§ π β (β€β₯βπ))) β§ π = (π β 1)) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ))) |
111 | 96, 110 | rspcdv 3558 |
. . . . . . . . . . . . 13
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ (π β β β§ π β (β€β₯βπ))) β (βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ))) |
112 | 111 | 3exp 1119 |
. . . . . . . . . . . 12
β’ (π β Word (VtxβπΊ) β ((β―βπ) = (π + 1) β ((π β β β§ π β (β€β₯βπ)) β (βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ))))) |
113 | 112 | com34 91 |
. . . . . . . . . . 11
β’ (π β Word (VtxβπΊ) β ((β―βπ) = (π + 1) β (βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β ((π β β β§ π β (β€β₯βπ)) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ))))) |
114 | 113 | 3imp1 1347 |
. . . . . . . . . 10
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ)) |
115 | 114 | adantr 482 |
. . . . . . . . 9
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β {(πβ(π β 1)), (πβπ)} β (EdgβπΊ)) |
116 | | preq2 4674 |
. . . . . . . . . . 11
β’ ((πβπ) = (πβ0) β {(πβ(π β 1)), (πβπ)} = {(πβ(π β 1)), (πβ0)}) |
117 | 116 | eleq1d 2821 |
. . . . . . . . . 10
β’ ((πβπ) = (πβ0) β ({(πβ(π β 1)), (πβπ)} β (EdgβπΊ) β {(πβ(π β 1)), (πβ0)} β (EdgβπΊ))) |
118 | 117 | adantl 483 |
. . . . . . . . 9
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β ({(πβ(π β 1)), (πβπ)} β (EdgβπΊ) β {(πβ(π β 1)), (πβ0)} β (EdgβπΊ))) |
119 | 115, 118 | mpbid 231 |
. . . . . . . 8
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β {(πβ(π β 1)), (πβ0)} β (EdgβπΊ)) |
120 | 93, 119 | eqeltrd 2837 |
. . . . . . 7
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β {(lastSβ(π prefix π)), ((π prefix π)β0)} β (EdgβπΊ)) |
121 | 26, 79, 120 | 3jca 1128 |
. . . . . 6
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (π β β β§ π β (β€β₯βπ))) β§ (πβπ) = (πβ0)) β (((π prefix π) β Word (VtxβπΊ) β§ (π prefix π) β β
) β§ βπ β
(0..^((β―β(π
prefix π)) β
1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix π)), ((π prefix π)β0)} β (EdgβπΊ))) |
122 | 121 | exp31 421 |
. . . . 5
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β ((π β β β§ π β (β€β₯βπ)) β ((πβπ) = (πβ0) β (((π prefix π) β Word (VtxβπΊ) β§ (π prefix π) β β
) β§ βπ β
(0..^((β―β(π
prefix π)) β
1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix π)), ((π prefix π)β0)} β (EdgβπΊ))))) |
123 | 122 | 3imp21 1114 |
. . . 4
β’ (((π β β β§ π β
(β€β₯βπ)) β§ (π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (πβπ) = (πβ0)) β (((π prefix π) β Word (VtxβπΊ) β§ (π prefix π) β β
) β§ βπ β
(0..^((β―β(π
prefix π)) β
1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix π)), ((π prefix π)β0)} β (EdgβπΊ))) |
124 | 1, 2 | isclwwlk 28397 |
. . . 4
β’ ((π prefix π) β (ClWWalksβπΊ) β (((π prefix π) β Word (VtxβπΊ) β§ (π prefix π) β β
) β§ βπ β
(0..^((β―β(π
prefix π)) β
1)){((π prefix π)βπ), ((π prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix π)), ((π prefix π)β0)} β (EdgβπΊ))) |
125 | 123, 124 | sylibr 233 |
. . 3
β’ (((π β β β§ π β
(β€β₯βπ)) β§ (π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (πβπ) = (πβ0)) β (π prefix π) β (ClWWalksβπΊ)) |
126 | 47 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β (0...π)) |
127 | 126, 48 | syl 17 |
. . . . . . . . . 10
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β (0...(π + 1))) |
128 | 127, 53 | mpbird 257 |
. . . . . . . . 9
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β π β (0...(β―βπ))) |
129 | 7, 128 | jca 513 |
. . . . . . . 8
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β§ (π β β β§ π β (β€β₯βπ))) β (π β Word (VtxβπΊ) β§ π β (0...(β―βπ)))) |
130 | 129 | ex 414 |
. . . . . . 7
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1)) β ((π β β β§ π β (β€β₯βπ)) β (π β Word (VtxβπΊ) β§ π β (0...(β―βπ))))) |
131 | 130 | 3adant3 1132 |
. . . . . 6
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β ((π β β β§ π β (β€β₯βπ)) β (π β Word (VtxβπΊ) β§ π β (0...(β―βπ))))) |
132 | 131 | impcom 409 |
. . . . 5
β’ (((π β β β§ π β
(β€β₯βπ)) β§ (π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) β (π β Word (VtxβπΊ) β§ π β (0...(β―βπ)))) |
133 | 132 | 3adant3 1132 |
. . . 4
β’ (((π β β β§ π β
(β€β₯βπ)) β§ (π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (πβπ) = (πβ0)) β (π β Word (VtxβπΊ) β§ π β (0...(β―βπ)))) |
134 | 133, 55 | syl 17 |
. . 3
β’ (((π β β β§ π β
(β€β₯βπ)) β§ (π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (πβπ) = (πβ0)) β (β―β(π prefix π)) = π) |
135 | | isclwwlkn 28440 |
. . 3
β’ ((π prefix π) β (π ClWWalksN πΊ) β ((π prefix π) β (ClWWalksβπΊ) β§ (β―β(π prefix π)) = π)) |
136 | 125, 134,
135 | sylanbrc 584 |
. 2
β’ (((π β β β§ π β
(β€β₯βπ)) β§ (π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (πβπ) = (πβ0)) β (π prefix π) β (π ClWWalksN πΊ)) |
137 | 3, 136 | syl3an2 1164 |
1
β’ (((π β β β§ π β
(β€β₯βπ)) β§ π β (π WWalksN πΊ) β§ (πβπ) = (πβ0)) β (π prefix π) β (π ClWWalksN πΊ)) |