Step | Hyp | Ref
| Expression |
1 | | uz3m2nn 12875 |
. . . . . . . 8
β’ (π β
(β€β₯β3) β (π β 2) β β) |
2 | 1 | nnne0d 12262 |
. . . . . . 7
β’ (π β
(β€β₯β3) β (π β 2) β 0) |
3 | 2 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β (π β 2) β
0) |
4 | | clwwlknonex2.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
5 | | clwwlknonex2.e |
. . . . . . 7
β’ πΈ = (EdgβπΊ) |
6 | 4, 5 | clwwlknonel 29348 |
. . . . . 6
β’ ((π β 2) β 0 β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
7 | 3, 6 | syl 17 |
. . . . 5
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
8 | | simpr11 1258 |
. . . . . . . . . 10
β’ (((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β π β Word π) |
9 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β π β Word π) |
10 | | simpll1 1213 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β π β π) |
11 | | simpll2 1214 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β π β π) |
12 | | ccatw2s1cl 14574 |
. . . . . . . . 9
β’ ((π β Word π β§ π β π β§ π β π) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π) |
13 | 9, 10, 11, 12 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π) |
14 | 4, 5 | clwwlknonex2lem2 29361 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β βπ β ((0..^((β―βπ) β 1)) βͺ
{((β―βπ) β
1), (β―βπ)}){(((π ++ β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ) |
15 | | simp11 1204 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β π β Word π) |
16 | 15 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β π β Word π) |
17 | | ccatw2s1len 14575 |
. . . . . . . . . . . . . 14
β’ (π β Word π β (β―β((π ++ β¨βπββ©) ++ β¨βπββ©)) =
((β―βπ) +
2)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (β―β((π ++ β¨βπββ©) ++ β¨βπββ©)) =
((β―βπ) +
2)) |
19 | 18 | oveq1d 7424 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β ((β―β((π ++ β¨βπββ©) ++ β¨βπββ©)) β 1) =
(((β―βπ) + 2)
β 1)) |
20 | 19 | oveq2d 7425 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (0..^((β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) β 1)) =
(0..^(((β―βπ) +
2) β 1))) |
21 | | simp3 1139 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β π β
(β€β₯β3)) |
22 | | simp2 1138 |
. . . . . . . . . . . . . 14
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β (β―βπ) = (π β 2)) |
23 | 21, 22 | anim12i 614 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β (π β (β€β₯β3)
β§ (β―βπ) =
(π β
2))) |
24 | 23 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (π β (β€β₯β3)
β§ (β―βπ) =
(π β
2))) |
25 | | clwwlknonex2lem1 29360 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β3) β§ (β―βπ) = (π β 2)) β
(0..^(((β―βπ) +
2) β 1)) = ((0..^((β―βπ) β 1)) βͺ {((β―βπ) β 1),
(β―βπ)})) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (0..^(((β―βπ) + 2) β 1)) =
((0..^((β―βπ)
β 1)) βͺ {((β―βπ) β 1), (β―βπ)})) |
27 | 20, 26 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (0..^((β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) β 1)) =
((0..^((β―βπ)
β 1)) βͺ {((β―βπ) β 1), (β―βπ)})) |
28 | 27 | raleqdv 3326 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (βπ β (0..^((β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) β 1)){(((π ++ β¨βπββ©) ++
β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β βπ β ((0..^((β―βπ) β 1)) βͺ
{((β―βπ) β
1), (β―βπ)}){(((π ++ β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ)) |
29 | 14, 28 | mpbird 257 |
. . . . . . . 8
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β βπ β (0..^((β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) β 1)){(((π ++ β¨βπββ©) ++
β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ) |
30 | | ccatws1cl 14566 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ π β π) β (π ++ β¨βπββ©) β Word π) |
31 | | lswccats1 14584 |
. . . . . . . . . . . 12
β’ (((π ++ β¨βπββ©) β Word π β§ π β π) β (lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)) = π) |
32 | 30, 31 | stoic3 1779 |
. . . . . . . . . . 11
β’ ((π β Word π β§ π β π β§ π β π) β (lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)) = π) |
33 | 16, 10, 11, 32 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)) = π) |
34 | 1 | nngt0d 12261 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β3) β 0 < (π β 2)) |
35 | | breq2 5153 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
(π β 2) β (0
< (β―βπ)
β 0 < (π β
2))) |
36 | 34, 35 | imbitrrid 245 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ) =
(π β 2) β (π β
(β€β₯β3) β 0 < (β―βπ))) |
37 | 36 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β (π β (β€β₯β3)
β 0 < (β―βπ))) |
38 | 37 | com12 32 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β3) β (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β 0 < (β―βπ))) |
39 | 38 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β (((π β Word
π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β 0 < (β―βπ))) |
40 | 39 | imp 408 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β 0 < (β―βπ)) |
41 | 40 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β 0 < (β―βπ)) |
42 | | ccat2s1fst 14589 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 0 < (β―βπ)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)β0) = (πβ0)) |
43 | 16, 41, 42 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (((π ++ β¨βπββ©) ++ β¨βπββ©)β0) = (πβ0)) |
44 | 33, 43 | preq12d 4746 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} = {π, (πβ0)}) |
45 | | prcom 4737 |
. . . . . . . . . . . . 13
β’ {π, π} = {π, π} |
46 | 45 | eleq1i 2825 |
. . . . . . . . . . . 12
β’ ({π, π} β πΈ β {π, π} β πΈ) |
47 | 46 | biimpi 215 |
. . . . . . . . . . 11
β’ ({π, π} β πΈ β {π, π} β πΈ) |
48 | 47 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β {π, π} β πΈ) |
49 | | preq2 4739 |
. . . . . . . . . . . . 13
β’ ((πβ0) = π β {π, (πβ0)} = {π, π}) |
50 | 49 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ ((πβ0) = π β ({π, (πβ0)} β πΈ β {π, π} β πΈ)) |
51 | 50 | 3ad2ant3 1136 |
. . . . . . . . . . 11
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β ({π, (πβ0)} β πΈ β {π, π} β πΈ)) |
52 | 51 | ad2antlr 726 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β ({π, (πβ0)} β πΈ β {π, π} β πΈ)) |
53 | 48, 52 | mpbird 257 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β {π, (πβ0)} β πΈ) |
54 | 44, 53 | eqeltrd 2834 |
. . . . . . . 8
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) |
55 | 13, 29, 54 | 3jca 1129 |
. . . . . . 7
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ)) |
56 | 17 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β (β―β((π ++ β¨βπββ©) ++ β¨βπββ©)) =
((β―βπ) +
2)) |
57 | 56 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β (β―β((π ++ β¨βπββ©) ++ β¨βπββ©)) =
((β―βπ) +
2)) |
58 | 57 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (β―β((π ++ β¨βπββ©) ++ β¨βπββ©)) =
((β―βπ) +
2)) |
59 | | oveq1 7416 |
. . . . . . . . . . . . . . 15
β’
((β―βπ) =
(π β 2) β
((β―βπ) + 2) =
((π β 2) +
2)) |
60 | | eluzelcn 12834 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β3) β π β β) |
61 | | 2cn 12287 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
62 | | npcan 11469 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ 2 β
β) β ((π β
2) + 2) = π) |
63 | 60, 61, 62 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β3) β ((π β 2) + 2) = π) |
64 | 59, 63 | sylan9eq 2793 |
. . . . . . . . . . . . . 14
β’
(((β―βπ)
= (π β 2) β§ π β
(β€β₯β3)) β ((β―βπ) + 2) = π) |
65 | 64 | ex 414 |
. . . . . . . . . . . . 13
β’
((β―βπ) =
(π β 2) β (π β
(β€β₯β3) β ((β―βπ) + 2) = π)) |
66 | 65 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β (π β (β€β₯β3)
β ((β―βπ) +
2) = π)) |
67 | 66 | com12 32 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β3) β (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β ((β―βπ) + 2) = π)) |
68 | 67 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β (((π β Word
π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β ((β―βπ) + 2) = π)) |
69 | 68 | imp 408 |
. . . . . . . . 9
β’ (((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β ((β―βπ) + 2) = π) |
70 | 69 | adantr 482 |
. . . . . . . 8
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β ((β―βπ) + 2) = π) |
71 | 58, 70 | eqtrd 2773 |
. . . . . . 7
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β (β―β((π ++ β¨βπββ©) ++ β¨βπββ©)) = π) |
72 | 55, 71 | jca 513 |
. . . . . 6
β’ ((((π β π β§ π β π β§ π β (β€β₯β3))
β§ ((π β Word π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π)) |
73 | 72 | exp31 421 |
. . . . 5
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β (((π β Word
π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β ({π, π} β πΈ β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π)))) |
74 | 7, 73 | sylbid 239 |
. . . 4
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ({π, π} β πΈ β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π)))) |
75 | 74 | com23 86 |
. . 3
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β ({π, π} β πΈ β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π)))) |
76 | 75 | 3imp 1112 |
. 2
β’ (((π β π β§ π β π β§ π β (β€β₯β3))
β§ {π, π} β πΈ β§ π β (π(ClWWalksNOnβπΊ)(π β 2))) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π)) |
77 | | eluzge3nn 12874 |
. . . . 5
β’ (π β
(β€β₯β3) β π β β) |
78 | 4, 5 | isclwwlknx 29289 |
. . . . 5
β’ (π β β β (((π ++ β¨βπββ©) ++
β¨βπββ©) β (π ClWWalksN πΊ) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π))) |
79 | 77, 78 | syl 17 |
. . . 4
β’ (π β
(β€β₯β3) β (((π ++ β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π))) |
80 | 79 | 3ad2ant3 1136 |
. . 3
β’ ((π β π β§ π β π β§ π β (β€β₯β3))
β (((π ++
β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π))) |
81 | 80 | 3ad2ant1 1134 |
. 2
β’ (((π β π β§ π β π β§ π β (β€β₯β3))
β§ {π, π} β πΈ β§ π β (π(ClWWalksNOnβπΊ)(π β 2))) β (((π ++ β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) β Word π β§ βπ β
(0..^((β―β((π ++
β¨βπββ©) ++ β¨βπββ©)) β
1)){(((π ++
β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ β§ {(lastSβ((π ++ β¨βπββ©) ++ β¨βπββ©)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β0)} β πΈ) β§ (β―β((π ++ β¨βπββ©) ++
β¨βπββ©)) = π))) |
82 | 76, 81 | mpbird 257 |
1
β’ (((π β π β§ π β π β§ π β (β€β₯β3))
β§ {π, π} β πΈ β§ π β (π(ClWWalksNOnβπΊ)(π β 2))) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ)) |