Step | Hyp | Ref
| Expression |
1 | | clwlkwlk 28765 |
. . . . 5
β’ (π β (ClWalksβπΊ) β π β (WalksβπΊ)) |
2 | | wlkcpr 28619 |
. . . . 5
β’ (π β (WalksβπΊ) β (1st
βπ)(WalksβπΊ)(2nd βπ)) |
3 | 1, 2 | sylib 217 |
. . . 4
β’ (π β (ClWalksβπΊ) β (1st
βπ)(WalksβπΊ)(2nd βπ)) |
4 | | eqid 2737 |
. . . . 5
β’
(VtxβπΊ) =
(VtxβπΊ) |
5 | 4 | wlkpwrd 28607 |
. . . 4
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (2nd βπ) β Word (VtxβπΊ)) |
6 | 3, 5 | syl 17 |
. . 3
β’ (π β (ClWalksβπΊ) β (2nd
βπ) β Word
(VtxβπΊ)) |
7 | 6 | 3ad2ant2 1135 |
. 2
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β (2nd βπ) β Word (VtxβπΊ)) |
8 | | eluzge2nn0 12819 |
. . . . . . 7
β’ (π β
(β€β₯β2) β π β
β0) |
9 | 8 | 3ad2ant3 1136 |
. . . . . 6
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β π β
β0) |
10 | | eleq1 2826 |
. . . . . . 7
β’
((β―β(1st βπ)) = π β ((β―β(1st
βπ)) β
β0 β π β
β0)) |
11 | 10 | 3ad2ant1 1134 |
. . . . . 6
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β ((β―β(1st βπ)) β β0 β π β
β0)) |
12 | 9, 11 | mpbird 257 |
. . . . 5
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β (β―β(1st βπ)) β
β0) |
13 | | nn0fz0 13546 |
. . . . 5
β’
((β―β(1st βπ)) β β0 β
(β―β(1st βπ)) β (0...(β―β(1st
βπ)))) |
14 | 12, 13 | sylib 217 |
. . . 4
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β (β―β(1st βπ)) β (0...(β―β(1st
βπ)))) |
15 | | fzelp1 13500 |
. . . 4
β’
((β―β(1st βπ)) β (0...(β―β(1st
βπ))) β
(β―β(1st βπ)) β
(0...((β―β(1st βπ)) + 1))) |
16 | 14, 15 | syl 17 |
. . 3
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β (β―β(1st βπ)) β
(0...((β―β(1st βπ)) + 1))) |
17 | | wlklenvp1 28608 |
. . . . . . . 8
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (β―β(2nd
βπ)) =
((β―β(1st βπ)) + 1)) |
18 | 17 | eqcomd 2743 |
. . . . . . 7
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β ((β―β(1st
βπ)) + 1) =
(β―β(2nd βπ))) |
19 | 3, 18 | syl 17 |
. . . . . 6
β’ (π β (ClWalksβπΊ) β
((β―β(1st βπ)) + 1) = (β―β(2nd
βπ))) |
20 | 19 | oveq2d 7378 |
. . . . 5
β’ (π β (ClWalksβπΊ) β
(0...((β―β(1st βπ)) + 1)) =
(0...(β―β(2nd βπ)))) |
21 | 20 | eleq2d 2824 |
. . . 4
β’ (π β (ClWalksβπΊ) β
((β―β(1st βπ)) β
(0...((β―β(1st βπ)) + 1)) β
(β―β(1st βπ)) β (0...(β―β(2nd
βπ))))) |
22 | 21 | 3ad2ant2 1135 |
. . 3
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β ((β―β(1st βπ)) β
(0...((β―β(1st βπ)) + 1)) β
(β―β(1st βπ)) β (0...(β―β(2nd
βπ))))) |
23 | 16, 22 | mpbid 231 |
. 2
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β (β―β(1st βπ)) β (0...(β―β(2nd
βπ)))) |
24 | | 2nn 12233 |
. . . . . . 7
β’ 2 β
β |
25 | 24 | a1i 11 |
. . . . . 6
β’ (π β
(β€β₯β2) β 2 β β) |
26 | | eluz2nn 12816 |
. . . . . 6
β’ (π β
(β€β₯β2) β π β β) |
27 | | eluzle 12783 |
. . . . . 6
β’ (π β
(β€β₯β2) β 2 β€ π) |
28 | | elfz1b 13517 |
. . . . . 6
β’ (2 β
(1...π) β (2 β
β β§ π β
β β§ 2 β€ π)) |
29 | 25, 26, 27, 28 | syl3anbrc 1344 |
. . . . 5
β’ (π β
(β€β₯β2) β 2 β (1...π)) |
30 | | ubmelfzo 13644 |
. . . . 5
β’ (2 β
(1...π) β (π β 2) β (0..^π)) |
31 | 29, 30 | syl 17 |
. . . 4
β’ (π β
(β€β₯β2) β (π β 2) β (0..^π)) |
32 | 31 | 3ad2ant3 1136 |
. . 3
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β (π β 2) β
(0..^π)) |
33 | | oveq2 7370 |
. . . . 5
β’
((β―β(1st βπ)) = π β (0..^(β―β(1st
βπ))) = (0..^π)) |
34 | 33 | eleq2d 2824 |
. . . 4
β’
((β―β(1st βπ)) = π β ((π β 2) β
(0..^(β―β(1st βπ))) β (π β 2) β (0..^π))) |
35 | 34 | 3ad2ant1 1134 |
. . 3
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β ((π β 2)
β (0..^(β―β(1st βπ))) β (π β 2) β (0..^π))) |
36 | 32, 35 | mpbird 257 |
. 2
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β (π β 2) β
(0..^(β―β(1st βπ)))) |
37 | | pfxfv 14577 |
. 2
β’
(((2nd βπ) β Word (VtxβπΊ) β§ (β―β(1st
βπ)) β
(0...(β―β(2nd βπ))) β§ (π β 2) β
(0..^(β―β(1st βπ)))) β (((2nd βπ) prefix
(β―β(1st βπ)))β(π β 2)) = ((2nd βπ)β(π β 2))) |
38 | 7, 23, 36, 37 | syl3anc 1372 |
1
β’
(((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2))
β (((2nd βπ) prefix (β―β(1st
βπ)))β(π β 2)) = ((2nd
βπ)β(π β 2))) |