Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12460 |
. . . . . . . . . . . 12
β’ (π β β0
β (π + 1) β
β0) |
2 | | iswwlksn 28825 |
. . . . . . . . . . . 12
β’ ((π + 1) β β0
β (π β ((π + 1) WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)))) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
β’ (π β β0
β (π β ((π + 1) WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)))) |
4 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(VtxβπΊ) =
(VtxβπΊ) |
5 | 4 | wwlkbp 28828 |
. . . . . . . . . . . . . . . 16
β’ (π β (WWalksβπΊ) β (πΊ β V β§ π β Word (VtxβπΊ))) |
6 | | lencl 14428 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word (VtxβπΊ) β (β―βπ) β
β0) |
7 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ) =
((π + 1) + 1) β
((π + 1) + 1) =
(β―βπ)) |
8 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ)
β β0 β (β―βπ) β β) |
9 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β0 β§ π β β0) β
(β―βπ) β
β) |
10 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β0 β§ π β β0) β 1 β
β) |
11 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π + 1) β β0
β (π + 1) β
β) |
12 | 1, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β (π + 1) β
β) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β0 β§ π β β0) β (π + 1) β
β) |
14 | | subadd2 11412 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((β―βπ)
β β β§ 1 β β β§ (π + 1) β β) β
(((β―βπ) β
1) = (π + 1) β ((π + 1) + 1) =
(β―βπ))) |
15 | 14 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β β§ 1 β β β§ (π + 1) β β) β (((π + 1) + 1) =
(β―βπ) β
((β―βπ) β
1) = (π +
1))) |
16 | 9, 10, 13, 15 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ)
β β0 β§ π β β0) β (((π + 1) + 1) =
(β―βπ) β
((β―βπ) β
1) = (π +
1))) |
17 | 7, 16 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β―βπ)
β β0 β§ π β β0) β
((β―βπ) =
((π + 1) + 1) β
((β―βπ) β
1) = (π +
1))) |
18 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ)
β 1) = (π + 1) β
(π + 1) =
((β―βπ) β
1)) |
19 | 18 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β―βπ)
β 1) = (π + 1) β
(π + 1) =
((β―βπ) β
1)) |
20 | 17, 19 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β―βπ)
β β0 β§ π β β0) β
((β―βπ) =
((π + 1) + 1) β (π + 1) = ((β―βπ) β 1))) |
21 | 20 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ)
β β0 β (π β β0 β
((β―βπ) =
((π + 1) + 1) β (π + 1) = ((β―βπ) β 1)))) |
22 | 21 | com23 86 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ)
β β0 β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π + 1) = ((β―βπ) β 1)))) |
23 | 6, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β Word (VtxβπΊ) β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π + 1) = ((β―βπ) β 1)))) |
24 | 5, 23 | simpl2im 505 |
. . . . . . . . . . . . . . 15
β’ (π β (WWalksβπΊ) β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π + 1) = ((β―βπ) β 1)))) |
25 | 24 | imp31 419 |
. . . . . . . . . . . . . 14
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π + 1) = ((β―βπ) β 1)) |
26 | 25 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π prefix (π + 1)) = (π prefix ((β―βπ) β 1))) |
27 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β π β (WWalksβπΊ)) |
28 | | nn0ge0 12445 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β 0 β€ π) |
29 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β 2 β β) |
31 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β) |
32 | 30, 31 | addge02d 11751 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (0 β€ π β 2
β€ (π +
2))) |
33 | 28, 32 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β 2 β€ (π +
2)) |
34 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β) |
35 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β 1 β β) |
36 | 34, 35, 35 | addassd 11184 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β ((π + 1) + 1) =
(π + (1 +
1))) |
37 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1 + 1) =
2 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (1 + 1) = 2) |
39 | 38 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (π + (1 + 1)) =
(π + 2)) |
40 | 36, 39 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β ((π + 1) + 1) =
(π + 2)) |
41 | 33, 40 | breqtrrd 5138 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β 2 β€ ((π + 1) +
1)) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β 2 β€
((π + 1) +
1)) |
43 | | breq2 5114 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ) =
((π + 1) + 1) β (2
β€ (β―βπ)
β 2 β€ ((π + 1) +
1))) |
44 | 43 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (2 β€
(β―βπ) β 2
β€ ((π + 1) +
1))) |
45 | 42, 44 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β 2 β€
(β―βπ)) |
46 | | wwlksm1edg 28868 |
. . . . . . . . . . . . . 14
β’ ((π β (WWalksβπΊ) β§ 2 β€
(β―βπ)) β
(π prefix
((β―βπ) β
1)) β (WWalksβπΊ)) |
47 | 27, 45, 46 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π prefix ((β―βπ) β 1)) β
(WWalksβπΊ)) |
48 | 26, 47 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π prefix (π + 1)) β (WWalksβπΊ)) |
49 | 48 | expcom 415 |
. . . . . . . . . . 11
β’ (π β β0
β ((π β
(WWalksβπΊ) β§
(β―βπ) = ((π + 1) + 1)) β (π prefix (π + 1)) β (WWalksβπΊ))) |
50 | 3, 49 | sylbid 239 |
. . . . . . . . . 10
β’ (π β β0
β (π β ((π + 1) WWalksN πΊ) β (π prefix (π + 1)) β (WWalksβπΊ))) |
51 | 50 | com12 32 |
. . . . . . . . 9
β’ (π β ((π + 1) WWalksN πΊ) β (π β β0 β (π prefix (π + 1)) β (WWalksβπΊ))) |
52 | 51 | adantr 482 |
. . . . . . . 8
β’ ((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β (π β β0 β (π prefix (π + 1)) β (WWalksβπΊ))) |
53 | 52 | imp 408 |
. . . . . . 7
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β (π prefix (π + 1)) β (WWalksβπΊ)) |
54 | | wwlksnextprop.e |
. . . . . . . . . . . 12
β’ πΈ = (EdgβπΊ) |
55 | 4, 54 | wwlknp 28830 |
. . . . . . . . . . 11
β’ (π β ((π + 1) WWalksN πΊ) β (π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) |
56 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β π β Word (VtxβπΊ)) |
57 | | peano2nn0 12460 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) β β0
β ((π + 1) + 1) β
β0) |
58 | 1, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β ((π + 1) + 1) β
β0) |
59 | | peano2re 11335 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (π + 1) β
β) |
60 | 31, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (π + 1) β
β) |
61 | 60 | lep1d 12093 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (π + 1) β€ ((π + 1) + 1)) |
62 | | elfz2nn0 13539 |
. . . . . . . . . . . . . . . . . 18
β’ ((π + 1) β (0...((π + 1) + 1)) β ((π + 1) β β0
β§ ((π + 1) + 1) β
β0 β§ (π + 1) β€ ((π + 1) + 1))) |
63 | 1, 58, 61, 62 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π + 1) β
(0...((π + 1) +
1))) |
64 | 63 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (π + 1) β
(0...((π + 1) +
1))) |
65 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
((π + 1) + 1) β
(0...(β―βπ)) =
(0...((π + 1) +
1))) |
66 | 65 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (0...(β―βπ)) = (0...((π + 1) + 1))) |
67 | 64, 66 | eleqtrrd 2841 |
. . . . . . . . . . . . . . 15
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (π + 1) β
(0...(β―βπ))) |
68 | 67 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π + 1) β
(0...(β―βπ))) |
69 | 56, 68 | jca 513 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)))) |
70 | 69 | ex 414 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))))) |
71 | 70 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))))) |
72 | 55, 71 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π + 1) WWalksN πΊ) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))))) |
73 | 72 | adantr 482 |
. . . . . . . . 9
β’ ((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))))) |
74 | 73 | imp 408 |
. . . . . . . 8
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)))) |
75 | | pfxlen 14578 |
. . . . . . . 8
β’ ((π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))) β (β―β(π prefix (π + 1))) = (π + 1)) |
76 | 74, 75 | syl 17 |
. . . . . . 7
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β
(β―β(π prefix
(π + 1))) = (π + 1)) |
77 | 53, 76 | jca 513 |
. . . . . 6
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β ((π prefix (π + 1)) β (WWalksβπΊ) β§ (β―β(π prefix (π + 1))) = (π + 1))) |
78 | | iswwlksn 28825 |
. . . . . . 7
β’ (π β β0
β ((π prefix (π + 1)) β (π WWalksN πΊ) β ((π prefix (π + 1)) β (WWalksβπΊ) β§ (β―β(π prefix (π + 1))) = (π + 1)))) |
79 | 78 | adantl 483 |
. . . . . 6
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β ((π prefix (π + 1)) β (π WWalksN πΊ) β ((π prefix (π + 1)) β (WWalksβπΊ) β§ (β―β(π prefix (π + 1))) = (π + 1)))) |
80 | 77, 79 | mpbird 257 |
. . . . 5
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β (π prefix (π + 1)) β (π WWalksN πΊ)) |
81 | 80 | exp31 421 |
. . . 4
β’ (π β ((π + 1) WWalksN πΊ) β ((πβ0) = π β (π β β0 β (π prefix (π + 1)) β (π WWalksN πΊ)))) |
82 | | wwlksnextprop.x |
. . . 4
β’ π = ((π + 1) WWalksN πΊ) |
83 | 81, 82 | eleq2s 2856 |
. . 3
β’ (π β π β ((πβ0) = π β (π β β0 β (π prefix (π + 1)) β (π WWalksN πΊ)))) |
84 | 83 | 3imp 1112 |
. 2
β’ ((π β π β§ (πβ0) = π β§ π β β0) β (π prefix (π + 1)) β (π WWalksN πΊ)) |
85 | 82 | wwlksnextproplem1 28896 |
. . . 4
β’ ((π β π β§ π β β0) β ((π prefix (π + 1))β0) = (πβ0)) |
86 | 85 | 3adant2 1132 |
. . 3
β’ ((π β π β§ (πβ0) = π β§ π β β0) β ((π prefix (π + 1))β0) = (πβ0)) |
87 | | simp2 1138 |
. . 3
β’ ((π β π β§ (πβ0) = π β§ π β β0) β (πβ0) = π) |
88 | 86, 87 | eqtrd 2777 |
. 2
β’ ((π β π β§ (πβ0) = π β§ π β β0) β ((π prefix (π + 1))β0) = π) |
89 | | fveq1 6846 |
. . . 4
β’ (π€ = (π prefix (π + 1)) β (π€β0) = ((π prefix (π + 1))β0)) |
90 | 89 | eqeq1d 2739 |
. . 3
β’ (π€ = (π prefix (π + 1)) β ((π€β0) = π β ((π prefix (π + 1))β0) = π)) |
91 | | wwlksnextprop.y |
. . 3
β’ π = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} |
92 | 90, 91 | elrab2 3653 |
. 2
β’ ((π prefix (π + 1)) β π β ((π prefix (π + 1)) β (π WWalksN πΊ) β§ ((π prefix (π + 1))β0) = π)) |
93 | 84, 88, 92 | sylanbrc 584 |
1
β’ ((π β π β§ (πβ0) = π β§ π β β0) β (π prefix (π + 1)) β π) |