Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12460 |
. . 3
β’ (π β β0
β (π + 1) β
β0) |
2 | | iswwlksn 28825 |
. . 3
β’ ((π + 1) β β0
β (π β ((π + 1) WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)))) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β β0
β (π β ((π + 1) WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)))) |
4 | | eqid 2737 |
. . . . 5
β’
(VtxβπΊ) =
(VtxβπΊ) |
5 | | eqid 2737 |
. . . . 5
β’
(EdgβπΊ) =
(EdgβπΊ) |
6 | 4, 5 | iswwlks 28823 |
. . . 4
β’ (π β (WWalksβπΊ) β (π β β
β§ π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
7 | | simp1 1137 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ π β β0) β π β Word (VtxβπΊ)) |
8 | | nn0p1nn 12459 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π + 1) β
β) |
9 | 8 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ π β β0) β (π + 1) β
β) |
10 | 1 | nn0red 12481 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β) |
11 | 10 | lep1d 12093 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 1) β€ ((π + 1) + 1)) |
12 | 11 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ π β β0) β (π + 1) β€ ((π + 1) + 1)) |
13 | | breq2 5114 |
. . . . . . . . . . . . . 14
β’
((β―βπ) =
((π + 1) + 1) β
((π + 1) β€
(β―βπ) β
(π + 1) β€ ((π + 1) + 1))) |
14 | 13 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ π β β0) β ((π + 1) β€ (β―βπ) β (π + 1) β€ ((π + 1) + 1))) |
15 | 12, 14 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ π β β0) β (π + 1) β€ (β―βπ)) |
16 | | pfxn0 14581 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ (π + 1) β β β§ (π + 1) β€ (β―βπ)) β (π prefix (π + 1)) β β
) |
17 | 7, 9, 15, 16 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ π β β0) β (π prefix (π + 1)) β β
) |
18 | 17 | 3exp 1120 |
. . . . . . . . . 10
β’ (π β Word (VtxβπΊ) β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π prefix (π + 1)) β β
))) |
19 | 18 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π prefix (π + 1)) β β
))) |
20 | 19 | imp 408 |
. . . . . . . 8
β’ (((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1)) β (π β β0 β (π prefix (π + 1)) β β
)) |
21 | 20 | impcom 409 |
. . . . . . 7
β’ ((π β β0
β§ ((π β β
β§ π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1))) β (π prefix (π + 1)) β β
) |
22 | | pfxcl 14572 |
. . . . . . . . . 10
β’ (π β Word (VtxβπΊ) β (π prefix (π + 1)) β Word (VtxβπΊ)) |
23 | 22 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β (π prefix (π + 1)) β Word (VtxβπΊ)) |
24 | 23 | adantr 482 |
. . . . . . . 8
β’ (((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1)) β (π prefix (π + 1)) β Word (VtxβπΊ)) |
25 | 24 | adantl 483 |
. . . . . . 7
β’ ((π β β0
β§ ((π β β
β§ π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1))) β (π prefix (π + 1)) β Word (VtxβπΊ)) |
26 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ) =
((π + 1) + 1) β
((β―βπ) β
1) = (((π + 1) + 1) β
1)) |
27 | 1 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β (π + 1) β
β) |
28 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β 1 β β) |
29 | 27, 28 | pncand 11520 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β (((π + 1) + 1)
β 1) = (π +
1)) |
30 | 26, 29 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β ((β―βπ)
β 1) = (π +
1)) |
31 | 30 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (0..^((β―βπ) β 1)) = (0..^(π + 1))) |
32 | 31 | raleqdv 3316 |
. . . . . . . . . . . . . . . . . 18
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
33 | 32 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
34 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β π β
β€) |
35 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π + 1) β β0
β (π + 1) β
β€) |
36 | 1, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β (π + 1) β
β€) |
37 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β0
β π β
β) |
38 | 37 | lep1d 12093 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β π β€ (π + 1)) |
39 | 34, 36, 38 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β (π β β€
β§ (π + 1) β
β€ β§ π β€ (π + 1))) |
40 | 39 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β (π β β€ β§ (π + 1) β β€ β§ π β€ (π + 1))) |
41 | | eluz2 12776 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π + 1) β
(β€β₯βπ) β (π β β€ β§ (π + 1) β β€ β§ π β€ (π + 1))) |
42 | 40, 41 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β (π + 1) β
(β€β₯βπ)) |
43 | | fzoss2 13607 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π + 1) β
(β€β₯βπ) β (0..^π) β (0..^(π + 1))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(0..^π) β (0..^(π + 1))) |
45 | | ssralv 4015 |
. . . . . . . . . . . . . . . . . . 19
β’
((0..^π) β
(0..^(π + 1)) β
(βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
47 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β π β Word (VtxβπΊ)) |
48 | | nn0fz0 13546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π + 1) β β0
β (π + 1) β
(0...(π +
1))) |
49 | 1, 48 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β0
β (π + 1) β
(0...(π +
1))) |
50 | 49 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β (π + 1) β (0...(π + 1))) |
51 | | fzelp1 13500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π + 1) β (0...(π + 1)) β (π + 1) β (0...((π + 1) + 1))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β (π + 1) β (0...((π + 1) + 1))) |
53 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((β―βπ) =
((π + 1) + 1) β
(0...(β―βπ)) =
(0...((π + 1) +
1))) |
54 | 53 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((β―βπ) =
((π + 1) + 1) β
((π + 1) β
(0...(β―βπ))
β (π + 1) β
(0...((π + 1) +
1)))) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β ((π + 1) β
(0...(β―βπ))
β (π + 1) β
(0...((π + 1) +
1)))) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β ((π + 1) β
(0...(β―βπ))
β (π + 1) β
(0...((π + 1) +
1)))) |
57 | 52, 56 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β (π + 1) β
(0...(β―βπ))) |
58 | 57 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β (π + 1) β (0...(β―βπ))) |
59 | | fzossfzop1 13657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β0
β (0..^π) β
(0..^(π +
1))) |
60 | 59 | sseld 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β0
β (π β (0..^π) β π β (0..^(π + 1)))) |
61 | 60 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β (π β (0..^π) β π β (0..^(π + 1)))) |
62 | 61 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β π β (0..^(π + 1))) |
63 | | pfxfv 14577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)) β§ π β (0..^(π + 1))) β ((π prefix (π + 1))βπ) = (πβπ)) |
64 | 47, 58, 62, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β ((π prefix (π + 1))βπ) = (πβπ)) |
65 | 64 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β (πβπ) = ((π prefix (π + 1))βπ)) |
66 | | fzofzp1 13676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (0..^π) β (π + 1) β (0...π)) |
67 | 66 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β (π + 1) β (0...π)) |
68 | | fzval3 13648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β€ β
(0...π) = (0..^(π + 1))) |
69 | 68 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β€ β
(0..^(π + 1)) = (0...π)) |
70 | 34, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β0
β (0..^(π + 1)) =
(0...π)) |
71 | 70 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β0
β ((π + 1) β
(0..^(π + 1)) β (π + 1) β (0...π))) |
72 | 71 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β ((π + 1) β (0..^(π + 1)) β (π + 1) β (0...π))) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β ((π + 1) β (0..^(π + 1)) β (π + 1) β (0...π))) |
74 | 67, 73 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β (π + 1) β (0..^(π + 1))) |
75 | | pfxfv 14577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)) β§ (π + 1) β (0..^(π + 1))) β ((π prefix (π + 1))β(π + 1)) = (πβ(π + 1))) |
76 | 47, 58, 74, 75 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β ((π prefix (π + 1))β(π + 1)) = (πβ(π + 1))) |
77 | 76 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β (πβ(π + 1)) = ((π prefix (π + 1))β(π + 1))) |
78 | 65, 77 | preq12d 4707 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β {(πβπ), (πβ(π + 1))} = {((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))}) |
79 | 78 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
80 | 79 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§ π β (0..^π)) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
81 | 80 | ralimdva 3165 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(βπ β
(0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^π){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
82 | 46, 81 | syld 47 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^π){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
83 | 33, 82 | sylbid 239 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^π){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
84 | 83 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β βπ β (0..^π){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ)) |
85 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β π β
β) |
86 | 85, 28 | pncand 11520 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β ((π + 1) β 1)
= π) |
87 | 86 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (0..^((π + 1)
β 1)) = (0..^π)) |
88 | 87 | ad2antll 728 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(0..^((π + 1) β 1)) =
(0..^π)) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β (0..^((π + 1) β 1)) = (0..^π)) |
90 | 89 | raleqdv 3316 |
. . . . . . . . . . . . . . 15
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β (βπ β (0..^((π + 1) β 1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ) β βπ β (0..^π){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
91 | 84, 90 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β βπ β (0..^((π + 1) β 1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ)) |
92 | | pfxlen 14578 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))) β (β―β(π prefix (π + 1))) = (π + 1)) |
93 | 57, 92 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(β―β(π prefix
(π + 1))) = (π + 1)) |
94 | 93 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
((β―β(π prefix
(π + 1))) β 1) =
((π + 1) β
1)) |
95 | 94 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(0..^((β―β(π
prefix (π + 1))) β
1)) = (0..^((π + 1) β
1))) |
96 | 95 | raleqdv 3316 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β
(βπ β
(0..^((β―β(π
prefix (π + 1))) β
1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ) β βπ β (0..^((π + 1) β 1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β (βπ β (0..^((β―β(π prefix (π + 1))) β 1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ) β βπ β (0..^((π + 1) β 1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
98 | 91, 97 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β βπ β (0..^((β―β(π prefix (π + 1))) β 1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ)) |
99 | 98 | exp31 421 |
. . . . . . . . . . . 12
β’ (π β Word (VtxβπΊ) β (((β―βπ) = ((π + 1) + 1) β§ π β β0) β
(βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^((β―β(π prefix (π + 1))) β 1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ)))) |
100 | 99 | com23 86 |
. . . . . . . . . . 11
β’ (π β Word (VtxβπΊ) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β (((β―βπ) = ((π + 1) + 1) β§ π β β0) β
βπ β
(0..^((β―β(π
prefix (π + 1))) β
1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ)))) |
101 | 100 | imp 408 |
. . . . . . . . . 10
β’ ((π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β (((β―βπ) = ((π + 1) + 1) β§ π β β0) β
βπ β
(0..^((β―β(π
prefix (π + 1))) β
1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
102 | 101 | 3adant1 1131 |
. . . . . . . . 9
β’ ((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β (((β―βπ) = ((π + 1) + 1) β§ π β β0) β
βπ β
(0..^((β―β(π
prefix (π + 1))) β
1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
103 | 102 | expdimp 454 |
. . . . . . . 8
β’ (((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1)) β (π β β0 β
βπ β
(0..^((β―β(π
prefix (π + 1))) β
1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
104 | 103 | impcom 409 |
. . . . . . 7
β’ ((π β β0
β§ ((π β β
β§ π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1))) β βπ β
(0..^((β―β(π
prefix (π + 1))) β
1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ)) |
105 | 4, 5 | iswwlks 28823 |
. . . . . . 7
β’ ((π prefix (π + 1)) β (WWalksβπΊ) β ((π prefix (π + 1)) β β
β§ (π prefix (π + 1)) β Word (VtxβπΊ) β§ βπ β
(0..^((β―β(π
prefix (π + 1))) β
1)){((π prefix (π + 1))βπ), ((π prefix (π + 1))β(π + 1))} β (EdgβπΊ))) |
106 | 21, 25, 104, 105 | syl3anbrc 1344 |
. . . . . 6
β’ ((π β β0
β§ ((π β β
β§ π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1))) β (π prefix (π + 1)) β (WWalksβπΊ)) |
107 | | peano2nn0 12460 |
. . . . . . . . . . . . . . . 16
β’ ((π + 1) β β0
β ((π + 1) + 1) β
β0) |
108 | 1, 107 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β ((π + 1) + 1) β
β0) |
109 | | elfz2nn0 13539 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) β (0...((π + 1) + 1)) β ((π + 1) β β0
β§ ((π + 1) + 1) β
β0 β§ (π + 1) β€ ((π + 1) + 1))) |
110 | 1, 108, 11, 109 | syl3anbrc 1344 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 1) β
(0...((π + 1) +
1))) |
111 | 110 | adantl 483 |
. . . . . . . . . . . . 13
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (π + 1) β
(0...((π + 1) +
1))) |
112 | 111, 55 | mpbird 257 |
. . . . . . . . . . . 12
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (π + 1) β
(0...(β―βπ))) |
113 | 112 | anim2i 618 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = ((π + 1) + 1) β§ π β β0)) β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)))) |
114 | 113 | exp32 422 |
. . . . . . . . . 10
β’ (π β Word (VtxβπΊ) β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)))))) |
115 | 114 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)))))) |
116 | 115 | imp 408 |
. . . . . . . 8
β’ (((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1)) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))))) |
117 | 116 | impcom 409 |
. . . . . . 7
β’ ((π β β0
β§ ((π β β
β§ π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1))) β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)))) |
118 | 117, 92 | syl 17 |
. . . . . 6
β’ ((π β β0
β§ ((π β β
β§ π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1))) β (β―β(π prefix (π + 1))) = (π + 1)) |
119 | | iswwlksn 28825 |
. . . . . . 7
β’ (π β β0
β ((π prefix (π + 1)) β (π WWalksN πΊ) β ((π prefix (π + 1)) β (WWalksβπΊ) β§ (β―β(π prefix (π + 1))) = (π + 1)))) |
120 | 119 | adantr 482 |
. . . . . 6
β’ ((π β β0
β§ ((π β β
β§ π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1))) β ((π prefix (π + 1)) β (π WWalksN πΊ) β ((π prefix (π + 1)) β (WWalksβπΊ) β§ (β―β(π prefix (π + 1))) = (π + 1)))) |
121 | 106, 118,
120 | mpbir2and 712 |
. . . . 5
β’ ((π β β0
β§ ((π β β
β§ π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1))) β (π prefix (π + 1)) β (π WWalksN πΊ)) |
122 | 121 | expcom 415 |
. . . 4
β’ (((π β β
β§ π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β§ (β―βπ) = ((π + 1) + 1)) β (π β β0 β (π prefix (π + 1)) β (π WWalksN πΊ))) |
123 | 6, 122 | sylanb 582 |
. . 3
β’ ((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β (π β β0 β (π prefix (π + 1)) β (π WWalksN πΊ))) |
124 | 123 | com12 32 |
. 2
β’ (π β β0
β ((π β
(WWalksβπΊ) β§
(β―βπ) = ((π + 1) + 1)) β (π prefix (π + 1)) β (π WWalksN πΊ))) |
125 | 3, 124 | sylbid 239 |
1
β’ (π β β0
β (π β ((π + 1) WWalksN πΊ) β (π prefix (π + 1)) β (π WWalksN πΊ))) |