Step | Hyp | Ref
| Expression |
1 | | eqidd 2737 |
. . 3
β’ ((π β β0
β§ π β ((π + 1) WWalksN πΊ)) β (π prefix (π + 1)) = (π prefix (π + 1))) |
2 | | eqid 2736 |
. . . . 5
β’
(VtxβπΊ) =
(VtxβπΊ) |
3 | | wwlksnredwwlkn.e |
. . . . 5
β’ πΈ = (EdgβπΊ) |
4 | 2, 3 | wwlknp 28788 |
. . . 4
β’ (π β ((π + 1) WWalksN πΊ) β (π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) |
5 | | simprl 769 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1))) β π β Word (VtxβπΊ)) |
6 | | peano2nn0 12453 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π + 1) β
β0) |
7 | | peano2nn0 12453 |
. . . . . . . . . . . . 13
β’ ((π + 1) β β0
β ((π + 1) + 1) β
β0) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
β’ (π β β0
β ((π + 1) + 1) β
β0) |
9 | | id 22 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β0) |
10 | | nn0p1nn 12452 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β β0
β ((π + 1) + 1) β
β) |
11 | 6, 10 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β0
β ((π + 1) + 1) β
β) |
12 | | nn0re 12422 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β π β
β) |
13 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
14 | | peano2re 11328 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
β) |
15 | | peano2re 11328 |
. . . . . . . . . . . . . . . . 17
β’ ((π + 1) β β β
((π + 1) + 1) β
β) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π + 1) + 1) β
β) |
17 | 13, 14, 16 | 3jca 1128 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π β β β§ (π + 1) β β β§
((π + 1) + 1) β
β)) |
18 | 12, 17 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π β β
β§ (π + 1) β
β β§ ((π + 1) + 1)
β β)) |
19 | 12 | ltp1d 12085 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π < (π + 1)) |
20 | | nn0re 12422 |
. . . . . . . . . . . . . . . 16
β’ ((π + 1) β β0
β (π + 1) β
β) |
21 | 6, 20 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β) |
22 | 21 | ltp1d 12085 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 1) < ((π + 1) + 1)) |
23 | | lttr 11231 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ (π + 1) β β β§
((π + 1) + 1) β
β) β ((π <
(π + 1) β§ (π + 1) < ((π + 1) + 1)) β π < ((π + 1) + 1))) |
24 | 23 | imp 407 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π + 1) β β β§
((π + 1) + 1) β
β) β§ (π <
(π + 1) β§ (π + 1) < ((π + 1) + 1))) β π < ((π + 1) + 1)) |
25 | 18, 19, 22, 24 | syl12anc 835 |
. . . . . . . . . . . . 13
β’ (π β β0
β π < ((π + 1) + 1)) |
26 | | elfzo0 13613 |
. . . . . . . . . . . . 13
β’ (π β (0..^((π + 1) + 1)) β (π β β0 β§ ((π + 1) + 1) β β β§
π < ((π + 1) + 1))) |
27 | 9, 11, 25, 26 | syl3anbrc 1343 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
(0..^((π + 1) +
1))) |
28 | | fz0add1fz1 13642 |
. . . . . . . . . . . 12
β’ ((((π + 1) + 1) β
β0 β§ π
β (0..^((π + 1) + 1)))
β (π + 1) β
(1...((π + 1) +
1))) |
29 | 8, 27, 28 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β β0
β (π + 1) β
(1...((π + 1) +
1))) |
30 | 29 | adantr 481 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1))) β (π + 1) β (1...((π + 1) + 1))) |
31 | | oveq2 7365 |
. . . . . . . . . . . . 13
β’
((β―βπ) =
((π + 1) + 1) β
(1...(β―βπ)) =
(1...((π + 1) +
1))) |
32 | 31 | eleq2d 2823 |
. . . . . . . . . . . 12
β’
((β―βπ) =
((π + 1) + 1) β
((π + 1) β
(1...(β―βπ))
β (π + 1) β
(1...((π + 1) +
1)))) |
33 | 32 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β ((π + 1) β (1...(β―βπ)) β (π + 1) β (1...((π + 1) + 1)))) |
34 | 33 | adantl 482 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1))) β ((π + 1) β
(1...(β―βπ))
β (π + 1) β
(1...((π + 1) +
1)))) |
35 | 30, 34 | mpbird 256 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1))) β (π + 1) β
(1...(β―βπ))) |
36 | 5, 35 | jca 512 |
. . . . . . . 8
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1))) β (π β Word (VtxβπΊ) β§ (π + 1) β (1...(β―βπ)))) |
37 | 36 | 3adantr3 1171 |
. . . . . . 7
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β (π β Word (VtxβπΊ) β§ (π + 1) β (1...(β―βπ)))) |
38 | | pfxfvlsw 14583 |
. . . . . . 7
β’ ((π β Word (VtxβπΊ) β§ (π + 1) β (1...(β―βπ))) β (lastSβ(π prefix (π + 1))) = (πβ((π + 1) β 1))) |
39 | 37, 38 | syl 17 |
. . . . . 6
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β (lastSβ(π prefix (π + 1))) = (πβ((π + 1) β 1))) |
40 | | lsw 14452 |
. . . . . . . 8
β’ (π β Word (VtxβπΊ) β (lastSβπ) = (πβ((β―βπ) β 1))) |
41 | 40 | 3ad2ant1 1133 |
. . . . . . 7
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β (lastSβπ) = (πβ((β―βπ) β 1))) |
42 | 41 | adantl 482 |
. . . . . 6
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β (lastSβπ) = (πβ((β―βπ) β 1))) |
43 | 39, 42 | preq12d 4702 |
. . . . 5
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β {(lastSβ(π prefix (π + 1))), (lastSβπ)} = {(πβ((π + 1) β 1)), (πβ((β―βπ) β 1))}) |
44 | | oveq1 7364 |
. . . . . . . . . . 11
β’
((β―βπ) =
((π + 1) + 1) β
((β―βπ) β
1) = (((π + 1) + 1) β
1)) |
45 | 44 | 3ad2ant2 1134 |
. . . . . . . . . 10
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β ((β―βπ) β 1) = (((π + 1) + 1) β 1)) |
46 | 45 | adantl 482 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β ((β―βπ) β 1) = (((π + 1) + 1) β 1)) |
47 | 46 | fveq2d 6846 |
. . . . . . . 8
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β (πβ((β―βπ) β 1)) = (πβ(((π + 1) + 1) β 1))) |
48 | 47 | preq2d 4701 |
. . . . . . 7
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β {(πβ((π + 1) β 1)), (πβ((β―βπ) β 1))} = {(πβ((π + 1) β 1)), (πβ(((π + 1) + 1) β 1))}) |
49 | | nn0cn 12423 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β) |
50 | | 1cnd 11150 |
. . . . . . . . . . 11
β’ (π β β0
β 1 β β) |
51 | 49, 50 | pncand 11513 |
. . . . . . . . . 10
β’ (π β β0
β ((π + 1) β 1)
= π) |
52 | 51 | fveq2d 6846 |
. . . . . . . . 9
β’ (π β β0
β (πβ((π + 1) β 1)) = (πβπ)) |
53 | 6 | nn0cnd 12475 |
. . . . . . . . . . 11
β’ (π β β0
β (π + 1) β
β) |
54 | 53, 50 | pncand 11513 |
. . . . . . . . . 10
β’ (π β β0
β (((π + 1) + 1)
β 1) = (π +
1)) |
55 | 54 | fveq2d 6846 |
. . . . . . . . 9
β’ (π β β0
β (πβ(((π + 1) + 1) β 1)) = (πβ(π + 1))) |
56 | 52, 55 | preq12d 4702 |
. . . . . . . 8
β’ (π β β0
β {(πβ((π + 1) β 1)), (πβ(((π + 1) + 1) β 1))} = {(πβπ), (πβ(π + 1))}) |
57 | 56 | adantr 481 |
. . . . . . 7
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β {(πβ((π + 1) β 1)), (πβ(((π + 1) + 1) β 1))} = {(πβπ), (πβ(π + 1))}) |
58 | 48, 57 | eqtrd 2776 |
. . . . . 6
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β {(πβ((π + 1) β 1)), (πβ((β―βπ) β 1))} = {(πβπ), (πβ(π + 1))}) |
59 | | fveq2 6842 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
60 | | fvoveq1 7380 |
. . . . . . . . . . . 12
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
61 | 59, 60 | preq12d 4702 |
. . . . . . . . . . 11
β’ (π = π β {(πβπ), (πβ(π + 1))} = {(πβπ), (πβ(π + 1))}) |
62 | 61 | eleq1d 2822 |
. . . . . . . . . 10
β’ (π = π β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβπ), (πβ(π + 1))} β πΈ)) |
63 | 62 | rspcv 3577 |
. . . . . . . . 9
β’ (π β (0..^(π + 1)) β (βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ β {(πβπ), (πβ(π + 1))} β πΈ)) |
64 | | fzonn0p1 13649 |
. . . . . . . . 9
β’ (π β β0
β π β (0..^(π + 1))) |
65 | 63, 64 | syl11 33 |
. . . . . . . 8
β’
(βπ β
(0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ β (π β β0 β {(πβπ), (πβ(π + 1))} β πΈ)) |
66 | 65 | 3ad2ant3 1135 |
. . . . . . 7
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β (π β β0 β {(πβπ), (πβ(π + 1))} β πΈ)) |
67 | 66 | impcom 408 |
. . . . . 6
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β {(πβπ), (πβ(π + 1))} β πΈ) |
68 | 58, 67 | eqeltrd 2837 |
. . . . 5
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β {(πβ((π + 1) β 1)), (πβ((β―βπ) β 1))} β πΈ) |
69 | 43, 68 | eqeltrd 2837 |
. . . 4
β’ ((π β β0
β§ (π β Word
(VtxβπΊ) β§
(β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) β {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ) |
70 | 4, 69 | sylan2 593 |
. . 3
β’ ((π β β0
β§ π β ((π + 1) WWalksN πΊ)) β {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ) |
71 | | wwlksnred 28837 |
. . . . 5
β’ (π β β0
β (π β ((π + 1) WWalksN πΊ) β (π prefix (π + 1)) β (π WWalksN πΊ))) |
72 | 71 | imp 407 |
. . . 4
β’ ((π β β0
β§ π β ((π + 1) WWalksN πΊ)) β (π prefix (π + 1)) β (π WWalksN πΊ)) |
73 | | eqeq2 2748 |
. . . . . 6
β’ (π¦ = (π prefix (π + 1)) β ((π prefix (π + 1)) = π¦ β (π prefix (π + 1)) = (π prefix (π + 1)))) |
74 | | fveq2 6842 |
. . . . . . . 8
β’ (π¦ = (π prefix (π + 1)) β (lastSβπ¦) = (lastSβ(π prefix (π + 1)))) |
75 | 74 | preq1d 4700 |
. . . . . . 7
β’ (π¦ = (π prefix (π + 1)) β {(lastSβπ¦), (lastSβπ)} = {(lastSβ(π prefix (π + 1))), (lastSβπ)}) |
76 | 75 | eleq1d 2822 |
. . . . . 6
β’ (π¦ = (π prefix (π + 1)) β ({(lastSβπ¦), (lastSβπ)} β πΈ β {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ)) |
77 | 73, 76 | anbi12d 631 |
. . . . 5
β’ (π¦ = (π prefix (π + 1)) β (((π prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ)} β πΈ) β ((π prefix (π + 1)) = (π prefix (π + 1)) β§ {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ))) |
78 | 77 | adantl 482 |
. . . 4
β’ (((π β β0
β§ π β ((π + 1) WWalksN πΊ)) β§ π¦ = (π prefix (π + 1))) β (((π prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ)} β πΈ) β ((π prefix (π + 1)) = (π prefix (π + 1)) β§ {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ))) |
79 | 72, 78 | rspcedv 3574 |
. . 3
β’ ((π β β0
β§ π β ((π + 1) WWalksN πΊ)) β (((π prefix (π + 1)) = (π prefix (π + 1)) β§ {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ) β βπ¦ β (π WWalksN πΊ)((π prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ)} β πΈ))) |
80 | 1, 70, 79 | mp2and 697 |
. 2
β’ ((π β β0
β§ π β ((π + 1) WWalksN πΊ)) β βπ¦ β (π WWalksN πΊ)((π prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ)} β πΈ)) |
81 | 80 | ex 413 |
1
β’ (π β β0
β (π β ((π + 1) WWalksN πΊ) β βπ¦ β (π WWalksN πΊ)((π prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ)} β πΈ))) |