Step | Hyp | Ref
| Expression |
1 | | eldifi 4126 |
. . . . . 6
β’ (πΉ β (Word β β
{β
}) β πΉ β
Word β) |
2 | | s1cl 14557 |
. . . . . 6
β’ (πΎ β β β
β¨βπΎββ©
β Word β) |
3 | | ccatcl 14529 |
. . . . . 6
β’ ((πΉ β Word β β§
β¨βπΎββ©
β Word β) β (πΉ ++ β¨βπΎββ©) β Word
β) |
4 | 1, 2, 3 | syl2an 595 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (πΉ ++
β¨βπΎββ©) β Word
β) |
5 | | signsv.p |
. . . . . 6
⒠⨣ =
(π β {-1, 0, 1}, π β {-1, 0, 1} β¦
if(π = 0, π, π)) |
6 | | signsv.w |
. . . . . 6
β’ π = {β¨(Baseβndx), {-1,
0, 1}β©, β¨(+gβndx), ⨣
β©} |
7 | | signsv.t |
. . . . . 6
β’ π = (π β Word β β¦ (π β
(0..^(β―βπ))
β¦ (π
Ξ£g (π β (0...π) β¦ (sgnβ(πβπ)))))) |
8 | | signsv.v |
. . . . . 6
β’ π = (π β Word β β¦ Ξ£π β
(1..^(β―βπ))if(((πβπ)βπ) β ((πβπ)β(π β 1)), 1, 0)) |
9 | 5, 6, 7, 8 | signsvvfval 33888 |
. . . . 5
β’ ((πΉ ++ β¨βπΎββ©) β Word
β β (πβ(πΉ ++ β¨βπΎββ©)) = Ξ£π β (1..^(β―β(πΉ ++ β¨βπΎββ©)))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0)) |
10 | 4, 9 | syl 17 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (πβ(πΉ ++ β¨βπΎββ©)) = Ξ£π β (1..^(β―β(πΉ ++ β¨βπΎββ©)))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0)) |
11 | | ccatlen 14530 |
. . . . . . . 8
β’ ((πΉ β Word β β§
β¨βπΎββ©
β Word β) β (β―β(πΉ ++ β¨βπΎββ©)) = ((β―βπΉ) +
(β―ββ¨βπΎββ©))) |
12 | 1, 2, 11 | syl2an 595 |
. . . . . . 7
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (β―β(πΉ ++ β¨βπΎββ©)) = ((β―βπΉ) +
(β―ββ¨βπΎββ©))) |
13 | | s1len 14561 |
. . . . . . . 8
β’
(β―ββ¨βπΎββ©) = 1 |
14 | 13 | oveq2i 7423 |
. . . . . . 7
β’
((β―βπΉ) +
(β―ββ¨βπΎββ©)) = ((β―βπΉ) + 1) |
15 | 12, 14 | eqtrdi 2787 |
. . . . . 6
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (β―β(πΉ ++ β¨βπΎββ©)) = ((β―βπΉ) + 1)) |
16 | 15 | oveq2d 7428 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (1..^(β―β(πΉ ++ β¨βπΎββ©))) =
(1..^((β―βπΉ) +
1))) |
17 | 16 | sumeq1d 15652 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β Ξ£π
β (1..^(β―β(πΉ ++ β¨βπΎββ©)))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = Ξ£π β
(1..^((β―βπΉ) +
1))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0)) |
18 | | eldifsn 4790 |
. . . . . . . 8
β’ (πΉ β (Word β β
{β
}) β (πΉ β
Word β β§ πΉ β
β
)) |
19 | | lennncl 14489 |
. . . . . . . 8
β’ ((πΉ β Word β β§ πΉ β β
) β
(β―βπΉ) β
β) |
20 | 18, 19 | sylbi 216 |
. . . . . . 7
β’ (πΉ β (Word β β
{β
}) β (β―βπΉ) β β) |
21 | | nnuz 12870 |
. . . . . . 7
β’ β =
(β€β₯β1) |
22 | 20, 21 | eleqtrdi 2842 |
. . . . . 6
β’ (πΉ β (Word β β
{β
}) β (β―βπΉ) β
(β€β₯β1)) |
23 | 22 | adantr 480 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (β―βπΉ) β
(β€β₯β1)) |
24 | | 1cnd 11214 |
. . . . . 6
β’ ((((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1...(β―βπΉ)))
β§ ((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1))) β 1 β
β) |
25 | | 0cnd 11212 |
. . . . . 6
β’ ((((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1...(β―βπΉ)))
β§ Β¬ ((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1))) β 0 β
β) |
26 | 24, 25 | ifclda 4563 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1...(β―βπΉ)))
β if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) β
β) |
27 | | fveq2 6891 |
. . . . . . 7
β’ (π = (β―βπΉ) β ((πβ(πΉ ++ β¨βπΎββ©))βπ) = ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ))) |
28 | | fvoveq1 7435 |
. . . . . . 7
β’ (π = (β―βπΉ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) = ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1))) |
29 | 27, 28 | neeq12d 3001 |
. . . . . 6
β’ (π = (β―βπΉ) β (((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)))) |
30 | 29 | ifbid 4551 |
. . . . 5
β’ (π = (β―βπΉ) β if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1,
0)) |
31 | 23, 26, 30 | fzosump1 15703 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β Ξ£π
β (1..^((β―βπΉ) + 1))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = (Ξ£π β
(1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) + if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1,
0))) |
32 | 10, 17, 31 | 3eqtrd 2775 |
. . 3
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (πβ(πΉ ++ β¨βπΎββ©)) = (Ξ£π β (1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) + if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1,
0))) |
33 | 32 | adantlr 712 |
. 2
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (πβ(πΉ ++ β¨βπΎββ©)) = (Ξ£π β (1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) + if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1,
0))) |
34 | | simpl 482 |
. . . . . . . . . . 11
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β πΉ β
(Word β β {β
})) |
35 | 34 | eldifad 3960 |
. . . . . . . . . 10
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β πΉ β
Word β) |
36 | 35 | adantr 480 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β πΉ β Word
β) |
37 | | simplr 766 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β πΎ β
β) |
38 | | fzo0ss1 13667 |
. . . . . . . . . . 11
β’
(1..^(β―βπΉ)) β (0..^(β―βπΉ)) |
39 | 38 | a1i 11 |
. . . . . . . . . 10
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (1..^(β―βπΉ)) β (0..^(β―βπΉ))) |
40 | 39 | sselda 3982 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β π β
(0..^(β―βπΉ))) |
41 | 5, 6, 7, 8 | signstfvp 33881 |
. . . . . . . . 9
β’ ((πΉ β Word β β§ πΎ β β β§ π β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ β¨βπΎββ©))βπ) = ((πβπΉ)βπ)) |
42 | 36, 37, 40, 41 | syl3anc 1370 |
. . . . . . . 8
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β ((πβ(πΉ ++ β¨βπΎββ©))βπ) = ((πβπΉ)βπ)) |
43 | | elfzoel2 13636 |
. . . . . . . . . . . . 13
β’ (π β
(1..^(β―βπΉ))
β (β―βπΉ)
β β€) |
44 | 43 | adantl 481 |
. . . . . . . . . . . 12
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (β―βπΉ)
β β€) |
45 | | 1nn0 12493 |
. . . . . . . . . . . 12
β’ 1 β
β0 |
46 | | eluzmn 12834 |
. . . . . . . . . . . 12
β’
(((β―βπΉ)
β β€ β§ 1 β β0) β (β―βπΉ) β
(β€β₯β((β―βπΉ) β 1))) |
47 | 44, 45, 46 | sylancl 585 |
. . . . . . . . . . 11
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (β―βπΉ)
β (β€β₯β((β―βπΉ) β 1))) |
48 | | fzoss2 13665 |
. . . . . . . . . . 11
β’
((β―βπΉ)
β (β€β₯β((β―βπΉ) β 1)) β
(0..^((β―βπΉ)
β 1)) β (0..^(β―βπΉ))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (0..^((β―βπΉ) β 1)) β
(0..^(β―βπΉ))) |
50 | | elfzo1elm1fzo0 13738 |
. . . . . . . . . . 11
β’ (π β
(1..^(β―βπΉ))
β (π β 1) β
(0..^((β―βπΉ)
β 1))) |
51 | 50 | adantl 481 |
. . . . . . . . . 10
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (π β 1) β
(0..^((β―βπΉ)
β 1))) |
52 | 49, 51 | sseldd 3983 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (π β 1) β
(0..^(β―βπΉ))) |
53 | 5, 6, 7, 8 | signstfvp 33881 |
. . . . . . . . 9
β’ ((πΉ β Word β β§ πΎ β β β§ (π β 1) β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) = ((πβπΉ)β(π β 1))) |
54 | 36, 37, 52, 53 | syl3anc 1370 |
. . . . . . . 8
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) = ((πβπΉ)β(π β 1))) |
55 | 42, 54 | neeq12d 3001 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) β ((πβπΉ)βπ) β ((πβπΉ)β(π β 1)))) |
56 | 55 | ifbid 4551 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = if(((πβπΉ)βπ) β ((πβπΉ)β(π β 1)), 1, 0)) |
57 | 56 | sumeq2dv 15654 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β Ξ£π
β (1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = Ξ£π β
(1..^(β―βπΉ))if(((πβπΉ)βπ) β ((πβπΉ)β(π β 1)), 1, 0)) |
58 | 5, 6, 7, 8 | signsvvfval 33888 |
. . . . . 6
β’ (πΉ β Word β β
(πβπΉ) = Ξ£π β (1..^(β―βπΉ))if(((πβπΉ)βπ) β ((πβπΉ)β(π β 1)), 1, 0)) |
59 | 35, 58 | syl 17 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (πβπΉ) = Ξ£π β (1..^(β―βπΉ))if(((πβπΉ)βπ) β ((πβπΉ)β(π β 1)), 1, 0)) |
60 | 57, 59 | eqtr4d 2774 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β Ξ£π
β (1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = (πβπΉ)) |
61 | 60 | adantlr 712 |
. . 3
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β Ξ£π β
(1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = (πβπΉ)) |
62 | 5, 6, 7, 8 | signstfvn 33879 |
. . . . . . 7
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) = (((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ))) |
63 | 62 | adantlr 712 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) = (((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ))) |
64 | 35 | adantlr 712 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β πΉ β Word β) |
65 | | simpr 484 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β πΎ β β) |
66 | | fzo0end 13729 |
. . . . . . . . 9
β’
((β―βπΉ)
β β β ((β―βπΉ) β 1) β
(0..^(β―βπΉ))) |
67 | 20, 66 | syl 17 |
. . . . . . . 8
β’ (πΉ β (Word β β
{β
}) β ((β―βπΉ) β 1) β
(0..^(β―βπΉ))) |
68 | 67 | ad2antrr 723 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β
((β―βπΉ) β
1) β (0..^(β―βπΉ))) |
69 | 5, 6, 7, 8 | signstfvp 33881 |
. . . . . . 7
β’ ((πΉ β Word β β§ πΎ β β β§
((β―βπΉ) β
1) β (0..^(β―βπΉ))) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)) = ((πβπΉ)β((β―βπΉ) β 1))) |
70 | 64, 65, 68, 69 | syl3anc 1370 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)) = ((πβπΉ)β((β―βπΉ) β 1))) |
71 | 63, 70 | neeq12d 3001 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)) β (((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ)) β ((πβπΉ)β((β―βπΉ) β 1)))) |
72 | 5, 6, 7, 8 | signstfvcl 33883 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§
((β―βπΉ) β
1) β (0..^(β―βπΉ))) β ((πβπΉ)β((β―βπΉ) β 1)) β {-1,
1}) |
73 | 68, 72 | syldan 590 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((πβπΉ)β((β―βπΉ) β 1)) β {-1,
1}) |
74 | | rexr 11265 |
. . . . . . . 8
β’ (πΎ β β β πΎ β
β*) |
75 | | sgncl 33836 |
. . . . . . . 8
β’ (πΎ β β*
β (sgnβπΎ) β
{-1, 0, 1}) |
76 | 74, 75 | syl 17 |
. . . . . . 7
β’ (πΎ β β β
(sgnβπΎ) β {-1,
0, 1}) |
77 | 76 | adantl 481 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (sgnβπΎ) β {-1, 0,
1}) |
78 | 5, 6 | signswch 33871 |
. . . . . 6
β’ ((((πβπΉ)β((β―βπΉ) β 1)) β {-1, 1} β§
(sgnβπΎ) β {-1,
0, 1}) β ((((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ)) β ((πβπΉ)β((β―βπΉ) β 1)) β (((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0)) |
79 | 73, 77, 78 | syl2anc 583 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ)) β ((πβπΉ)β((β―βπΉ) β 1)) β (((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0)) |
80 | 65 | rexrd 11269 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β πΎ β
β*) |
81 | | sgnsgn 33846 |
. . . . . . . . 9
β’ (πΎ β β*
β (sgnβ(sgnβπΎ)) = (sgnβπΎ)) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β
(sgnβ(sgnβπΎ)) =
(sgnβπΎ)) |
83 | 82 | oveq2d 7428 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβ(sgnβπΎ)))
= ((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β· (sgnβπΎ))) |
84 | 83 | breq1d 5158 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβ(sgnβπΎ)))
< 0 β ((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β· (sgnβπΎ)) < 0)) |
85 | | neg1rr 12332 |
. . . . . . . . 9
β’ -1 β
β |
86 | | 1re 11219 |
. . . . . . . . 9
β’ 1 β
β |
87 | | prssi 4824 |
. . . . . . . . 9
β’ ((-1
β β β§ 1 β β) β {-1, 1} β
β) |
88 | 85, 86, 87 | mp2an 689 |
. . . . . . . 8
β’ {-1, 1}
β β |
89 | 88, 73 | sselid 3980 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((πβπΉ)β((β―βπΉ) β 1)) β
β) |
90 | | sgnclre 33837 |
. . . . . . . 8
β’ (πΎ β β β
(sgnβπΎ) β
β) |
91 | 90 | adantl 481 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (sgnβπΎ) β
β) |
92 | | sgnmulsgn 33847 |
. . . . . . 7
β’ ((((πβπΉ)β((β―βπΉ) β 1)) β β β§
(sgnβπΎ) β
β) β ((((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0 β
((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβ(sgnβπΎ)))
< 0)) |
93 | 89, 91, 92 | syl2anc 583 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0 β
((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβ(sgnβπΎ)))
< 0)) |
94 | | sgnmulsgn 33847 |
. . . . . . 7
β’ ((((πβπΉ)β((β―βπΉ) β 1)) β β β§ πΎ β β) β
((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0 β
((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβπΎ)) <
0)) |
95 | 89, 94 | sylancom 587 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0 β ((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β· (sgnβπΎ)) < 0)) |
96 | 84, 93, 95 | 3bitr4d 311 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0 β (((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0)) |
97 | 71, 79, 96 | 3bitrd 305 |
. . . 4
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)) β (((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0)) |
98 | 97 | ifbid 4551 |
. . 3
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1, 0) =
if((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0, 1,
0)) |
99 | 61, 98 | oveq12d 7430 |
. 2
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (Ξ£π β
(1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) + if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1, 0)) = ((πβπΉ) + if((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0, 1, 0))) |
100 | 33, 99 | eqtrd 2771 |
1
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (πβ(πΉ ++ β¨βπΎββ©)) = ((πβπΉ) + if((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0, 1, 0))) |