Step | Hyp | Ref
| Expression |
1 | | elfzoelz 13632 |
. . . . . . . . 9
β’ (π β
(1..^(β―βπ))
β π β
β€) |
2 | | cshwlen 14749 |
. . . . . . . . 9
β’ ((π β Word π β§ π β β€) β
(β―β(π cyclShift
π)) = (β―βπ)) |
3 | 1, 2 | sylan2 594 |
. . . . . . . 8
β’ ((π β Word π β§ π β (1..^(β―βπ))) β (β―β(π cyclShift π)) = (β―βπ)) |
4 | 3 | oveq1d 7424 |
. . . . . . 7
β’ ((π β Word π β§ π β (1..^(β―βπ))) β
((β―β(π
cyclShift π)) β 1) =
((β―βπ) β
1)) |
5 | 4 | oveq2d 7425 |
. . . . . 6
β’ ((π β Word π β§ π β (1..^(β―βπ))) β
(0..^((β―β(π
cyclShift π)) β 1)) =
(0..^((β―βπ)
β 1))) |
6 | 5 | eleq2d 2820 |
. . . . 5
β’ ((π β Word π β§ π β (1..^(β―βπ))) β (π β (0..^((β―β(π cyclShift π)) β 1)) β π β (0..^((β―βπ) β 1)))) |
7 | 6 | adantr 482 |
. . . 4
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β (π β (0..^((β―β(π cyclShift π)) β 1)) β π β (0..^((β―βπ) β 1)))) |
8 | | simpll 766 |
. . . . . . . . 9
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ π β (0..^((β―βπ) β 1))) β π β Word π) |
9 | 1 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ π β (0..^((β―βπ) β 1))) β π β
β€) |
10 | | lencl 14483 |
. . . . . . . . . . . . 13
β’ (π β Word π β (β―βπ) β
β0) |
11 | | nn0z 12583 |
. . . . . . . . . . . . . . 15
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
12 | | peano2zm 12605 |
. . . . . . . . . . . . . . 15
β’
((β―βπ)
β β€ β ((β―βπ) β 1) β
β€) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
β’
((β―βπ)
β β0 β ((β―βπ) β 1) β
β€) |
14 | | nn0re 12481 |
. . . . . . . . . . . . . . 15
β’
((β―βπ)
β β0 β (β―βπ) β β) |
15 | 14 | lem1d 12147 |
. . . . . . . . . . . . . 14
β’
((β―βπ)
β β0 β ((β―βπ) β 1) β€ (β―βπ)) |
16 | | eluz2 12828 |
. . . . . . . . . . . . . 14
β’
((β―βπ)
β (β€β₯β((β―βπ) β 1)) β (((β―βπ) β 1) β β€
β§ (β―βπ)
β β€ β§ ((β―βπ) β 1) β€ (β―βπ))) |
17 | 13, 11, 15, 16 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β0 β (β―βπ) β
(β€β₯β((β―βπ) β 1))) |
18 | 10, 17 | syl 17 |
. . . . . . . . . . . 12
β’ (π β Word π β (β―βπ) β
(β€β₯β((β―βπ) β 1))) |
19 | 18 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β Word π β§ π β (1..^(β―βπ))) β (β―βπ) β
(β€β₯β((β―βπ) β 1))) |
20 | | fzoss2 13660 |
. . . . . . . . . . 11
β’
((β―βπ)
β (β€β₯β((β―βπ) β 1)) β
(0..^((β―βπ)
β 1)) β (0..^(β―βπ))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
β’ ((π β Word π β§ π β (1..^(β―βπ))) β
(0..^((β―βπ)
β 1)) β (0..^(β―βπ))) |
22 | 21 | sselda 3983 |
. . . . . . . . 9
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ π β (0..^((β―βπ) β 1))) β π β
(0..^(β―βπ))) |
23 | | cshwidxmod 14753 |
. . . . . . . . 9
β’ ((π β Word π β§ π β β€ β§ π β (0..^(β―βπ))) β ((π cyclShift π)βπ) = (πβ((π + π) mod (β―βπ)))) |
24 | 8, 9, 22, 23 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ π β (0..^((β―βπ) β 1))) β ((π cyclShift π)βπ) = (πβ((π + π) mod (β―βπ)))) |
25 | | elfzo1 13682 |
. . . . . . . . . . . 12
β’ (π β
(1..^(β―βπ))
β (π β β
β§ (β―βπ)
β β β§ π <
(β―βπ))) |
26 | 25 | simp2bi 1147 |
. . . . . . . . . . 11
β’ (π β
(1..^(β―βπ))
β (β―βπ)
β β) |
27 | 26 | adantl 483 |
. . . . . . . . . 10
β’ ((π β Word π β§ π β (1..^(β―βπ))) β (β―βπ) β
β) |
28 | | elfzom1p1elfzo 13712 |
. . . . . . . . . 10
β’
(((β―βπ)
β β β§ π
β (0..^((β―βπ) β 1))) β (π + 1) β (0..^(β―βπ))) |
29 | 27, 28 | sylan 581 |
. . . . . . . . 9
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ π β (0..^((β―βπ) β 1))) β (π + 1) β
(0..^(β―βπ))) |
30 | | cshwidxmod 14753 |
. . . . . . . . 9
β’ ((π β Word π β§ π β β€ β§ (π + 1) β (0..^(β―βπ))) β ((π cyclShift π)β(π + 1)) = (πβ(((π + 1) + π) mod (β―βπ)))) |
31 | 8, 9, 29, 30 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ π β (0..^((β―βπ) β 1))) β ((π cyclShift π)β(π + 1)) = (πβ(((π + 1) + π) mod (β―βπ)))) |
32 | 24, 31 | preq12d 4746 |
. . . . . . 7
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ π β (0..^((β―βπ) β 1))) β {((π cyclShift π)βπ), ((π cyclShift π)β(π + 1))} = {(πβ((π + π) mod (β―βπ))), (πβ(((π + 1) + π) mod (β―βπ)))}) |
33 | 32 | adantlr 714 |
. . . . . 6
β’ ((((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ π β (0..^((β―βπ) β 1))) β {((π cyclShift π)βπ), ((π cyclShift π)β(π + 1))} = {(πβ((π + π) mod (β―βπ))), (πβ(((π + 1) + π) mod (β―βπ)))}) |
34 | | 2z 12594 |
. . . . . . . . . . 11
β’ 2 β
β€ |
35 | 34 | a1i 11 |
. . . . . . . . . 10
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β 2
β β€) |
36 | | nnz 12579 |
. . . . . . . . . . 11
β’
((β―βπ)
β β β (β―βπ) β β€) |
37 | 36 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β
(β―βπ) β
β€) |
38 | | nnnn0 12479 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β β (β―βπ) β
β0) |
39 | 38 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β
(β―βπ) β
β0) |
40 | | nnne0 12246 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β β (β―βπ) β 0) |
41 | 40 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β
(β―βπ) β
0) |
42 | | 1red 11215 |
. . . . . . . . . . . 12
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β 1
β β) |
43 | | nnre 12219 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
44 | 43 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β
π β
β) |
45 | | nnre 12219 |
. . . . . . . . . . . . . 14
β’
((β―βπ)
β β β (β―βπ) β β) |
46 | 45 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β
(β―βπ) β
β) |
47 | | nnge1 12240 |
. . . . . . . . . . . . . 14
β’ (π β β β 1 β€
π) |
48 | 47 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β 1
β€ π) |
49 | | simp3 1139 |
. . . . . . . . . . . . 13
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β
π < (β―βπ)) |
50 | 42, 44, 46, 48, 49 | lelttrd 11372 |
. . . . . . . . . . . 12
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β 1
< (β―βπ)) |
51 | 42, 50 | gtned 11349 |
. . . . . . . . . . 11
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β
(β―βπ) β
1) |
52 | | nn0n0n1ge2 12539 |
. . . . . . . . . . 11
β’
(((β―βπ)
β β0 β§ (β―βπ) β 0 β§ (β―βπ) β 1) β 2 β€
(β―βπ)) |
53 | 39, 41, 51, 52 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β 2
β€ (β―βπ)) |
54 | | eluz2 12828 |
. . . . . . . . . 10
β’
((β―βπ)
β (β€β₯β2) β (2 β β€ β§
(β―βπ) β
β€ β§ 2 β€ (β―βπ))) |
55 | 35, 37, 53, 54 | syl3anbrc 1344 |
. . . . . . . . 9
β’ ((π β β β§
(β―βπ) β
β β§ π <
(β―βπ)) β
(β―βπ) β
(β€β₯β2)) |
56 | 25, 55 | sylbi 216 |
. . . . . . . 8
β’ (π β
(1..^(β―βπ))
β (β―βπ)
β (β€β₯β2)) |
57 | 56 | ad3antlr 730 |
. . . . . . 7
β’ ((((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ π β (0..^((β―βπ) β 1))) β
(β―βπ) β
(β€β₯β2)) |
58 | | elfzoelz 13632 |
. . . . . . . 8
β’ (π β
(0..^((β―βπ)
β 1)) β π β
β€) |
59 | 58 | adantl 483 |
. . . . . . 7
β’ ((((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ π β (0..^((β―βπ) β 1))) β π β
β€) |
60 | 1 | ad3antlr 730 |
. . . . . . 7
β’ ((((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ π β (0..^((β―βπ) β 1))) β π β
β€) |
61 | | simplrl 776 |
. . . . . . 7
β’ ((((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ π β (0..^((β―βπ) β 1))) β
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ) |
62 | | lsw 14514 |
. . . . . . . . . . . . . 14
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ π β (1..^(β―βπ))) β (lastSβπ) = (πβ((β―βπ) β 1))) |
64 | 63 | preq1d 4744 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ π β (1..^(β―βπ))) β {(lastSβπ), (πβ0)} = {(πβ((β―βπ) β 1)), (πβ0)}) |
65 | 64 | eleq1d 2819 |
. . . . . . . . . . 11
β’ ((π β Word π β§ π β (1..^(β―βπ))) β ({(lastSβπ), (πβ0)} β πΈ β {(πβ((β―βπ) β 1)), (πβ0)} β πΈ)) |
66 | 65 | biimpcd 248 |
. . . . . . . . . 10
β’
({(lastSβπ),
(πβ0)} β πΈ β ((π β Word π β§ π β (1..^(β―βπ))) β {(πβ((β―βπ) β 1)), (πβ0)} β πΈ)) |
67 | 66 | adantl 483 |
. . . . . . . . 9
β’
((βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β ((π β Word π β§ π β (1..^(β―βπ))) β {(πβ((β―βπ) β 1)), (πβ0)} β πΈ)) |
68 | 67 | impcom 409 |
. . . . . . . 8
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β {(πβ((β―βπ) β 1)), (πβ0)} β πΈ) |
69 | 68 | adantr 482 |
. . . . . . 7
β’ ((((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ π β (0..^((β―βπ) β 1))) β {(πβ((β―βπ) β 1)), (πβ0)} β πΈ) |
70 | | clwwisshclwwslemlem 29266 |
. . . . . . 7
β’
((((β―βπ)
β (β€β₯β2) β§ π β β€ β§ π β β€) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β πΈ) β {(πβ((π + π) mod (β―βπ))), (πβ(((π + 1) + π) mod (β―βπ)))} β πΈ) |
71 | 57, 59, 60, 61, 69, 70 | syl311anc 1385 |
. . . . . 6
β’ ((((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ π β (0..^((β―βπ) β 1))) β {(πβ((π + π) mod (β―βπ))), (πβ(((π + 1) + π) mod (β―βπ)))} β πΈ) |
72 | 33, 71 | eqeltrd 2834 |
. . . . 5
β’ ((((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ π β (0..^((β―βπ) β 1))) β {((π cyclShift π)βπ), ((π cyclShift π)β(π + 1))} β πΈ) |
73 | 72 | ex 414 |
. . . 4
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β (π β (0..^((β―βπ) β 1)) β {((π cyclShift π)βπ), ((π cyclShift π)β(π + 1))} β πΈ)) |
74 | 7, 73 | sylbid 239 |
. . 3
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β (π β (0..^((β―β(π cyclShift π)) β 1)) β {((π cyclShift π)βπ), ((π cyclShift π)β(π + 1))} β πΈ)) |
75 | 74 | ralrimiv 3146 |
. 2
β’ (((π β Word π β§ π β (1..^(β―βπ))) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β βπ β (0..^((β―β(π cyclShift π)) β 1)){((π cyclShift π)βπ), ((π cyclShift π)β(π + 1))} β πΈ) |
76 | 75 | ex 414 |
1
β’ ((π β Word π β§ π β (1..^(β―βπ))) β ((βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β βπ β (0..^((β―β(π cyclShift π)) β 1)){((π cyclShift π)βπ), ((π cyclShift π)β(π + 1))} β πΈ)) |