Step | Hyp | Ref
| Expression |
1 | | wwlksnextbij0.d |
. 2
β’ π· = {π€ β Word π β£ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)} |
2 | | 3anass 1096 |
. . . . 5
β’
(((β―βπ€)
= (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ) β ((β―βπ€) = (π + 2) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) |
3 | 2 | bianass 641 |
. . . 4
β’ ((π€ β Word π β§ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) |
4 | | wwlksnextbij0.v |
. . . . . . . . . . 11
β’ π = (VtxβπΊ) |
5 | 4 | wwlknbp 28829 |
. . . . . . . . . 10
β’ (π β (π WWalksN πΊ) β (πΊ β V β§ π β β0 β§ π β Word π)) |
6 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) β π β
β0) |
7 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β π€ β Word π) |
8 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β π β
β) |
9 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 β
β |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β 2 β β) |
11 | | nn0ge0 12445 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β 0 β€ π) |
12 | | 2pos 12263 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 <
2 |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β 0 < 2) |
14 | 8, 10, 11, 13 | addgegt0d 11735 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β 0 < (π +
2)) |
15 | 14 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β 0 < (π + 2)) |
16 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ€) =
(π + 2) β (0 <
(β―βπ€) β 0
< (π +
2))) |
17 | 16 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β (0 < (β―βπ€) β 0 < (π + 2))) |
18 | 15, 17 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β 0 < (β―βπ€)) |
19 | | hashgt0n0 14272 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ β Word π β§ 0 < (β―βπ€)) β π€ β β
) |
20 | 7, 18, 19 | syl2an2 685 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β π€ β β
) |
21 | | lswcl 14463 |
. . . . . . . . . . . . . . . 16
β’ ((π€ β Word π β§ π€ β β
) β (lastSβπ€) β π) |
22 | 7, 20, 21 | syl2an2 685 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β (lastSβπ€) β π) |
23 | 22 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) β (lastSβπ€) β π) |
24 | | pfxcl 14572 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β Word π β (π€ prefix (π + 1)) β Word π) |
25 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π€ prefix (π + 1)) β (π β Word π β (π€ prefix (π + 1)) β Word π)) |
26 | 24, 25 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π€ prefix (π + 1)) β (π€ β Word π β π β Word π)) |
27 | 26 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π€ prefix (π + 1)) = π β (π€ β Word π β π β Word π)) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ) β (π€ β Word π β π β Word π)) |
29 | 28 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’ (π€ β Word π β (((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ) β π β Word π)) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β (((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ) β π β Word π)) |
31 | 30 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β π β Word π) |
32 | 31 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) β π β Word π) |
33 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π€ prefix (π + 1)) β (π ++ β¨β(lastSβπ€)ββ©) = ((π€ prefix (π + 1)) ++ β¨β(lastSβπ€)ββ©)) |
34 | 33 | eqcoms 2745 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ prefix (π + 1)) = π β (π ++ β¨β(lastSβπ€)ββ©) = ((π€ prefix (π + 1)) ++ β¨β(lastSβπ€)ββ©)) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ) β (π ++ β¨β(lastSβπ€)ββ©) = ((π€ prefix (π + 1)) ++ β¨β(lastSβπ€)ββ©)) |
36 | 35 | ad2antll 728 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) β (π ++ β¨β(lastSβπ€)ββ©) = ((π€ prefix (π + 1)) ++ β¨β(lastSβπ€)ββ©)) |
37 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ€) =
(π + 2) β
((β―βπ€) β
1) = ((π + 2) β
1)) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β ((β―βπ€) β 1) = ((π + 2) β
1)) |
39 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β π β
β) |
40 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β 2 β β) |
41 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β 1 β β) |
42 | 39, 40, 41 | addsubassd 11539 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β ((π + 2) β 1)
= (π + (2 β
1))) |
43 | | 2m1e1 12286 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (2
β 1) = 1 |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β (2 β 1) = 1) |
45 | 44 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β (π + (2 β 1))
= (π + 1)) |
46 | 42, 45 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β ((π + 2) β 1)
= (π + 1)) |
47 | 38, 46 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β ((β―βπ€) β 1) = (π + 1)) |
48 | 47 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β (π€ prefix ((β―βπ€) β 1)) = (π€ prefix (π + 1))) |
49 | 48 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β ((π€ prefix ((β―βπ€) β 1)) ++
β¨β(lastSβπ€)ββ©) = ((π€ prefix (π + 1)) ++ β¨β(lastSβπ€)ββ©)) |
50 | | pfxlswccat 14608 |
. . . . . . . . . . . . . . . . . 18
β’ ((π€ β Word π β§ π€ β β
) β ((π€ prefix ((β―βπ€) β 1)) ++
β¨β(lastSβπ€)ββ©) = π€) |
51 | 7, 20, 50 | syl2an2 685 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β ((π€ prefix ((β―βπ€) β 1)) ++
β¨β(lastSβπ€)ββ©) = π€) |
52 | 49, 51 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ (π€ β Word π β§ (β―βπ€) = (π + 2))) β ((π€ prefix (π + 1)) ++ β¨β(lastSβπ€)ββ©) = π€) |
53 | 52 | adantrr 716 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) β ((π€ prefix (π + 1)) ++ β¨β(lastSβπ€)ββ©) = π€) |
54 | 36, 53 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) β π€ = (π ++ β¨β(lastSβπ€)ββ©)) |
55 | | simprrr 781 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) β {(lastSβπ), (lastSβπ€)} β πΈ) |
56 | | wwlksnextbij0.e |
. . . . . . . . . . . . . . 15
β’ πΈ = (EdgβπΊ) |
57 | 4, 56 | wwlksnextbi 28881 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ (lastSβπ€)
β π) β§ (π β Word π β§ π€ = (π ++ β¨β(lastSβπ€)ββ©) β§
{(lastSβπ),
(lastSβπ€)} β
πΈ)) β (π€ β ((π + 1) WWalksN πΊ) β π β (π WWalksN πΊ))) |
58 | 6, 23, 32, 54, 55, 57 | syl23anc 1378 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ ((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ))) β (π€ β ((π + 1) WWalksN πΊ) β π β (π WWalksN πΊ))) |
59 | 58 | exbiri 810 |
. . . . . . . . . . . 12
β’ (π β β0
β (((π€ β Word
π β§
(β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β (π β (π WWalksN πΊ) β π€ β ((π + 1) WWalksN πΊ)))) |
60 | 59 | com23 86 |
. . . . . . . . . . 11
β’ (π β β0
β (π β (π WWalksN πΊ) β (((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β π€ β ((π + 1) WWalksN πΊ)))) |
61 | 60 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((πΊ β V β§ π β β0
β§ π β Word π) β (π β (π WWalksN πΊ) β (((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β π€ β ((π + 1) WWalksN πΊ)))) |
62 | 5, 61 | mpcom 38 |
. . . . . . . . 9
β’ (π β (π WWalksN πΊ) β (((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β π€ β ((π + 1) WWalksN πΊ))) |
63 | 62 | expcomd 418 |
. . . . . . . 8
β’ (π β (π WWalksN πΊ) β (((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ) β ((π€ β Word π β§ (β―βπ€) = (π + 2)) β π€ β ((π + 1) WWalksN πΊ)))) |
64 | 63 | imp 408 |
. . . . . . 7
β’ ((π β (π WWalksN πΊ) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β ((π€ β Word π β§ (β―βπ€) = (π + 2)) β π€ β ((π + 1) WWalksN πΊ))) |
65 | 4, 56 | wwlknp 28830 |
. . . . . . . . . . . 12
β’ (π€ β ((π + 1) WWalksN πΊ) β (π€ β Word π β§ (β―βπ€) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(π€βπ), (π€β(π + 1))} β πΈ)) |
66 | 39, 41, 41 | addassd 11184 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β ((π + 1) + 1) =
(π + (1 +
1))) |
67 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 + 1) =
2 |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β (1 + 1) = 2) |
69 | 68 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (π + (1 + 1)) =
(π + 2)) |
70 | 66, 69 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β ((π + 1) + 1) =
(π + 2)) |
71 | 70 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β ((β―βπ€) =
((π + 1) + 1) β
(β―βπ€) = (π + 2))) |
72 | 71 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β ((β―βπ€) =
((π + 1) + 1) β
(β―βπ€) = (π + 2))) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π β Word π) β ((β―βπ€) = ((π + 1) + 1) β (β―βπ€) = (π + 2))) |
74 | 73 | com12 32 |
. . . . . . . . . . . . . . 15
β’
((β―βπ€) =
((π + 1) + 1) β
((π β
β0 β§ π
β Word π) β
(β―βπ€) = (π + 2))) |
75 | 74 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π€ β Word π β§ (β―βπ€) = ((π + 1) + 1)) β ((π β β0 β§ π β Word π) β (β―βπ€) = (π + 2))) |
76 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π€ β Word π β§ (β―βπ€) = ((π + 1) + 1)) β π€ β Word π) |
77 | 75, 76 | jctild 527 |
. . . . . . . . . . . . 13
β’ ((π€ β Word π β§ (β―βπ€) = ((π + 1) + 1)) β ((π β β0 β§ π β Word π) β (π€ β Word π β§ (β―βπ€) = (π + 2)))) |
78 | 77 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π€ β Word π β§ (β―βπ€) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(π€βπ), (π€β(π + 1))} β πΈ) β ((π β β0 β§ π β Word π) β (π€ β Word π β§ (β―βπ€) = (π + 2)))) |
79 | 65, 78 | syl 17 |
. . . . . . . . . . 11
β’ (π€ β ((π + 1) WWalksN πΊ) β ((π β β0 β§ π β Word π) β (π€ β Word π β§ (β―βπ€) = (π + 2)))) |
80 | 79 | com12 32 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β Word π) β (π€ β ((π + 1) WWalksN πΊ) β (π€ β Word π β§ (β―βπ€) = (π + 2)))) |
81 | 80 | 3adant1 1131 |
. . . . . . . . 9
β’ ((πΊ β V β§ π β β0
β§ π β Word π) β (π€ β ((π + 1) WWalksN πΊ) β (π€ β Word π β§ (β―βπ€) = (π + 2)))) |
82 | 5, 81 | syl 17 |
. . . . . . . 8
β’ (π β (π WWalksN πΊ) β (π€ β ((π + 1) WWalksN πΊ) β (π€ β Word π β§ (β―βπ€) = (π + 2)))) |
83 | 82 | adantr 482 |
. . . . . . 7
β’ ((π β (π WWalksN πΊ) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β (π€ β ((π + 1) WWalksN πΊ) β (π€ β Word π β§ (β―βπ€) = (π + 2)))) |
84 | 64, 83 | impbid 211 |
. . . . . 6
β’ ((π β (π WWalksN πΊ) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β ((π€ β Word π β§ (β―βπ€) = (π + 2)) β π€ β ((π + 1) WWalksN πΊ))) |
85 | 84 | ex 414 |
. . . . 5
β’ (π β (π WWalksN πΊ) β (((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ) β ((π€ β Word π β§ (β―βπ€) = (π + 2)) β π€ β ((π + 1) WWalksN πΊ)))) |
86 | 85 | pm5.32rd 579 |
. . . 4
β’ (π β (π WWalksN πΊ) β (((π€ β Word π β§ (β―βπ€) = (π + 2)) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β (π€ β ((π + 1) WWalksN πΊ) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)))) |
87 | 3, 86 | bitrid 283 |
. . 3
β’ (π β (π WWalksN πΊ) β ((π€ β Word π β§ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)) β (π€ β ((π + 1) WWalksN πΊ) β§ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)))) |
88 | 87 | rabbidva2 3412 |
. 2
β’ (π β (π WWalksN πΊ) β {π€ β Word π β£ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)} = {π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)}) |
89 | 1, 88 | eqtrid 2789 |
1
β’ (π β (π WWalksN πΊ) β π· = {π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)}) |