Step | Hyp | Ref
| Expression |
1 | | uzuzle23 12821 |
. . . . 5
β’ (π β
(β€β₯β3) β π β
(β€β₯β2)) |
2 | | 2clwwlk.c |
. . . . . 6
β’ πΆ = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) |
3 | 2 | 2clwwlkel 29335 |
. . . . 5
β’ ((π β π β§ π β (β€β₯β2))
β (π β (ππΆπ) β (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π))) |
4 | 1, 3 | sylan2 594 |
. . . 4
β’ ((π β π β§ π β (β€β₯β3))
β (π β (ππΆπ) β (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π))) |
5 | | simpr 486 |
. . . . . . . . 9
β’ ((π β π β§ π β (β€β₯β3))
β π β
(β€β₯β3)) |
6 | 5 | anim1i 616 |
. . . . . . . 8
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β (π β (β€β₯β3)
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π))) |
7 | | 3anass 1096 |
. . . . . . . 8
β’ ((π β
(β€β₯β3) β§ π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π) β (π β (β€β₯β3)
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π))) |
8 | 6, 7 | sylibr 233 |
. . . . . . 7
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β (π β (β€β₯β3)
β§ π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) |
9 | | clwwnonrepclwwnon 29331 |
. . . . . . 7
β’ ((π β
(β€β₯β3) β§ π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π) β (π prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2))) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β (π prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2))) |
11 | 5 | adantr 482 |
. . . . . . 7
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β π β
(β€β₯β3)) |
12 | | simprl 770 |
. . . . . . 7
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β π β (π(ClWWalksNOnβπΊ)π)) |
13 | | simprr 772 |
. . . . . . . 8
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β (πβ(π β 2)) = π) |
14 | | isclwwlknon 29077 |
. . . . . . . . . 10
β’ (π β (π(ClWWalksNOnβπΊ)π) β (π β (π ClWWalksN πΊ) β§ (πβ0) = π)) |
15 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β (πβ0) = π) |
16 | 15 | eqcomd 2743 |
. . . . . . . . . 10
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β π = (πβ0)) |
17 | 14, 16 | sylbi 216 |
. . . . . . . . 9
β’ (π β (π(ClWWalksNOnβπΊ)π) β π = (πβ0)) |
18 | 17 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β π = (πβ0)) |
19 | 13, 18 | eqtrd 2777 |
. . . . . . 7
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β (πβ(π β 2)) = (πβ0)) |
20 | | 2clwwlk2clwwlklem 29332 |
. . . . . . 7
β’ ((π β
(β€β₯β3) β§ π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = (πβ0)) β (π substr β¨(π β 2), πβ©) β (π(ClWWalksNOnβπΊ)2)) |
21 | 11, 12, 19, 20 | syl3anc 1372 |
. . . . . 6
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β (π substr β¨(π β 2), πβ©) β (π(ClWWalksNOnβπΊ)2)) |
22 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(VtxβπΊ) =
(VtxβπΊ) |
23 | 22 | clwwlknbp 29021 |
. . . . . . . . . . . . 13
β’ (π β (π ClWWalksN πΊ) β (π β Word (VtxβπΊ) β§ (β―βπ) = π)) |
24 | | opeq2 4836 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (β―βπ) β β¨(π β 2), πβ© = β¨(π β 2), (β―βπ)β©) |
25 | 24 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π = (β―βπ) β (π substr β¨(π β 2), πβ©) = (π substr β¨(π β 2), (β―βπ)β©)) |
26 | 25 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = (β―βπ) β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = ((π prefix (π β 2)) ++ (π substr β¨(π β 2), (β―βπ)β©))) |
27 | 26 | eqcoms 2745 |
. . . . . . . . . . . . . . 15
β’
((β―βπ) =
π β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = ((π prefix (π β 2)) ++ (π substr β¨(π β 2), (β―βπ)β©))) |
28 | 27 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (π β π β§ π β (β€β₯β3)))
β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = ((π prefix (π β 2)) ++ (π substr β¨(π β 2), (β―βπ)β©))) |
29 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β π β Word (VtxβπΊ)) |
30 | | fz1ssfz0 13544 |
. . . . . . . . . . . . . . . . . . 19
β’
(1...π) β
(0...π) |
31 | | ige3m2fz 13472 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯β3) β (π β 2) β (1...π)) |
32 | 30, 31 | sselid 3947 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β3) β (π β 2) β (0...π)) |
33 | 32 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ π β (β€β₯β3))
β (π β 2) β
(0...π)) |
34 | 33 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (π β π β§ π β (β€β₯β3)))
β (π β 2) β
(0...π)) |
35 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ) =
π β
(0...(β―βπ)) =
(0...π)) |
36 | 35 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
π β ((π β 2) β
(0...(β―βπ))
β (π β 2) β
(0...π))) |
37 | 36 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (π β π β§ π β (β€β₯β3)))
β ((π β 2)
β (0...(β―βπ)) β (π β 2) β (0...π))) |
38 | 34, 37 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (π β π β§ π β (β€β₯β3)))
β (π β 2) β
(0...(β―βπ))) |
39 | | pfxcctswrd 14605 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ (π β 2) β (0...(β―βπ))) β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), (β―βπ)β©)) = π) |
40 | 29, 38, 39 | syl2an2r 684 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (π β π β§ π β (β€β₯β3)))
β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), (β―βπ)β©)) = π) |
41 | 28, 40 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (π β π β§ π β (β€β₯β3)))
β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = π) |
42 | 23, 41 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β (π ClWWalksN πΊ) β§ (π β π β§ π β (β€β₯β3)))
β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = π) |
43 | 42 | ex 414 |
. . . . . . . . . . 11
β’ (π β (π ClWWalksN πΊ) β ((π β π β§ π β (β€β₯β3))
β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = π)) |
44 | 43 | adantr 482 |
. . . . . . . . . 10
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β ((π β π β§ π β (β€β₯β3))
β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = π)) |
45 | 14, 44 | sylbi 216 |
. . . . . . . . 9
β’ (π β (π(ClWWalksNOnβπΊ)π) β ((π β π β§ π β (β€β₯β3))
β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = π)) |
46 | 45 | adantr 482 |
. . . . . . . 8
β’ ((π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π) β ((π β π β§ π β (β€β₯β3))
β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = π)) |
47 | 46 | impcom 409 |
. . . . . . 7
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)) = π) |
48 | 47 | eqcomd 2743 |
. . . . . 6
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β π = ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©))) |
49 | 10, 21, 48 | 3jca 1129 |
. . . . 5
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π)) β ((π prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2)) β§ (π substr β¨(π β 2), πβ©) β (π(ClWWalksNOnβπΊ)2) β§ π = ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©)))) |
50 | 49 | ex 414 |
. . . 4
β’ ((π β π β§ π β (β€β₯β3))
β ((π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π) β ((π prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2)) β§ (π substr β¨(π β 2), πβ©) β (π(ClWWalksNOnβπΊ)2) β§ π = ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©))))) |
51 | 4, 50 | sylbid 239 |
. . 3
β’ ((π β π β§ π β (β€β₯β3))
β (π β (ππΆπ) β ((π prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2)) β§ (π substr β¨(π β 2), πβ©) β (π(ClWWalksNOnβπΊ)2) β§ π = ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©))))) |
52 | | rspceov 7409 |
. . 3
β’ (((π prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2)) β§ (π substr β¨(π β 2), πβ©) β (π(ClWWalksNOnβπΊ)2) β§ π = ((π prefix (π β 2)) ++ (π substr β¨(π β 2), πβ©))) β βπ β (π(ClWWalksNOnβπΊ)(π β 2))βπ β (π(ClWWalksNOnβπΊ)2)π = (π ++ π)) |
53 | 51, 52 | syl6 35 |
. 2
β’ ((π β π β§ π β (β€β₯β3))
β (π β (ππΆπ) β βπ β (π(ClWWalksNOnβπΊ)(π β 2))βπ β (π(ClWWalksNOnβπΊ)2)π = (π ++ π))) |
54 | | eluzelcn 12782 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β3) β π β β) |
55 | | 2cnd 12238 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β3) β 2 β β) |
56 | 54, 55 | npcand 11523 |
. . . . . . . . . 10
β’ (π β
(β€β₯β3) β ((π β 2) + 2) = π) |
57 | 56 | adantl 483 |
. . . . . . . . 9
β’ ((π β π β§ π β (β€β₯β3))
β ((π β 2) + 2)
= π) |
58 | 57 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯β3))
β (π(ClWWalksNOnβπΊ)((π β 2) + 2)) = (π(ClWWalksNOnβπΊ)π)) |
59 | 58 | eleq2d 2824 |
. . . . . . 7
β’ ((π β π β§ π β (β€β₯β3))
β ((π ++ π) β (π(ClWWalksNOnβπΊ)((π β 2) + 2)) β (π ++ π) β (π(ClWWalksNOnβπΊ)π))) |
60 | 59 | biimpd 228 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯β3))
β ((π ++ π) β (π(ClWWalksNOnβπΊ)((π β 2) + 2)) β (π ++ π) β (π(ClWWalksNOnβπΊ)π))) |
61 | | clwwlknonccat 29082 |
. . . . . 6
β’ ((π β (π(ClWWalksNOnβπΊ)(π β 2)) β§ π β (π(ClWWalksNOnβπΊ)2)) β (π ++ π) β (π(ClWWalksNOnβπΊ)((π β 2) + 2))) |
62 | 60, 61 | impel 507 |
. . . . 5
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)(π β 2)) β§ π β (π(ClWWalksNOnβπΊ)2))) β (π ++ π) β (π(ClWWalksNOnβπΊ)π)) |
63 | | isclwwlknon 29077 |
. . . . . . . 8
β’ (π β (π(ClWWalksNOnβπΊ)2) β (π β (2 ClWWalksN πΊ) β§ (πβ0) = π)) |
64 | | clwwlkn2 29030 |
. . . . . . . . . 10
β’ (π β (2 ClWWalksN πΊ) β ((β―βπ) = 2 β§ π β Word (VtxβπΊ) β§ {(πβ0), (πβ1)} β (EdgβπΊ))) |
65 | | isclwwlknon 29077 |
. . . . . . . . . . . . 13
β’ (π β (π(ClWWalksNOnβπΊ)(π β 2)) β (π β ((π β 2) ClWWalksN πΊ) β§ (πβ0) = π)) |
66 | 22 | clwwlknbp 29021 |
. . . . . . . . . . . . . . 15
β’ (π β ((π β 2) ClWWalksN πΊ) β (π β Word (VtxβπΊ) β§ (β―βπ) = (π β 2))) |
67 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β π β Word (VtxβπΊ)) |
68 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β π β Word (VtxβπΊ)) |
69 | | 2nn 12233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 2 β
β |
70 | | lbfzo0 13619 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (0 β
(0..^2) β 2 β β) |
71 | 69, 70 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β
(0..^2) |
72 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ) =
2 β (0..^(β―βπ)) = (0..^2)) |
73 | 71, 72 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ) =
2 β 0 β (0..^(β―βπ))) |
74 | 73 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β 0 β
(0..^(β―βπ))) |
75 | 67, 68, 74 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β (π β Word (VtxβπΊ) β§ π β Word (VtxβπΊ) β§ 0 β (0..^(β―βπ)))) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β (π β Word (VtxβπΊ) β§ π β Word (VtxβπΊ) β§ 0 β (0..^(β―βπ)))) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β§ (π β π β§ π β (β€β₯β3)))
β (π β Word
(VtxβπΊ) β§ π β Word (VtxβπΊ) β§ 0 β
(0..^(β―βπ)))) |
78 | | ccatval3 14474 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Word (VtxβπΊ) β§ π β Word (VtxβπΊ) β§ 0 β (0..^(β―βπ))) β ((π ++ π)β(0 + (β―βπ))) = (πβ0)) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β§ (π β π β§ π β (β€β₯β3)))
β ((π ++ π)β(0 +
(β―βπ))) =
(πβ0)) |
80 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πβ0) = π β§ (β―βπ) = (π β 2)) β (β―βπ) = (π β 2)) |
81 | 80 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβ0) = π β§ (β―βπ) = (π β 2)) β (0 +
(β―βπ)) = (0 +
(π β
2))) |
82 | 81 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β (0 +
(β―βπ)) = (0 +
(π β
2))) |
83 | 54, 55 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
(β€β₯β3) β (π β 2) β β) |
84 | 83 | addid2d 11363 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯β3) β (0 + (π β 2)) = (π β 2)) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π β§ π β (β€β₯β3))
β (0 + (π β 2))
= (π β
2)) |
86 | 82, 85 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β§ (π β π β§ π β (β€β₯β3)))
β (0 + (β―βπ)) = (π β 2)) |
87 | 86 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β§ (π β π β§ π β (β€β₯β3)))
β (π β 2) = (0 +
(β―βπ))) |
88 | 87 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β§ (π β π β§ π β (β€β₯β3)))
β ((π ++ π)β(π β 2)) = ((π ++ π)β(0 + (β―βπ)))) |
89 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβ0) = π β§ (β―βπ) = (π β 2)) β (πβ0) = π) |
90 | 89 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβ0) = π β§ (β―βπ) = (π β 2)) β π = (πβ0)) |
91 | 90 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β§ (π β π β§ π β (β€β₯β3)))
β π = (πβ0)) |
92 | 79, 88, 91 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Word (VtxβπΊ) β§ ((β―βπ) = 2 β§ π β Word (VtxβπΊ))) β§ ((πβ0) = π β§ (β―βπ) = (π β 2))) β§ (π β π β§ π β (β€β₯β3)))
β ((π ++ π)β(π β 2)) = π) |
93 | 92 | exp53 449 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word (VtxβπΊ) β (((β―βπ) = 2 β§ π β Word (VtxβπΊ)) β ((πβ0) = π β ((β―βπ) = (π β 2) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π))))) |
94 | 93 | com24 95 |
. . . . . . . . . . . . . . . 16
β’ (π β Word (VtxβπΊ) β ((β―βπ) = (π β 2) β ((πβ0) = π β (((β―βπ) = 2 β§ π β Word (VtxβπΊ)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π))))) |
95 | 94 | imp 408 |
. . . . . . . . . . . . . . 15
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = (π β 2)) β ((πβ0) = π β (((β―βπ) = 2 β§ π β Word (VtxβπΊ)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π)))) |
96 | 66, 95 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((π β 2) ClWWalksN πΊ) β ((πβ0) = π β (((β―βπ) = 2 β§ π β Word (VtxβπΊ)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π)))) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β ((π β 2) ClWWalksN πΊ) β§ (πβ0) = π) β ((πβ0) = π β (((β―βπ) = 2 β§ π β Word (VtxβπΊ)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π)))) |
98 | 65, 97 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((πβ0) = π β (((β―βπ) = 2 β§ π β Word (VtxβπΊ)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π)))) |
99 | 98 | com13 88 |
. . . . . . . . . . 11
β’
(((β―βπ)
= 2 β§ π β Word
(VtxβπΊ)) β
((πβ0) = π β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π)))) |
100 | 99 | 3adant3 1133 |
. . . . . . . . . 10
β’
(((β―βπ)
= 2 β§ π β Word
(VtxβπΊ) β§ {(πβ0), (πβ1)} β (EdgβπΊ)) β ((πβ0) = π β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π)))) |
101 | 64, 100 | sylbi 216 |
. . . . . . . . 9
β’ (π β (2 ClWWalksN πΊ) β ((πβ0) = π β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π)))) |
102 | 101 | imp 408 |
. . . . . . . 8
β’ ((π β (2 ClWWalksN πΊ) β§ (πβ0) = π) β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π))) |
103 | 63, 102 | sylbi 216 |
. . . . . . 7
β’ (π β (π(ClWWalksNOnβπΊ)2) β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π))) |
104 | 103 | impcom 409 |
. . . . . 6
β’ ((π β (π(ClWWalksNOnβπΊ)(π β 2)) β§ π β (π(ClWWalksNOnβπΊ)2)) β ((π β π β§ π β (β€β₯β3))
β ((π ++ π)β(π β 2)) = π)) |
105 | 104 | impcom 409 |
. . . . 5
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)(π β 2)) β§ π β (π(ClWWalksNOnβπΊ)2))) β ((π ++ π)β(π β 2)) = π) |
106 | 2 | 2clwwlkel 29335 |
. . . . . . 7
β’ ((π β π β§ π β (β€β₯β2))
β ((π ++ π) β (ππΆπ) β ((π ++ π) β (π(ClWWalksNOnβπΊ)π) β§ ((π ++ π)β(π β 2)) = π))) |
107 | 1, 106 | sylan2 594 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯β3))
β ((π ++ π) β (ππΆπ) β ((π ++ π) β (π(ClWWalksNOnβπΊ)π) β§ ((π ++ π)β(π β 2)) = π))) |
108 | 107 | adantr 482 |
. . . . 5
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)(π β 2)) β§ π β (π(ClWWalksNOnβπΊ)2))) β ((π ++ π) β (ππΆπ) β ((π ++ π) β (π(ClWWalksNOnβπΊ)π) β§ ((π ++ π)β(π β 2)) = π))) |
109 | 62, 105, 108 | mpbir2and 712 |
. . . 4
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)(π β 2)) β§ π β (π(ClWWalksNOnβπΊ)2))) β (π ++ π) β (ππΆπ)) |
110 | | eleq1 2826 |
. . . 4
β’ (π = (π ++ π) β (π β (ππΆπ) β (π ++ π) β (ππΆπ))) |
111 | 109, 110 | syl5ibrcom 247 |
. . 3
β’ (((π β π β§ π β (β€β₯β3))
β§ (π β (π(ClWWalksNOnβπΊ)(π β 2)) β§ π β (π(ClWWalksNOnβπΊ)2))) β (π = (π ++ π) β π β (ππΆπ))) |
112 | 111 | rexlimdvva 3206 |
. 2
β’ ((π β π β§ π β (β€β₯β3))
β (βπ β
(π(ClWWalksNOnβπΊ)(π β 2))βπ β (π(ClWWalksNOnβπΊ)2)π = (π ++ π) β π β (ππΆπ))) |
113 | 53, 112 | impbid 211 |
1
β’ ((π β π β§ π β (β€β₯β3))
β (π β (ππΆπ) β βπ β (π(ClWWalksNOnβπΊ)(π β 2))βπ β (π(ClWWalksNOnβπΊ)2)π = (π ++ π))) |