Step | Hyp | Ref
| Expression |
1 | | eldifi 4125 |
. . . . . 6
β’ (πΉ β (Word β β
{β
}) β πΉ β
Word β) |
2 | | s1cl 14556 |
. . . . . 6
β’ (πΎ β β β
β¨βπΎββ©
β Word β) |
3 | | ccatcl 14528 |
. . . . . 6
β’ ((πΉ β Word β β§
β¨βπΎββ©
β Word β) β (πΉ ++ β¨βπΎββ©) β Word
β) |
4 | 1, 2, 3 | syl2an 594 |
. . . . 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 33887 |
. . . . 5
β’ ((πΉ ++ β¨βπΎββ©) β Word
β β (πβ(πΉ ++ β¨βπΎββ©)) = Ξ£π β (1..^(β―β(πΉ ++ β¨βπΎββ©)))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0)) |
10 | 4, 9 | syl 17 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (πβ(πΉ ++ β¨βπΎββ©)) = Ξ£π β (1..^(β―β(πΉ ++ β¨βπΎββ©)))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0)) |
11 | | ccatlen 14529 |
. . . . . . . 8
β’ ((πΉ β Word β β§
β¨βπΎββ©
β Word β) β (β―β(πΉ ++ β¨βπΎββ©)) = ((β―βπΉ) +
(β―ββ¨βπΎββ©))) |
12 | 1, 2, 11 | syl2an 594 |
. . . . . . 7
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (β―β(πΉ ++ β¨βπΎββ©)) = ((β―βπΉ) +
(β―ββ¨βπΎββ©))) |
13 | | s1len 14560 |
. . . . . . . 8
β’
(β―ββ¨βπΎββ©) = 1 |
14 | 13 | oveq2i 7422 |
. . . . . . 7
β’
((β―βπΉ) +
(β―ββ¨βπΎββ©)) = ((β―βπΉ) + 1) |
15 | 12, 14 | eqtrdi 2786 |
. . . . . 6
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (β―β(πΉ ++ β¨βπΎββ©)) = ((β―βπΉ) + 1)) |
16 | 15 | oveq2d 7427 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (1..^(β―β(πΉ ++ β¨βπΎββ©))) =
(1..^((β―βπΉ) +
1))) |
17 | 16 | sumeq1d 15651 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β Ξ£π
β (1..^(β―β(πΉ ++ β¨βπΎββ©)))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = Ξ£π β
(1..^((β―βπΉ) +
1))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0)) |
18 | | eldifsn 4789 |
. . . . . . . 8
β’ (πΉ β (Word β β
{β
}) β (πΉ β
Word β β§ πΉ β
β
)) |
19 | | lennncl 14488 |
. . . . . . . 8
β’ ((πΉ β Word β β§ πΉ β β
) β
(β―βπΉ) β
β) |
20 | 18, 19 | sylbi 216 |
. . . . . . 7
β’ (πΉ β (Word β β
{β
}) β (β―βπΉ) β β) |
21 | | nnuz 12869 |
. . . . . . 7
β’ β =
(β€β₯β1) |
22 | 20, 21 | eleqtrdi 2841 |
. . . . . 6
β’ (πΉ β (Word β β
{β
}) β (β―βπΉ) β
(β€β₯β1)) |
23 | 22 | adantr 479 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (β―βπΉ) β
(β€β₯β1)) |
24 | | 1cnd 11213 |
. . . . . 6
β’ ((((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1...(β―βπΉ)))
β§ ((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1))) β 1 β
β) |
25 | | 0cnd 11211 |
. . . . . 6
β’ ((((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1...(β―βπΉ)))
β§ Β¬ ((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1))) β 0 β
β) |
26 | 24, 25 | ifclda 4562 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1...(β―βπΉ)))
β if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) β
β) |
27 | | fveq2 6890 |
. . . . . . 7
β’ (π = (β―βπΉ) β ((πβ(πΉ ++ β¨βπΎββ©))βπ) = ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ))) |
28 | | fvoveq1 7434 |
. . . . . . 7
β’ (π = (β―βπΉ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) = ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1))) |
29 | 27, 28 | neeq12d 3000 |
. . . . . 6
β’ (π = (β―βπΉ) β (((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)))) |
30 | 29 | ifbid 4550 |
. . . . 5
β’ (π = (β―βπΉ) β if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1,
0)) |
31 | 23, 26, 30 | fzosump1 15702 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β Ξ£π
β (1..^((β―βπΉ) + 1))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = (Ξ£π β
(1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) + if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1,
0))) |
32 | 10, 17, 31 | 3eqtrd 2774 |
. . 3
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (πβ(πΉ ++ β¨βπΎββ©)) = (Ξ£π β (1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) + if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1,
0))) |
33 | 32 | adantlr 711 |
. 2
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (πβ(πΉ ++ β¨βπΎββ©)) = (Ξ£π β (1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) + if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1,
0))) |
34 | | simpl 481 |
. . . . . . . . . . 11
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β πΉ β
(Word β β {β
})) |
35 | 34 | eldifad 3959 |
. . . . . . . . . 10
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β πΉ β
Word β) |
36 | 35 | adantr 479 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β πΉ β Word
β) |
37 | | simplr 765 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β πΎ β
β) |
38 | | fzo0ss1 13666 |
. . . . . . . . . . 11
β’
(1..^(β―βπΉ)) β (0..^(β―βπΉ)) |
39 | 38 | a1i 11 |
. . . . . . . . . 10
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (1..^(β―βπΉ)) β (0..^(β―βπΉ))) |
40 | 39 | sselda 3981 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β π β
(0..^(β―βπΉ))) |
41 | 5, 6, 7, 8 | signstfvp 33880 |
. . . . . . . . 9
β’ ((πΉ β Word β β§ πΎ β β β§ π β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ β¨βπΎββ©))βπ) = ((πβπΉ)βπ)) |
42 | 36, 37, 40, 41 | syl3anc 1369 |
. . . . . . . 8
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β ((πβ(πΉ ++ β¨βπΎββ©))βπ) = ((πβπΉ)βπ)) |
43 | | elfzoel2 13635 |
. . . . . . . . . . . . 13
β’ (π β
(1..^(β―βπΉ))
β (β―βπΉ)
β β€) |
44 | 43 | adantl 480 |
. . . . . . . . . . . 12
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (β―βπΉ)
β β€) |
45 | | 1nn0 12492 |
. . . . . . . . . . . 12
β’ 1 β
β0 |
46 | | eluzmn 12833 |
. . . . . . . . . . . 12
β’
(((β―βπΉ)
β β€ β§ 1 β β0) β (β―βπΉ) β
(β€β₯β((β―βπΉ) β 1))) |
47 | 44, 45, 46 | sylancl 584 |
. . . . . . . . . . 11
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (β―βπΉ)
β (β€β₯β((β―βπΉ) β 1))) |
48 | | fzoss2 13664 |
. . . . . . . . . . 11
β’
((β―βπΉ)
β (β€β₯β((β―βπΉ) β 1)) β
(0..^((β―βπΉ)
β 1)) β (0..^(β―βπΉ))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (0..^((β―βπΉ) β 1)) β
(0..^(β―βπΉ))) |
50 | | elfzo1elm1fzo0 13737 |
. . . . . . . . . . 11
β’ (π β
(1..^(β―βπΉ))
β (π β 1) β
(0..^((β―βπΉ)
β 1))) |
51 | 50 | adantl 480 |
. . . . . . . . . 10
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (π β 1) β
(0..^((β―βπΉ)
β 1))) |
52 | 49, 51 | sseldd 3982 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (π β 1) β
(0..^(β―βπΉ))) |
53 | 5, 6, 7, 8 | signstfvp 33880 |
. . . . . . . . 9
β’ ((πΉ β Word β β§ πΎ β β β§ (π β 1) β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) = ((πβπΉ)β(π β 1))) |
54 | 36, 37, 52, 53 | syl3anc 1369 |
. . . . . . . 8
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) = ((πβπΉ)β(π β 1))) |
55 | 42, 54 | neeq12d 3000 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β (((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)) β ((πβπΉ)βπ) β ((πβπΉ)β(π β 1)))) |
56 | 55 | ifbid 4550 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(1..^(β―βπΉ)))
β if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = if(((πβπΉ)βπ) β ((πβπΉ)β(π β 1)), 1, 0)) |
57 | 56 | sumeq2dv 15653 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β Ξ£π
β (1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = Ξ£π β
(1..^(β―βπΉ))if(((πβπΉ)βπ) β ((πβπΉ)β(π β 1)), 1, 0)) |
58 | 5, 6, 7, 8 | signsvvfval 33887 |
. . . . . 6
β’ (πΉ β Word β β
(πβπΉ) = Ξ£π β (1..^(β―βπΉ))if(((πβπΉ)βπ) β ((πβπΉ)β(π β 1)), 1, 0)) |
59 | 35, 58 | syl 17 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (πβπΉ) = Ξ£π β (1..^(β―βπΉ))if(((πβπΉ)βπ) β ((πβπΉ)β(π β 1)), 1, 0)) |
60 | 57, 59 | eqtr4d 2773 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β Ξ£π
β (1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = (πβπΉ)) |
61 | 60 | adantlr 711 |
. . 3
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β Ξ£π β
(1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) = (πβπΉ)) |
62 | 5, 6, 7, 8 | signstfvn 33878 |
. . . . . . 7
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) = (((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ))) |
63 | 62 | adantlr 711 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) = (((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ))) |
64 | 35 | adantlr 711 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β πΉ β Word β) |
65 | | simpr 483 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β πΎ β β) |
66 | | fzo0end 13728 |
. . . . . . . . 9
β’
((β―βπΉ)
β β β ((β―βπΉ) β 1) β
(0..^(β―βπΉ))) |
67 | 20, 66 | syl 17 |
. . . . . . . 8
β’ (πΉ β (Word β β
{β
}) β ((β―βπΉ) β 1) β
(0..^(β―βπΉ))) |
68 | 67 | ad2antrr 722 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β
((β―βπΉ) β
1) β (0..^(β―βπΉ))) |
69 | 5, 6, 7, 8 | signstfvp 33880 |
. . . . . . 7
β’ ((πΉ β Word β β§ πΎ β β β§
((β―βπΉ) β
1) β (0..^(β―βπΉ))) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)) = ((πβπΉ)β((β―βπΉ) β 1))) |
70 | 64, 65, 68, 69 | syl3anc 1369 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)) = ((πβπΉ)β((β―βπΉ) β 1))) |
71 | 63, 70 | neeq12d 3000 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)) β (((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ)) β ((πβπΉ)β((β―βπΉ) β 1)))) |
72 | 5, 6, 7, 8 | signstfvcl 33882 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§
((β―βπΉ) β
1) β (0..^(β―βπΉ))) β ((πβπΉ)β((β―βπΉ) β 1)) β {-1,
1}) |
73 | 68, 72 | syldan 589 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((πβπΉ)β((β―βπΉ) β 1)) β {-1,
1}) |
74 | | rexr 11264 |
. . . . . . . 8
β’ (πΎ β β β πΎ β
β*) |
75 | | sgncl 33835 |
. . . . . . . 8
β’ (πΎ β β*
β (sgnβπΎ) β
{-1, 0, 1}) |
76 | 74, 75 | syl 17 |
. . . . . . 7
β’ (πΎ β β β
(sgnβπΎ) β {-1,
0, 1}) |
77 | 76 | adantl 480 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (sgnβπΎ) β {-1, 0,
1}) |
78 | 5, 6 | signswch 33870 |
. . . . . 6
β’ ((((πβπΉ)β((β―βπΉ) β 1)) β {-1, 1} β§
(sgnβπΎ) β {-1,
0, 1}) β ((((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ)) β ((πβπΉ)β((β―βπΉ) β 1)) β (((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0)) |
79 | 73, 77, 78 | syl2anc 582 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ)) β ((πβπΉ)β((β―βπΉ) β 1)) β (((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0)) |
80 | 65 | rexrd 11268 |
. . . . . . . . 9
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β πΎ β
β*) |
81 | | sgnsgn 33845 |
. . . . . . . . 9
β’ (πΎ β β*
β (sgnβ(sgnβπΎ)) = (sgnβπΎ)) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β
(sgnβ(sgnβπΎ)) =
(sgnβπΎ)) |
83 | 82 | oveq2d 7427 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβ(sgnβπΎ)))
= ((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β· (sgnβπΎ))) |
84 | 83 | breq1d 5157 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβ(sgnβπΎ)))
< 0 β ((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β· (sgnβπΎ)) < 0)) |
85 | | neg1rr 12331 |
. . . . . . . . 9
β’ -1 β
β |
86 | | 1re 11218 |
. . . . . . . . 9
β’ 1 β
β |
87 | | prssi 4823 |
. . . . . . . . 9
β’ ((-1
β β β§ 1 β β) β {-1, 1} β
β) |
88 | 85, 86, 87 | mp2an 688 |
. . . . . . . 8
β’ {-1, 1}
β β |
89 | 88, 73 | sselid 3979 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((πβπΉ)β((β―βπΉ) β 1)) β
β) |
90 | | sgnclre 33836 |
. . . . . . . 8
β’ (πΎ β β β
(sgnβπΎ) β
β) |
91 | 90 | adantl 480 |
. . . . . . 7
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (sgnβπΎ) β
β) |
92 | | sgnmulsgn 33846 |
. . . . . . 7
β’ ((((πβπΉ)β((β―βπΉ) β 1)) β β β§
(sgnβπΎ) β
β) β ((((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0 β
((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβ(sgnβπΎ)))
< 0)) |
93 | 89, 91, 92 | syl2anc 582 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0 β
((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβ(sgnβπΎ)))
< 0)) |
94 | | sgnmulsgn 33846 |
. . . . . . 7
β’ ((((πβπΉ)β((β―βπΉ) β 1)) β β β§ πΎ β β) β
((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0 β
((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β·
(sgnβπΎ)) <
0)) |
95 | 89, 94 | sylancom 586 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0 β ((sgnβ((πβπΉ)β((β―βπΉ) β 1))) Β· (sgnβπΎ)) < 0)) |
96 | 84, 93, 95 | 3bitr4d 310 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β ((((πβπΉ)β((β―βπΉ) β 1)) Β· (sgnβπΎ)) < 0 β (((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0)) |
97 | 71, 79, 96 | 3bitrd 304 |
. . . 4
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)) β (((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0)) |
98 | 97 | ifbid 4550 |
. . 3
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1, 0) =
if((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0, 1,
0)) |
99 | 61, 98 | oveq12d 7429 |
. 2
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (Ξ£π β
(1..^(β―βπΉ))if(((πβ(πΉ ++ β¨βπΎββ©))βπ) β ((πβ(πΉ ++ β¨βπΎββ©))β(π β 1)), 1, 0) + if(((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) β ((πβ(πΉ ++ β¨βπΎββ©))β((β―βπΉ) β 1)), 1, 0)) = ((πβπΉ) + if((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0, 1, 0))) |
100 | 33, 99 | eqtrd 2770 |
1
β’ (((πΉ β (Word β β
{β
}) β§ (πΉβ0) β 0) β§ πΎ β β) β (πβ(πΉ ++ β¨βπΎββ©)) = ((πβπΉ) + if((((πβπΉ)β((β―βπΉ) β 1)) Β· πΎ) < 0, 1, 0))) |