Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12518 |
. . . . . . . . . . . 12
β’ (π β β0
β (π + 1) β
β0) |
2 | | iswwlksn 29357 |
. . . . . . . . . . . 12
β’ ((π + 1) β β0
β (π β ((π + 1) WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)))) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
β’ (π β β0
β (π β ((π + 1) WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)))) |
4 | | eqid 2730 |
. . . . . . . . . . . . . . . . 17
β’
(VtxβπΊ) =
(VtxβπΊ) |
5 | 4 | wwlkbp 29360 |
. . . . . . . . . . . . . . . 16
β’ (π β (WWalksβπΊ) β (πΊ β V β§ π β Word (VtxβπΊ))) |
6 | | lencl 14489 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word (VtxβπΊ) β (β―βπ) β
β0) |
7 | | eqcom 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ) =
((π + 1) + 1) β
((π + 1) + 1) =
(β―βπ)) |
8 | | nn0cn 12488 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ)
β β0 β (β―βπ) β β) |
9 | 8 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β0 β§ π β β0) β
(β―βπ) β
β) |
10 | | 1cnd 11215 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β0 β§ π β β0) β 1 β
β) |
11 | | nn0cn 12488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π + 1) β β0
β (π + 1) β
β) |
12 | 1, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β (π + 1) β
β) |
13 | 12 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β0 β§ π β β0) β (π + 1) β
β) |
14 | | subadd2 11470 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((β―βπ)
β β β§ 1 β β β§ (π + 1) β β) β
(((β―βπ) β
1) = (π + 1) β ((π + 1) + 1) =
(β―βπ))) |
15 | 14 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ)
β β β§ 1 β β β§ (π + 1) β β) β (((π + 1) + 1) =
(β―βπ) β
((β―βπ) β
1) = (π +
1))) |
16 | 9, 10, 13, 15 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ)
β β0 β§ π β β0) β (((π + 1) + 1) =
(β―βπ) β
((β―βπ) β
1) = (π +
1))) |
17 | 7, 16 | bitrid 282 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β―βπ)
β β0 β§ π β β0) β
((β―βπ) =
((π + 1) + 1) β
((β―βπ) β
1) = (π +
1))) |
18 | | eqcom 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ)
β 1) = (π + 1) β
(π + 1) =
((β―βπ) β
1)) |
19 | 18 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β―βπ)
β 1) = (π + 1) β
(π + 1) =
((β―βπ) β
1)) |
20 | 17, 19 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β―βπ)
β β0 β§ π β β0) β
((β―βπ) =
((π + 1) + 1) β (π + 1) = ((β―βπ) β 1))) |
21 | 20 | ex 411 |
. . . . . . . . . . . . . . . . . 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 502 |
. . . . . . . . . . . . . . 15
β’ (π β (WWalksβπΊ) β ((β―βπ) = ((π + 1) + 1) β (π β β0 β (π + 1) = ((β―βπ) β 1)))) |
25 | 24 | imp31 416 |
. . . . . . . . . . . . . 14
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π + 1) = ((β―βπ) β 1)) |
26 | 25 | oveq2d 7429 |
. . . . . . . . . . . . 13
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π prefix (π + 1)) = (π prefix ((β―βπ) β 1))) |
27 | | simpll 763 |
. . . . . . . . . . . . . 14
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β π β (WWalksβπΊ)) |
28 | | nn0ge0 12503 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β 0 β€ π) |
29 | | 2re 12292 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β 2 β β) |
31 | | nn0re 12487 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β) |
32 | 30, 31 | addge02d 11809 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (0 β€ π β 2
β€ (π +
2))) |
33 | 28, 32 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β 2 β€ (π +
2)) |
34 | | nn0cn 12488 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β) |
35 | | 1cnd 11215 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β 1 β β) |
36 | 34, 35, 35 | addassd 11242 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β ((π + 1) + 1) =
(π + (1 +
1))) |
37 | | 1p1e2 12343 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1 + 1) =
2 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (1 + 1) = 2) |
39 | 38 | oveq2d 7429 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (π + (1 + 1)) =
(π + 2)) |
40 | 36, 39 | eqtrd 2770 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β ((π + 1) + 1) =
(π + 2)) |
41 | 33, 40 | breqtrrd 5177 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β 2 β€ ((π + 1) +
1)) |
42 | 41 | adantl 480 |
. . . . . . . . . . . . . . 15
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β 2 β€
((π + 1) +
1)) |
43 | | breq2 5153 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ) =
((π + 1) + 1) β (2
β€ (β―βπ)
β 2 β€ ((π + 1) +
1))) |
44 | 43 | ad2antlr 723 |
. . . . . . . . . . . . . . 15
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (2 β€
(β―βπ) β 2
β€ ((π + 1) +
1))) |
45 | 42, 44 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β 2 β€
(β―βπ)) |
46 | | wwlksm1edg 29400 |
. . . . . . . . . . . . . 14
β’ ((π β (WWalksβπΊ) β§ 2 β€
(β―βπ)) β
(π prefix
((β―βπ) β
1)) β (WWalksβπΊ)) |
47 | 27, 45, 46 | syl2anc 582 |
. . . . . . . . . . . . 13
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π prefix ((β―βπ) β 1)) β
(WWalksβπΊ)) |
48 | 26, 47 | eqeltrd 2831 |
. . . . . . . . . . . 12
β’ (((π β (WWalksβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π prefix (π + 1)) β (WWalksβπΊ)) |
49 | 48 | expcom 412 |
. . . . . . . . . . 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 479 |
. . . . . . . 8
β’ ((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β (π β β0 β (π prefix (π + 1)) β (WWalksβπΊ))) |
53 | 52 | imp 405 |
. . . . . . 7
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β (π prefix (π + 1)) β (WWalksβπΊ)) |
54 | | wwlksnextprop.e |
. . . . . . . . . . . 12
β’ πΈ = (EdgβπΊ) |
55 | 4, 54 | wwlknp 29362 |
. . . . . . . . . . 11
β’ (π β ((π + 1) WWalksN πΊ) β (π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) |
56 | | simpll 763 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β π β Word (VtxβπΊ)) |
57 | | peano2nn0 12518 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) β β0
β ((π + 1) + 1) β
β0) |
58 | 1, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β ((π + 1) + 1) β
β0) |
59 | | peano2re 11393 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (π + 1) β
β) |
60 | 31, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (π + 1) β
β) |
61 | 60 | lep1d 12151 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (π + 1) β€ ((π + 1) + 1)) |
62 | | elfz2nn0 13598 |
. . . . . . . . . . . . . . . . . 18
β’ ((π + 1) β (0...((π + 1) + 1)) β ((π + 1) β β0
β§ ((π + 1) + 1) β
β0 β§ (π + 1) β€ ((π + 1) + 1))) |
63 | 1, 58, 61, 62 | syl3anbrc 1341 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π + 1) β
(0...((π + 1) +
1))) |
64 | 63 | adantl 480 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (π + 1) β
(0...((π + 1) +
1))) |
65 | | oveq2 7421 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
((π + 1) + 1) β
(0...(β―βπ)) =
(0...((π + 1) +
1))) |
66 | 65 | adantr 479 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (0...(β―βπ)) = (0...((π + 1) + 1))) |
67 | 64, 66 | eleqtrrd 2834 |
. . . . . . . . . . . . . . 15
β’
(((β―βπ)
= ((π + 1) + 1) β§ π β β0)
β (π + 1) β
(0...(β―βπ))) |
68 | 67 | adantll 710 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π + 1) β
(0...(β―βπ))) |
69 | 56, 68 | jca 510 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β§ π β β0) β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)))) |
70 | 69 | ex 411 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = ((π + 1) + 1)) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))))) |
71 | 70 | 3adant3 1130 |
. . . . . . . . . . 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 479 |
. . . . . . . . 9
β’ ((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β (π β β0 β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ))))) |
74 | 73 | imp 405 |
. . . . . . . 8
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β (π β Word (VtxβπΊ) β§ (π + 1) β (0...(β―βπ)))) |
75 | | pfxlen 14639 |
. . . . . . . 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 510 |
. . . . . 6
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β ((π prefix (π + 1)) β (WWalksβπΊ) β§ (β―β(π prefix (π + 1))) = (π + 1))) |
78 | | iswwlksn 29357 |
. . . . . . 7
β’ (π β β0
β ((π prefix (π + 1)) β (π WWalksN πΊ) β ((π prefix (π + 1)) β (WWalksβπΊ) β§ (β―β(π prefix (π + 1))) = (π + 1)))) |
79 | 78 | adantl 480 |
. . . . . 6
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β ((π prefix (π + 1)) β (π WWalksN πΊ) β ((π prefix (π + 1)) β (WWalksβπΊ) β§ (β―β(π prefix (π + 1))) = (π + 1)))) |
80 | 77, 79 | mpbird 256 |
. . . . 5
β’ (((π β ((π + 1) WWalksN πΊ) β§ (πβ0) = π) β§ π β β0) β (π prefix (π + 1)) β (π WWalksN πΊ)) |
81 | 80 | exp31 418 |
. . . 4
β’ (π β ((π + 1) WWalksN πΊ) β ((πβ0) = π β (π β β0 β (π prefix (π + 1)) β (π WWalksN πΊ)))) |
82 | | wwlksnextprop.x |
. . . 4
β’ π = ((π + 1) WWalksN πΊ) |
83 | 81, 82 | eleq2s 2849 |
. . 3
β’ (π β π β ((πβ0) = π β (π β β0 β (π prefix (π + 1)) β (π WWalksN πΊ)))) |
84 | 83 | 3imp 1109 |
. 2
β’ ((π β π β§ (πβ0) = π β§ π β β0) β (π prefix (π + 1)) β (π WWalksN πΊ)) |
85 | 82 | wwlksnextproplem1 29428 |
. . . 4
β’ ((π β π β§ π β β0) β ((π prefix (π + 1))β0) = (πβ0)) |
86 | 85 | 3adant2 1129 |
. . 3
β’ ((π β π β§ (πβ0) = π β§ π β β0) β ((π prefix (π + 1))β0) = (πβ0)) |
87 | | simp2 1135 |
. . 3
β’ ((π β π β§ (πβ0) = π β§ π β β0) β (πβ0) = π) |
88 | 86, 87 | eqtrd 2770 |
. 2
β’ ((π β π β§ (πβ0) = π β§ π β β0) β ((π prefix (π + 1))β0) = π) |
89 | | fveq1 6891 |
. . . 4
β’ (π€ = (π prefix (π + 1)) β (π€β0) = ((π prefix (π + 1))β0)) |
90 | 89 | eqeq1d 2732 |
. . 3
β’ (π€ = (π prefix (π + 1)) β ((π€β0) = π β ((π prefix (π + 1))β0) = π)) |
91 | | wwlksnextprop.y |
. . 3
β’ π = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} |
92 | 90, 91 | elrab2 3687 |
. 2
β’ ((π prefix (π + 1)) β π β ((π prefix (π + 1)) β (π WWalksN πΊ) β§ ((π prefix (π + 1))β0) = π)) |
93 | 84, 88, 92 | sylanbrc 581 |
1
β’ ((π β π β§ (πβ0) = π β§ π β β0) β (π prefix (π + 1)) β π) |