Step | Hyp | Ref
| Expression |
1 | | wwlksnext.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | 1 | wwlknbp 28829 |
. . 3
β’ (π β (π WWalksN πΊ) β (πΊ β V β§ π β β0 β§ π β Word π)) |
3 | | wwlksnext.e |
. . . . . . . . . . 11
β’ πΈ = (EdgβπΊ) |
4 | 1, 3 | wwlknp 28830 |
. . . . . . . . . 10
β’ (π β (π WWalksN πΊ) β (π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ)) |
5 | | simp1 1137 |
. . . . . . . . . . . . . . 15
β’ ((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β π β Word π) |
6 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ (π β π β§ {(lastSβπ), π} β πΈ)) β π β π) |
7 | | cats1un 14616 |
. . . . . . . . . . . . . . 15
β’ ((π β Word π β§ π β π) β (π ++ β¨βπββ©) = (π βͺ {β¨(β―βπ), πβ©})) |
8 | 5, 6, 7 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (π ++ β¨βπββ©) = (π βͺ {β¨(β―βπ), πβ©})) |
9 | | opex 5426 |
. . . . . . . . . . . . . . . . . . 19
β’
β¨(β―βπ), πβ© β V |
10 | 9 | snnz 4742 |
. . . . . . . . . . . . . . . . . 18
β’
{β¨(β―βπ), πβ©} β β
|
11 | 10 | neii 2946 |
. . . . . . . . . . . . . . . . 17
β’ Β¬
{β¨(β―βπ),
πβ©} =
β
|
12 | 11 | intnan 488 |
. . . . . . . . . . . . . . . 16
β’ Β¬
(π = β
β§
{β¨(β―βπ),
πβ©} =
β
) |
13 | | df-ne 2945 |
. . . . . . . . . . . . . . . . 17
β’ ((π βͺ
{β¨(β―βπ),
πβ©}) β β
β Β¬ (π βͺ
{β¨(β―βπ),
πβ©}) =
β
) |
14 | | un00 4407 |
. . . . . . . . . . . . . . . . 17
β’ ((π = β
β§
{β¨(β―βπ),
πβ©} = β
) β
(π βͺ
{β¨(β―βπ),
πβ©}) =
β
) |
15 | 13, 14 | xchbinxr 335 |
. . . . . . . . . . . . . . . 16
β’ ((π βͺ
{β¨(β―βπ),
πβ©}) β β
β Β¬ (π = β
β§ {β¨(β―βπ), πβ©} = β
)) |
16 | 12, 15 | mpbir 230 |
. . . . . . . . . . . . . . 15
β’ (π βͺ
{β¨(β―βπ),
πβ©}) β
β
|
17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (π βͺ {β¨(β―βπ), πβ©}) β β
) |
18 | 8, 17 | eqnetrd 3012 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (π ++ β¨βπββ©) β
β
) |
19 | | s1cl 14497 |
. . . . . . . . . . . . . . 15
β’ (π β π β β¨βπββ© β Word π) |
20 | 19 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ (π β π β§ {(lastSβπ), π} β πΈ)) β β¨βπββ© β Word π) |
21 | | ccatcl 14469 |
. . . . . . . . . . . . . 14
β’ ((π β Word π β§ β¨βπββ© β Word π) β (π ++ β¨βπββ©) β Word π) |
22 | 5, 20, 21 | syl2an 597 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (π ++ β¨βπββ©) β Word π) |
23 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β π β Word π) |
24 | | fzossfzop1 13657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β β0
β (0..^π) β
(0..^(π +
1))) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β (0..^π) β (0..^(π + 1))) |
26 | 25 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β π β (0..^(π + 1))) |
27 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((β―βπ) =
(π + 1) β
(0..^(β―βπ)) =
(0..^(π +
1))) |
28 | 27 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((β―βπ) =
(π + 1) β (π β
(0..^(β―βπ))
β π β (0..^(π + 1)))) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β Word π β§ (β―βπ) = (π + 1)) β (π β (0..^(β―βπ)) β π β (0..^(π + 1)))) |
30 | 29 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β (π β (0..^(β―βπ)) β π β (0..^(π + 1)))) |
31 | 26, 30 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β π β (0..^(β―βπ))) |
32 | | ccats1val1 14521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β Word π β§ π β (0..^(β―βπ))) β ((π ++ β¨βπββ©)βπ) = (πβπ)) |
33 | 23, 31, 32 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β ((π ++ β¨βπββ©)βπ) = (πβπ)) |
34 | | fzonn0p1p1 13658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (0..^π) β (π + 1) β (0..^(π + 1))) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β (π + 1) β (0..^(π + 1))) |
36 | 27 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β Word π β§ (β―βπ) = (π + 1)) β (0..^(β―βπ)) = (0..^(π + 1))) |
37 | 36 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β (0..^(β―βπ)) = (0..^(π + 1))) |
38 | 35, 37 | eleqtrrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β (π + 1) β (0..^(β―βπ))) |
39 | | ccats1val1 14521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β Word π β§ (π + 1) β (0..^(β―βπ))) β ((π ++ β¨βπββ©)β(π + 1)) = (πβ(π + 1))) |
40 | 23, 38, 39 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β ((π ++ β¨βπββ©)β(π + 1)) = (πβ(π + 1))) |
41 | 33, 40 | preq12d 4707 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ (β―βπ) = (π + 1))) β§ π β (0..^π)) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} = {(πβπ), (πβ(π + 1))}) |
42 | 41 | exp31 421 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β0
β§ π β π) β ((π β Word π β§ (β―βπ) = (π + 1)) β (π β (0..^π) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} = {(πβπ), (πβ(π + 1))}))) |
43 | 42 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β0
β§ (π β π β§ {(lastSβπ), π} β πΈ)) β ((π β Word π β§ (β―βπ) = (π + 1)) β (π β (0..^π) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} = {(πβπ), (πβ(π + 1))}))) |
44 | 43 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β Word π β§ (β―βπ) = (π + 1)) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (π β (0..^π) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} = {(πβπ), (πβ(π + 1))})) |
45 | 44 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β Word π β§ (β―βπ) = (π + 1)) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β§ π β (0..^π)) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} = {(πβπ), (πβ(π + 1))}) |
46 | 45 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β Word π β§ (β―βπ) = (π + 1)) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β§ π β (0..^π)) β ({((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β {(πβπ), (πβ(π + 1))} β πΈ)) |
47 | 46 | ralbidva 3173 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β Word π β§ (β―βπ) = (π + 1)) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ)) |
48 | 47 | exbiri 810 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word π β§ (β―βπ) = (π + 1)) β ((π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ)) β (βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ β βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ))) |
49 | 48 | com23 86 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Word π β§ (β―βπ) = (π + 1)) β (βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ β ((π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ)) β βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ))) |
50 | 49 | 3impia 1118 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β ((π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ)) β βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
51 | 50 | imp 408 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) |
52 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((β―βπ) =
(π + 1) β
((β―βπ) β
1) = ((π + 1) β
1)) |
53 | 52 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β Word π β§ (β―βπ) = (π + 1)) β ((β―βπ) β 1) = ((π + 1) β
1)) |
54 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β0
β π β
β) |
55 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β0
β 1 β β) |
56 | 54, 55 | pncand 11520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β0
β ((π + 1) β 1)
= π) |
57 | 56 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β π β§ π β β0) β ((π + 1) β 1) = π) |
58 | 53, 57 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β ((β―βπ) β 1) = π) |
59 | 58 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β (πβ((β―βπ) β 1)) = (πβπ)) |
60 | | lsw 14459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
61 | 60 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β (lastSβπ) = (πβ((β―βπ) β 1))) |
62 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β π β Word π) |
63 | | fzonn0p1 13656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β0
β π β (0..^(π + 1))) |
64 | 63 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β π β (0..^(π + 1))) |
65 | 27 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((β―βπ) =
(π + 1) β (π β
(0..^(β―βπ))
β π β (0..^(π + 1)))) |
66 | 65 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β (π β (0..^(β―βπ)) β π β (0..^(π + 1)))) |
67 | 64, 66 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β π β (0..^(β―βπ))) |
68 | | ccats1val1 14521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β Word π β§ π β (0..^(β―βπ))) β ((π ++ β¨βπββ©)βπ) = (πβπ)) |
69 | 62, 67, 68 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β ((π ++ β¨βπββ©)βπ) = (πβπ)) |
70 | 59, 61, 69 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β (lastSβπ) = ((π ++ β¨βπββ©)βπ)) |
71 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β π β π) |
72 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β (β―βπ) = (π + 1)) |
73 | 72 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β (π + 1) = (β―βπ)) |
74 | | ccats1val2 14522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β Word π β§ π β π β§ (π + 1) = (β―βπ)) β ((π ++ β¨βπββ©)β(π + 1)) = π) |
75 | 74 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β Word π β§ π β π β§ (π + 1) = (β―βπ)) β π = ((π ++ β¨βπββ©)β(π + 1))) |
76 | 62, 71, 73, 75 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β π = ((π ++ β¨βπββ©)β(π + 1))) |
77 | 70, 76 | preq12d 4707 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β {(lastSβπ), π} = {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))}) |
78 | 77 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β ({(lastSβπ), π} β πΈ β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
79 | 78 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
({(lastSβπ),
π} β πΈ β (((π β π β§ π β β0) β§ (π β Word π β§ (β―βπ) = (π + 1))) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
80 | 79 | exp4c 434 |
. . . . . . . . . . . . . . . . . . . . 21
β’
({(lastSβπ),
π} β πΈ β (π β π β (π β β0 β ((π β Word π β§ (β―βπ) = (π + 1)) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)))) |
81 | 80 | impcom 409 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π β§ {(lastSβπ), π} β πΈ) β (π β β0 β ((π β Word π β§ (β―βπ) = (π + 1)) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ))) |
82 | 81 | impcom 409 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ (π β π β§ {(lastSβπ), π} β πΈ)) β ((π β Word π β§ (β―βπ) = (π + 1)) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
83 | 82 | impcom 409 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Word π β§ (β―βπ) = (π + 1)) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) |
84 | 83 | 3adantl3 1169 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) |
85 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π ++ β¨βπββ©)βπ) = ((π ++ β¨βπββ©)βπ)) |
86 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π ++ β¨βπββ©)β(π + 1)) = ((π ++ β¨βπββ©)β(π + 1))) |
87 | 85, 86 | preq12d 4707 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} = {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))}) |
88 | 87 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ({((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
89 | 88 | ralsng 4639 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (βπ β
{π} {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
90 | 89 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (βπ β {π} {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
91 | 84, 90 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β βπ β {π} {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) |
92 | | ralunb 4156 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
((0..^π) βͺ {π}){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β (βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β§ βπ β {π} {((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
93 | 51, 91, 92 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β βπ β ((0..^π) βͺ {π}){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) |
94 | | elnn0uz 12815 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β π β
(β€β₯β0)) |
95 | | eluzfz2 13456 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯β0) β π β (0...π)) |
96 | 94, 95 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β (0...π)) |
97 | | fzelp1 13500 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0...π) β π β (0...(π + 1))) |
98 | | fzosplit 13612 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0...(π + 1)) β (0..^(π + 1)) = ((0..^π) βͺ (π..^(π + 1)))) |
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (0..^(π + 1)) =
((0..^π) βͺ (π..^(π + 1)))) |
100 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β π β
β€) |
101 | | fzosn 13650 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β€ β (π..^(π + 1)) = {π}) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (π..^(π + 1)) = {π}) |
103 | 102 | uneq2d 4128 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β ((0..^π) βͺ
(π..^(π + 1))) = ((0..^π) βͺ {π})) |
104 | 99, 103 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (0..^(π + 1)) =
((0..^π) βͺ {π})) |
105 | 104 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
106 | 105 | raleqdv 3316 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (βπ β (0..^(π + 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β βπ β ((0..^π) βͺ {π}){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
107 | 93, 106 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β βπ β (0..^(π + 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) |
108 | | ccatlen 14470 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word π β§ β¨βπββ© β Word π) β (β―β(π ++ β¨βπββ©)) = ((β―βπ) +
(β―ββ¨βπββ©))) |
109 | 5, 20, 108 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (β―β(π ++ β¨βπββ©)) = ((β―βπ) +
(β―ββ¨βπββ©))) |
110 | 109 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β ((β―β(π ++ β¨βπββ©)) β 1) =
(((β―βπ) +
(β―ββ¨βπββ©)) β 1)) |
111 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (β―βπ) = (π + 1)) |
112 | | s1len 14501 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β―ββ¨βπββ©) = 1 |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (β―ββ¨βπββ©) =
1) |
114 | 111, 113 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β ((β―βπ) + (β―ββ¨βπββ©)) = ((π + 1) + 1)) |
115 | 114 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (((β―βπ) +
(β―ββ¨βπββ©)) β 1) = (((π + 1) + 1) β
1)) |
116 | | peano2nn0 12460 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (π + 1) β
β0) |
117 | 116 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (π + 1) β
β) |
118 | 117, 55 | pncand 11520 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (((π + 1) + 1)
β 1) = (π +
1)) |
119 | 118 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (((π + 1) + 1) β 1) = (π + 1)) |
120 | 110, 115,
119 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β ((β―β(π ++ β¨βπββ©)) β 1) =
(π + 1)) |
121 | 120 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (0..^((β―β(π ++ β¨βπββ©)) β 1)) =
(0..^(π +
1))) |
122 | 121 | raleqdv 3316 |
. . . . . . . . . . . . . 14
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (βπ β (0..^((β―β(π ++ β¨βπββ©)) β
1)){((π ++
β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ β βπ β (0..^(π + 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
123 | 107, 122 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β βπ β (0..^((β―β(π ++ β¨βπββ©)) β
1)){((π ++
β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) |
124 | 18, 22, 123 | 3jca 1129 |
. . . . . . . . . . . 12
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β ((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
125 | 109, 114 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)) |
126 | 124, 125 | jca 513 |
. . . . . . . . . . 11
β’ (((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β§ (π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ))) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1))) |
127 | 126 | ex 414 |
. . . . . . . . . 10
β’ ((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ) β ((π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ)) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
128 | 4, 127 | syl 17 |
. . . . . . . . 9
β’ (π β (π WWalksN πΊ) β ((π β β0 β§ (π β π β§ {(lastSβπ), π} β πΈ)) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
129 | 128 | expd 417 |
. . . . . . . 8
β’ (π β (π WWalksN πΊ) β (π β β0 β ((π β π β§ {(lastSβπ), π} β πΈ) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1))))) |
130 | 129 | impcom 409 |
. . . . . . 7
β’ ((π β β0
β§ π β (π WWalksN πΊ)) β ((π β π β§ {(lastSβπ), π} β πΈ) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
131 | 130 | adantll 713 |
. . . . . 6
β’ (((πΊ β V β§ π β β0)
β§ π β (π WWalksN πΊ)) β ((π β π β§ {(lastSβπ), π} β πΈ) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
132 | | iswwlksn 28825 |
. . . . . . . . . 10
β’ ((π + 1) β β0
β ((π ++
β¨βπββ©) β ((π + 1) WWalksN πΊ) β ((π ++ β¨βπββ©) β (WWalksβπΊ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
133 | 116, 132 | syl 17 |
. . . . . . . . 9
β’ (π β β0
β ((π ++
β¨βπββ©) β ((π + 1) WWalksN πΊ) β ((π ++ β¨βπββ©) β (WWalksβπΊ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
134 | 133 | adantl 483 |
. . . . . . . 8
β’ ((πΊ β V β§ π β β0)
β ((π ++
β¨βπββ©) β ((π + 1) WWalksN πΊ) β ((π ++ β¨βπββ©) β (WWalksβπΊ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
135 | 1, 3 | iswwlks 28823 |
. . . . . . . . 9
β’ ((π ++ β¨βπββ©) β
(WWalksβπΊ) β
((π ++ β¨βπββ©) β β
β§ (π ++
β¨βπββ©) β Word π β§ βπ β (0..^((β―β(π ++ β¨βπββ©)) β
1)){((π ++
β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ)) |
136 | 135 | anbi1i 625 |
. . . . . . . 8
β’ (((π ++ β¨βπββ©) β
(WWalksβπΊ) β§
(β―β(π ++
β¨βπββ©)) = ((π + 1) + 1)) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1))) |
137 | 134, 136 | bitrdi 287 |
. . . . . . 7
β’ ((πΊ β V β§ π β β0)
β ((π ++
β¨βπββ©) β ((π + 1) WWalksN πΊ) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
138 | 137 | adantr 482 |
. . . . . 6
β’ (((πΊ β V β§ π β β0)
β§ π β (π WWalksN πΊ)) β ((π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ) β (((π ++ β¨βπββ©) β β
β§ (π ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β(π ++
β¨βπββ©)) β 1)){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β πΈ) β§ (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1)))) |
139 | 131, 138 | sylibrd 259 |
. . . . 5
β’ (((πΊ β V β§ π β β0)
β§ π β (π WWalksN πΊ)) β ((π β π β§ {(lastSβπ), π} β πΈ) β (π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ))) |
140 | 139 | ex 414 |
. . . 4
β’ ((πΊ β V β§ π β β0)
β (π β (π WWalksN πΊ) β ((π β π β§ {(lastSβπ), π} β πΈ) β (π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ)))) |
141 | 140 | 3adant3 1133 |
. . 3
β’ ((πΊ β V β§ π β β0
β§ π β Word π) β (π β (π WWalksN πΊ) β ((π β π β§ {(lastSβπ), π} β πΈ) β (π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ)))) |
142 | 2, 141 | mpcom 38 |
. 2
β’ (π β (π WWalksN πΊ) β ((π β π β§ {(lastSβπ), π} β πΈ) β (π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ))) |
143 | 142 | 3impib 1117 |
1
β’ ((π β (π WWalksN πΊ) β§ π β π β§ {(lastSβπ), π} β πΈ) β (π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ)) |