Step | Hyp | Ref
| Expression |
1 | | ccatws1n0 14527 |
. . . . . 6
β’ (π β Word (VtxβπΊ) β (π ++ β¨β(πβ0)ββ©) β
β
) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β (π ++ β¨β(πβ0)ββ©) β
β
) |
3 | 2 | 3ad2ant2 1135 |
. . . 4
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (π ++ β¨β(πβ0)ββ©) β
β
) |
4 | | simprl 770 |
. . . . . 6
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β π β Word (VtxβπΊ)) |
5 | | fstwrdne0 14451 |
. . . . . . 7
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (πβ0) β (VtxβπΊ)) |
6 | 5 | s1cld 14498 |
. . . . . 6
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β β¨β(πβ0)ββ© β Word
(VtxβπΊ)) |
7 | | ccatcl 14469 |
. . . . . 6
β’ ((π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β
Word (VtxβπΊ)) β
(π ++ β¨β(πβ0)ββ©) β
Word (VtxβπΊ)) |
8 | 4, 6, 7 | syl2anc 585 |
. . . . 5
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (π ++ β¨β(πβ0)ββ©) β Word
(VtxβπΊ)) |
9 | 8 | 3adant3 1133 |
. . . 4
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (π ++ β¨β(πβ0)ββ©) β Word
(VtxβπΊ)) |
10 | 4 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β π β Word (VtxβπΊ)) |
11 | 6 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β β¨β(πβ0)ββ© β
Word (VtxβπΊ)) |
12 | | elfzonn0 13624 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^(π β 1)) β π β β0) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β (0..^(π β 1))) β π β β0) |
14 | | nnz 12527 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β€) |
15 | 14 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β (0..^(π β 1))) β π β β€) |
16 | | elfzo0 13620 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^(π β 1)) β (π β β0 β§ (π β 1) β β β§
π < (π β 1))) |
17 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β0
β π β
β) |
18 | 17 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β0
β§ π β β)
β π β
β) |
19 | | nnre 12167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β π β
β) |
20 | | peano2rem 11475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β (π β 1) β
β) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β (π β 1) β
β) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β0
β§ π β β)
β (π β 1) β
β) |
23 | 19 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β0
β§ π β β)
β π β
β) |
24 | 18, 22, 23 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β0
β§ π β β)
β (π β β
β§ (π β 1) β
β β§ π β
β)) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β0
β§ π β β)
β§ π < (π β 1)) β (π β β β§ (π β 1) β β β§
π β
β)) |
26 | 19 | ltm1d 12094 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β (π β 1) < π) |
27 | 26 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β0
β§ π β β)
β (π β 1) <
π) |
28 | 27 | anim1ci 617 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β0
β§ π β β)
β§ π < (π β 1)) β (π < (π β 1) β§ (π β 1) < π)) |
29 | | lttr 11238 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ (π β 1) β β β§
π β β) β
((π < (π β 1) β§ (π β 1) < π) β π < π)) |
30 | 25, 28, 29 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β0
β§ π β β)
β§ π < (π β 1)) β π < π) |
31 | 30 | ex 414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β0
β§ π β β)
β (π < (π β 1) β π < π)) |
32 | 31 | impancom 453 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β0
β§ π < (π β 1)) β (π β β β π < π)) |
33 | 32 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ (π β 1) β
β β§ π < (π β 1)) β (π β β β π < π)) |
34 | 16, 33 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^(π β 1)) β (π β β β π < π)) |
35 | 34 | impcom 409 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β (0..^(π β 1))) β π < π) |
36 | | elfzo0z 13621 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β (π β β0 β§ π β β€ β§ π < π)) |
37 | 13, 15, 35, 36 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β (0..^(π β 1))) β π β (0..^π)) |
38 | 37 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β π β (0..^π)) |
39 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ) =
π β
(0..^(β―βπ)) =
(0..^π)) |
40 | 39 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
π β (π β
(0..^(β―βπ))
β π β (0..^π))) |
41 | 40 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (π β (0..^(β―βπ)) β π β (0..^π))) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β (π β (0..^(β―βπ)) β π β (0..^π))) |
43 | 38, 42 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β π β (0..^(β―βπ))) |
44 | | ccatval1 14472 |
. . . . . . . . . . . . . 14
β’ ((π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β
Word (VtxβπΊ) β§
π β
(0..^(β―βπ)))
β ((π ++
β¨β(πβ0)ββ©)βπ) = (πβπ)) |
45 | 10, 11, 43, 44 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β ((π ++ β¨β(πβ0)ββ©)βπ) = (πβπ)) |
46 | | elfzom1p1elfzo 13659 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β (0..^(π β 1))) β (π + 1) β (0..^π)) |
47 | 46 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β (π + 1) β (0..^π)) |
48 | 39 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (0..^(β―βπ)) = (0..^π)) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β
(0..^(β―βπ)) =
(0..^π)) |
50 | 47, 49 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β (π + 1) β (0..^(β―βπ))) |
51 | | ccatval1 14472 |
. . . . . . . . . . . . . 14
β’ ((π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β
Word (VtxβπΊ) β§
(π + 1) β
(0..^(β―βπ)))
β ((π ++
β¨β(πβ0)ββ©)β(π + 1)) = (πβ(π + 1))) |
52 | 10, 11, 50, 51 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β ((π ++ β¨β(πβ0)ββ©)β(π + 1)) = (πβ(π + 1))) |
53 | 45, 52 | preq12d 4707 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β {((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} = {(πβπ), (πβ(π + 1))}) |
54 | 53 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β§ π β (0..^(π β 1))) β ({((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β {(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
55 | 54 | ralbidva 3173 |
. . . . . . . . . 10
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (βπ β (0..^(π β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
56 | 55 | biimprcd 250 |
. . . . . . . . 9
β’
(βπ β
(0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β βπ β (0..^(π β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ))) |
57 | 56 | adantr 482 |
. . . . . . . 8
β’
((βπ β
(0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β βπ β (0..^(π β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ))) |
58 | 57 | expdcom 416 |
. . . . . . 7
β’ (π β β β ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β ((βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β βπ β (0..^(π β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)))) |
59 | 58 | 3imp 1112 |
. . . . . 6
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β βπ β (0..^(π β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)) |
60 | | fzo0end 13671 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π β 1) β (0..^π)) |
61 | 39 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ) =
π β ((π β 1) β
(0..^(β―βπ))
β (π β 1) β
(0..^π))) |
62 | 61 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β ((π β 1) β (0..^(β―βπ)) β (π β 1) β (0..^π))) |
63 | 60, 62 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β (π β 1) β (0..^(β―βπ)))) |
64 | 63 | imp 408 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (π β 1) β (0..^(β―βπ))) |
65 | | ccatval1 14472 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β
Word (VtxβπΊ) β§
(π β 1) β
(0..^(β―βπ)))
β ((π ++
β¨β(πβ0)ββ©)β(π β 1)) = (πβ(π β 1))) |
66 | 4, 6, 64, 65 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β ((π ++ β¨β(πβ0)ββ©)β(π β 1)) = (πβ(π β 1))) |
67 | | lsw 14459 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word (VtxβπΊ) β (lastSβπ) = (πβ((β―βπ) β 1))) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β (lastSβπ) = (πβ((β―βπ) β 1))) |
69 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
π β (πβ((β―βπ) β 1)) = (πβ(π β 1))) |
70 | 69 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β (πβ((β―βπ) β 1)) = (πβ(π β 1))) |
71 | 68, 70 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β (πβ(π β 1)) = (lastSβπ)) |
72 | 71 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (πβ(π β 1)) = (lastSβπ)) |
73 | 66, 72 | eqtr2d 2778 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (lastSβπ) = ((π ++ β¨β(πβ0)ββ©)β(π β 1))) |
74 | | nncn 12168 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β) |
75 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β 1 β
β) |
76 | 74, 75 | npcand 11523 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π β 1) + 1) = π) |
77 | 76 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1)) = ((π ++ β¨β(πβ0)ββ©)βπ)) |
78 | 77 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1)) = ((π ++ β¨β(πβ0)ββ©)βπ)) |
79 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’
((β―βπ) =
π β ((π ++ β¨β(πβ0)ββ©)β(β―βπ)) = ((π ++ β¨β(πβ0)ββ©)βπ)) |
80 | 79 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β ((π ++ β¨β(πβ0)ββ©)β(β―βπ)) = ((π ++ β¨β(πβ0)ββ©)βπ)) |
81 | | ccatws1ls 14528 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ (πβ0) β (VtxβπΊ)) β ((π ++ β¨β(πβ0)ββ©)β(β―βπ)) = (πβ0)) |
82 | 4, 5, 81 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β ((π ++ β¨β(πβ0)ββ©)β(β―βπ)) = (πβ0)) |
83 | 78, 80, 82 | 3eqtr2rd 2784 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (πβ0) = ((π ++ β¨β(πβ0)ββ©)β((π β 1) +
1))) |
84 | 73, 83 | preq12d 4707 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β {(lastSβπ), (πβ0)} = {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) +
1))}) |
85 | 84 | eleq1d 2823 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β ({(lastSβπ), (πβ0)} β (EdgβπΊ) β {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1))} β
(EdgβπΊ))) |
86 | 85 | biimpcd 249 |
. . . . . . . . . 10
β’
({(lastSβπ),
(πβ0)} β
(EdgβπΊ) β
((π β β β§
(π β Word
(VtxβπΊ) β§
(β―βπ) = π)) β {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1))} β
(EdgβπΊ))) |
87 | 86 | adantl 483 |
. . . . . . . . 9
β’
((βπ β
(0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1))} β
(EdgβπΊ))) |
88 | 87 | expdcom 416 |
. . . . . . . 8
β’ (π β β β ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β ((βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1))} β
(EdgβπΊ)))) |
89 | 88 | 3imp 1112 |
. . . . . . 7
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1))} β
(EdgβπΊ)) |
90 | | ovex 7395 |
. . . . . . . 8
β’ (π β 1) β
V |
91 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = (π β 1) β ((π ++ β¨β(πβ0)ββ©)βπ) = ((π ++ β¨β(πβ0)ββ©)β(π β 1))) |
92 | | fvoveq1 7385 |
. . . . . . . . . 10
β’ (π = (π β 1) β ((π ++ β¨β(πβ0)ββ©)β(π + 1)) = ((π ++ β¨β(πβ0)ββ©)β((π β 1) +
1))) |
93 | 91, 92 | preq12d 4707 |
. . . . . . . . 9
β’ (π = (π β 1) β {((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} = {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) +
1))}) |
94 | 93 | eleq1d 2823 |
. . . . . . . 8
β’ (π = (π β 1) β ({((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1))} β
(EdgβπΊ))) |
95 | 90, 94 | ralsn 4647 |
. . . . . . 7
β’
(βπ β
{(π β 1)} {((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β {((π ++ β¨β(πβ0)ββ©)β(π β 1)), ((π ++ β¨β(πβ0)ββ©)β((π β 1) + 1))} β
(EdgβπΊ)) |
96 | 89, 95 | sylibr 233 |
. . . . . 6
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β βπ β {(π β 1)} {((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)) |
97 | 74, 75, 75 | addsubd 11540 |
. . . . . . . . . . 11
β’ (π β β β ((π + 1) β 1) = ((π β 1) +
1)) |
98 | 97 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β β β
(0..^((π + 1) β 1)) =
(0..^((π β 1) +
1))) |
99 | | nnm1nn0 12461 |
. . . . . . . . . . . 12
β’ (π β β β (π β 1) β
β0) |
100 | | elnn0uz 12815 |
. . . . . . . . . . . 12
β’ ((π β 1) β
β0 β (π β 1) β
(β€β₯β0)) |
101 | 99, 100 | sylib 217 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
(β€β₯β0)) |
102 | | fzosplitsn 13687 |
. . . . . . . . . . 11
β’ ((π β 1) β
(β€β₯β0) β (0..^((π β 1) + 1)) = ((0..^(π β 1)) βͺ {(π β 1)})) |
103 | 101, 102 | syl 17 |
. . . . . . . . . 10
β’ (π β β β
(0..^((π β 1) + 1)) =
((0..^(π β 1)) βͺ
{(π β
1)})) |
104 | 98, 103 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β β β
(0..^((π + 1) β 1)) =
((0..^(π β 1)) βͺ
{(π β
1)})) |
105 | 104 | raleqdv 3316 |
. . . . . . . 8
β’ (π β β β
(βπ β
(0..^((π + 1) β
1)){((π ++
β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β βπ β ((0..^(π β 1)) βͺ {(π β 1)}){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ))) |
106 | | ralunb 4156 |
. . . . . . . 8
β’
(βπ β
((0..^(π β 1)) βͺ
{(π β 1)}){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β (βπ β (0..^(π β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β§ βπ β {(π β 1)} {((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ))) |
107 | 105, 106 | bitrdi 287 |
. . . . . . 7
β’ (π β β β
(βπ β
(0..^((π + 1) β
1)){((π ++
β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β (βπ β (0..^(π β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β§ βπ β {(π β 1)} {((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)))) |
108 | 107 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (βπ β (0..^((π + 1) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β (βπ β (0..^(π β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β§ βπ β {(π β 1)} {((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)))) |
109 | 59, 96, 108 | mpbir2and 712 |
. . . . 5
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β βπ β (0..^((π + 1) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)) |
110 | | ccatlen 14470 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β
Word (VtxβπΊ)) β
(β―β(π ++
β¨β(πβ0)ββ©)) =
((β―βπ) +
(β―ββ¨β(πβ0)ββ©))) |
111 | 4, 6, 110 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (β―β(π ++ β¨β(πβ0)ββ©)) =
((β―βπ) +
(β―ββ¨β(πβ0)ββ©))) |
112 | | id 22 |
. . . . . . . . . . . 12
β’
((β―βπ) =
π β
(β―βπ) = π) |
113 | | s1len 14501 |
. . . . . . . . . . . . 13
β’
(β―ββ¨β(πβ0)ββ©) = 1 |
114 | 113 | a1i 11 |
. . . . . . . . . . . 12
β’
((β―βπ) =
π β
(β―ββ¨β(πβ0)ββ©) =
1) |
115 | 112, 114 | oveq12d 7380 |
. . . . . . . . . . 11
β’
((β―βπ) =
π β
((β―βπ) +
(β―ββ¨β(πβ0)ββ©)) = (π + 1)) |
116 | 115 | ad2antll 728 |
. . . . . . . . . 10
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β ((β―βπ) + (β―ββ¨β(πβ0)ββ©)) =
(π + 1)) |
117 | 111, 116 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (β―β(π ++ β¨β(πβ0)ββ©)) = (π + 1)) |
118 | 117 | 3adant3 1133 |
. . . . . . . 8
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (β―β(π ++ β¨β(πβ0)ββ©)) =
(π + 1)) |
119 | 118 | oveq1d 7377 |
. . . . . . 7
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β
((β―β(π ++
β¨β(πβ0)ββ©)) β 1) =
((π + 1) β
1)) |
120 | 119 | oveq2d 7378 |
. . . . . 6
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β
(0..^((β―β(π ++
β¨β(πβ0)ββ©)) β 1)) =
(0..^((π + 1) β
1))) |
121 | 120 | raleqdv 3316 |
. . . . 5
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (βπ β
(0..^((β―β(π ++
β¨β(πβ0)ββ©)) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ) β βπ β (0..^((π + 1) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ))) |
122 | 109, 121 | mpbird 257 |
. . . 4
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β βπ β
(0..^((β―β(π ++
β¨β(πβ0)ββ©)) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)) |
123 | 3, 9, 122 | 3jca 1129 |
. . 3
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β ((π ++ β¨β(πβ0)ββ©) β β
β§
(π ++ β¨β(πβ0)ββ©) β
Word (VtxβπΊ) β§
βπ β
(0..^((β―β(π ++
β¨β(πβ0)ββ©)) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ))) |
124 | | nnnn0 12427 |
. . . . . 6
β’ (π β β β π β
β0) |
125 | | iswwlksn 28825 |
. . . . . 6
β’ (π β β0
β ((π ++
β¨β(πβ0)ββ©) β (π WWalksN πΊ) β ((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1)))) |
126 | 124, 125 | syl 17 |
. . . . 5
β’ (π β β β ((π ++ β¨β(πβ0)ββ©) β
(π WWalksN πΊ) β ((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1)))) |
127 | | eqid 2737 |
. . . . . . 7
β’
(VtxβπΊ) =
(VtxβπΊ) |
128 | | eqid 2737 |
. . . . . . 7
β’
(EdgβπΊ) =
(EdgβπΊ) |
129 | 127, 128 | iswwlks 28823 |
. . . . . 6
β’ ((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β
((π ++ β¨β(πβ0)ββ©) β
β
β§ (π ++
β¨β(πβ0)ββ©) β Word
(VtxβπΊ) β§
βπ β
(0..^((β―β(π ++
β¨β(πβ0)ββ©)) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ))) |
130 | 129 | anbi1i 625 |
. . . . 5
β’ (((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1)) β (((π ++ β¨β(πβ0)ββ©) β
β
β§ (π ++
β¨β(πβ0)ββ©) β Word
(VtxβπΊ) β§
βπ β
(0..^((β―β(π ++
β¨β(πβ0)ββ©)) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)) β§ (β―β(π ++ β¨β(πβ0)ββ©)) =
(π + 1))) |
131 | 126, 130 | bitrdi 287 |
. . . 4
β’ (π β β β ((π ++ β¨β(πβ0)ββ©) β
(π WWalksN πΊ) β (((π ++ β¨β(πβ0)ββ©) β β
β§
(π ++ β¨β(πβ0)ββ©) β
Word (VtxβπΊ) β§
βπ β
(0..^((β―β(π ++
β¨β(πβ0)ββ©)) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)) β§ (β―β(π ++ β¨β(πβ0)ββ©)) =
(π + 1)))) |
132 | 131 | 3ad2ant1 1134 |
. . 3
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β (((π ++ β¨β(πβ0)ββ©) β β
β§
(π ++ β¨β(πβ0)ββ©) β
Word (VtxβπΊ) β§
βπ β
(0..^((β―β(π ++
β¨β(πβ0)ββ©)) β 1)){((π ++ β¨β(πβ0)ββ©)βπ), ((π ++ β¨β(πβ0)ββ©)β(π + 1))} β (EdgβπΊ)) β§ (β―β(π ++ β¨β(πβ0)ββ©)) =
(π + 1)))) |
133 | 123, 118,
132 | mpbir2and 712 |
. 2
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ)) |
134 | | lswccats1 14529 |
. . . . 5
β’ ((π β Word (VtxβπΊ) β§ (πβ0) β (VtxβπΊ)) β (lastSβ(π ++ β¨β(πβ0)ββ©)) =
(πβ0)) |
135 | 4, 5, 134 | syl2anc 585 |
. . . 4
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (lastSβ(π ++ β¨β(πβ0)ββ©)) = (πβ0)) |
136 | | lbfzo0 13619 |
. . . . . . . 8
β’ (0 β
(0..^π) β π β
β) |
137 | 136 | biimpri 227 |
. . . . . . 7
β’ (π β β β 0 β
(0..^π)) |
138 | 39 | eleq2d 2824 |
. . . . . . . 8
β’
((β―βπ) =
π β (0 β
(0..^(β―βπ))
β 0 β (0..^π))) |
139 | 138 | adantl 483 |
. . . . . . 7
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β (0 β (0..^(β―βπ)) β 0 β (0..^π))) |
140 | 137, 139 | syl5ibrcom 247 |
. . . . . 6
β’ (π β β β ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β 0 β (0..^(β―βπ)))) |
141 | 140 | imp 408 |
. . . . 5
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β 0 β (0..^(β―βπ))) |
142 | | ccatval1 14472 |
. . . . 5
β’ ((π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β
Word (VtxβπΊ) β§ 0
β (0..^(β―βπ))) β ((π ++ β¨β(πβ0)ββ©)β0) = (πβ0)) |
143 | 4, 6, 141, 142 | syl3anc 1372 |
. . . 4
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β ((π ++ β¨β(πβ0)ββ©)β0) = (πβ0)) |
144 | 135, 143 | eqtr4d 2780 |
. . 3
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (lastSβ(π ++ β¨β(πβ0)ββ©)) = ((π ++ β¨β(πβ0)ββ©)β0)) |
145 | 144 | 3adant3 1133 |
. 2
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (lastSβ(π ++ β¨β(πβ0)ββ©)) =
((π ++ β¨β(πβ0)ββ©)β0)) |
146 | | fveq2 6847 |
. . . 4
β’ (π€ = (π ++ β¨β(πβ0)ββ©) β
(lastSβπ€) =
(lastSβ(π ++
β¨β(πβ0)ββ©))) |
147 | | fveq1 6846 |
. . . 4
β’ (π€ = (π ++ β¨β(πβ0)ββ©) β (π€β0) = ((π ++ β¨β(πβ0)ββ©)β0)) |
148 | 146, 147 | eqeq12d 2753 |
. . 3
β’ (π€ = (π ++ β¨β(πβ0)ββ©) β
((lastSβπ€) = (π€β0) β
(lastSβ(π ++
β¨β(πβ0)ββ©)) = ((π ++ β¨β(πβ0)ββ©)β0))) |
149 | | clwwlkf1o.d |
. . 3
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} |
150 | 148, 149 | elrab2 3653 |
. 2
β’ ((π ++ β¨β(πβ0)ββ©) β
π· β ((π ++ β¨β(πβ0)ββ©) β
(π WWalksN πΊ) β§ (lastSβ(π ++ β¨β(πβ0)ββ©)) =
((π ++ β¨β(πβ0)ββ©)β0))) |
151 | 133, 145,
150 | sylanbrc 584 |
1
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (π ++ β¨β(πβ0)ββ©) β π·) |