Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | | wwlksnextprop.e |
. . . . 5
β’ πΈ = (EdgβπΊ) |
3 | 1, 2 | wwlknp 29097 |
. . . 4
β’ (π β ((π + 1) WWalksN πΊ) β (π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) |
4 | | fzonn0p1 13709 |
. . . . . . . . . . 11
β’ (π β β0
β π β (0..^(π + 1))) |
5 | 4 | adantl 483 |
. . . . . . . . . 10
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β π β (0..^(π + 1))) |
6 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
7 | | fvoveq1 7432 |
. . . . . . . . . . . . 13
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
8 | 6, 7 | preq12d 4746 |
. . . . . . . . . . . 12
β’ (π = π β {(πβπ), (πβ(π + 1))} = {(πβπ), (πβ(π + 1))}) |
9 | 8 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π = π β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβπ), (πβ(π + 1))} β πΈ)) |
10 | 9 | rspcv 3609 |
. . . . . . . . . 10
β’ (π β (0..^(π + 1)) β (βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ β {(πβπ), (πβ(π + 1))} β πΈ)) |
11 | 5, 10 | syl 17 |
. . . . . . . . 9
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β
(βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ β {(πβπ), (πβ(π + 1))} β πΈ)) |
12 | 11 | imp 408 |
. . . . . . . 8
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β§
βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β {(πβπ), (πβ(π + 1))} β πΈ) |
13 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β π β Word (VtxβπΊ)) |
14 | | 1zzd 12593 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β 1 β
β€) |
15 | | lencl 14483 |
. . . . . . . . . . . . . . . 16
β’ (π β Word (VtxβπΊ) β (β―βπ) β
β0) |
16 | 15 | nn0zd 12584 |
. . . . . . . . . . . . . . 15
β’ (π β Word (VtxβπΊ) β (β―βπ) β
β€) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β
(β―βπ) β
β€) |
18 | | peano2nn0 12512 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π + 1) β
β0) |
19 | 18 | nn0zd 12584 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β€) |
20 | 19 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π + 1) β
β€) |
21 | | nn0ge0 12497 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β 0 β€ π) |
22 | | 1red 11215 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β 1 β β) |
23 | | nn0re 12481 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β π β
β) |
24 | 22, 23 | addge02d 11803 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (0 β€ π β 1
β€ (π +
1))) |
25 | 21, 24 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β 1 β€ (π +
1)) |
26 | 25 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β 1 β€
(π + 1)) |
27 | 18 | nn0red 12533 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (π + 1) β
β) |
28 | 27 | lep1d 12145 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (π + 1) β€ ((π + 1) + 1)) |
29 | | breq2 5153 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ) =
((π + 1) + 1) β
((π + 1) β€
(β―βπ) β
(π + 1) β€ ((π + 1) + 1))) |
30 | 28, 29 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β ((β―βπ) =
((π + 1) + 1) β (π + 1) β€ (β―βπ))) |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ)
β β0 β (π β β0 β
((β―βπ) =
((π + 1) + 1) β (π + 1) β€ (β―βπ)))) |
32 | 31 | com23 86 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ)
β β0 β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π + 1) β€ (β―βπ)))) |
33 | 15, 32 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β Word (VtxβπΊ) β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π + 1) β€ (β―βπ)))) |
34 | 33 | imp31 419 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π + 1) β€ (β―βπ)) |
35 | 14, 17, 20, 26, 34 | elfzd 13492 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π + 1) β
(1...(β―βπ))) |
36 | | pfxfvlsw 14645 |
. . . . . . . . . . . . 13
β’ ((π β Word (VtxβπΊ) β§ (π + 1) β (1...(β―βπ))) β (lastSβ(π prefix (π + 1))) = (πβ((π + 1) β 1))) |
37 | 13, 35, 36 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β
(lastSβ(π prefix
(π + 1))) = (πβ((π + 1) β 1))) |
38 | | nn0cn 12482 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β π β
β) |
39 | | 1cnd 11209 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β 1 β β) |
40 | 38, 39 | pncand 11572 |
. . . . . . . . . . . . . 14
β’ (π β β0
β ((π + 1) β 1)
= π) |
41 | 40 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (π β β0
β (πβ((π + 1) β 1)) = (πβπ)) |
42 | 41 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (πβ((π + 1) β 1)) = (πβπ)) |
43 | 37, 42 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β
(lastSβ(π prefix
(π + 1))) = (πβπ)) |
44 | | lsw 14514 |
. . . . . . . . . . . . 13
β’ (π β Word (VtxβπΊ) β (lastSβπ) = (πβ((β―βπ) β 1))) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β
(lastSβπ) = (πβ((β―βπ) β 1))) |
46 | | fvoveq1 7432 |
. . . . . . . . . . . . . 14
β’
((β―βπ) =
((π + 1) + 1) β (πβ((β―βπ) β 1)) = (πβ(((π + 1) + 1) β 1))) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β (πβ((β―βπ) β 1)) = (πβ(((π + 1) + 1) β 1))) |
48 | 18 | nn0cnd 12534 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β) |
49 | 48, 39 | pncand 11572 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (((π + 1) + 1)
β 1) = (π +
1)) |
50 | 49 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (π β β0
β (πβ(((π + 1) + 1) β 1)) = (πβ(π + 1))) |
51 | 47, 50 | sylan9eq 2793 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (πβ((β―βπ) β 1)) = (πβ(π + 1))) |
52 | 45, 51 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β
(lastSβπ) = (πβ(π + 1))) |
53 | 43, 52 | preq12d 4746 |
. . . . . . . . . 10
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β
{(lastSβ(π prefix
(π + 1))),
(lastSβπ)} = {(πβπ), (πβ(π + 1))}) |
54 | 53 | eleq1d 2819 |
. . . . . . . . 9
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β
({(lastSβ(π prefix
(π + 1))),
(lastSβπ)} β
πΈ β {(πβπ), (πβ(π + 1))} β πΈ)) |
55 | 54 | adantr 482 |
. . . . . . . 8
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β§
βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β ({(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ β {(πβπ), (πβ(π + 1))} β πΈ)) |
56 | 12, 55 | mpbird 257 |
. . . . . . 7
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β§
βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ) |
57 | 56 | exp31 421 |
. . . . . 6
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β (π β β0 β
(βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ β {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ))) |
58 | 57 | com23 86 |
. . . . 5
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β (βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ β (π β β0 β
{(lastSβ(π prefix
(π + 1))),
(lastSβπ)} β
πΈ))) |
59 | 58 | 3impia 1118 |
. . . 4
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β (π β β0 β
{(lastSβ(π prefix
(π + 1))),
(lastSβπ)} β
πΈ)) |
60 | 3, 59 | syl 17 |
. . 3
β’ (π β ((π + 1) WWalksN πΊ) β (π β β0 β
{(lastSβ(π prefix
(π + 1))),
(lastSβπ)} β
πΈ)) |
61 | | wwlksnextprop.x |
. . 3
β’ π = ((π + 1) WWalksN πΊ) |
62 | 60, 61 | eleq2s 2852 |
. 2
β’ (π β π β (π β β0 β
{(lastSβ(π prefix
(π + 1))),
(lastSβπ)} β
πΈ)) |
63 | 62 | imp 408 |
1
β’ ((π β π β§ π β β0) β
{(lastSβ(π prefix
(π + 1))),
(lastSβπ)} β
πΈ) |