Step | Hyp | Ref
| Expression |
1 | | signsvf.f |
. . . . . 6
β’ (π β πΉ = (πΈ ++ β¨βπ΄ββ©)) |
2 | 1 | fveq2d 6892 |
. . . . 5
β’ (π β (πβπΉ) = (πβ(πΈ ++ β¨βπ΄ββ©))) |
3 | | signsvf.e |
. . . . . 6
β’ (π β πΈ β (Word β β
{β
})) |
4 | | signsvf.0 |
. . . . . 6
β’ (π β (πΈβ0) β 0) |
5 | | signsvf.a |
. . . . . 6
β’ (π β π΄ β β) |
6 | | signsv.p |
. . . . . . 7
⒠⨣ =
(π β {-1, 0, 1}, π β {-1, 0, 1} β¦
if(π = 0, π, π)) |
7 | | signsv.w |
. . . . . . 7
β’ π = {β¨(Baseβndx), {-1,
0, 1}β©, β¨(+gβndx), ⨣
β©} |
8 | | signsv.t |
. . . . . . 7
β’ π = (π β Word β β¦ (π β
(0..^(β―βπ))
β¦ (π
Ξ£g (π β (0...π) β¦ (sgnβ(πβπ)))))) |
9 | | signsv.v |
. . . . . . 7
β’ π = (π β Word β β¦ Ξ£π β
(1..^(β―βπ))if(((πβπ)βπ) β ((πβπ)β(π β 1)), 1, 0)) |
10 | 6, 7, 8, 9 | signsvfn 33581 |
. . . . . 6
β’ (((πΈ β (Word β β
{β
}) β§ (πΈβ0) β 0) β§ π΄ β β) β (πβ(πΈ ++ β¨βπ΄ββ©)) = ((πβπΈ) + if((((πβπΈ)β((β―βπΈ) β 1)) Β· π΄) < 0, 1, 0))) |
11 | 3, 4, 5, 10 | syl21anc 836 |
. . . . 5
β’ (π β (πβ(πΈ ++ β¨βπ΄ββ©)) = ((πβπΈ) + if((((πβπΈ)β((β―βπΈ) β 1)) Β· π΄) < 0, 1, 0))) |
12 | 2, 11 | eqtrd 2772 |
. . . 4
β’ (π β (πβπΉ) = ((πβπΈ) + if((((πβπΈ)β((β―βπΈ) β 1)) Β· π΄) < 0, 1, 0))) |
13 | 12 | adantr 481 |
. . 3
β’ ((π β§ (π΄ Β· π΅) < 0) β (πβπΉ) = ((πβπΈ) + if((((πβπΈ)β((β―βπΈ) β 1)) Β· π΄) < 0, 1, 0))) |
14 | | signsvt.b |
. . . . . . . 8
β’ π΅ = ((πβπΈ)β(π β 1)) |
15 | | signsvf.n |
. . . . . . . . . 10
β’ π = (β―βπΈ) |
16 | 15 | oveq1i 7415 |
. . . . . . . . 9
β’ (π β 1) =
((β―βπΈ) β
1) |
17 | 16 | fveq2i 6891 |
. . . . . . . 8
β’ ((πβπΈ)β(π β 1)) = ((πβπΈ)β((β―βπΈ) β 1)) |
18 | 14, 17 | eqtri 2760 |
. . . . . . 7
β’ π΅ = ((πβπΈ)β((β―βπΈ) β 1)) |
19 | 18 | oveq1i 7415 |
. . . . . 6
β’ (π΅ Β· π΄) = (((πβπΈ)β((β―βπΈ) β 1)) Β· π΄) |
20 | 3 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΄ Β· π΅) < 0) β πΈ β (Word β β
{β
})) |
21 | 20 | eldifad 3959 |
. . . . . . . . . . . 12
β’ ((π β§ (π΄ Β· π΅) < 0) β πΈ β Word β) |
22 | 6, 7, 8, 9 | signstf 33565 |
. . . . . . . . . . . 12
β’ (πΈ β Word β β
(πβπΈ) β Word β) |
23 | | wrdf 14465 |
. . . . . . . . . . . 12
β’ ((πβπΈ) β Word β β (πβπΈ):(0..^(β―β(πβπΈ)))βΆβ) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ (π΄ Β· π΅) < 0) β (πβπΈ):(0..^(β―β(πβπΈ)))βΆβ) |
25 | | eldifsn 4789 |
. . . . . . . . . . . . . . 15
β’ (πΈ β (Word β β
{β
}) β (πΈ β
Word β β§ πΈ β
β
)) |
26 | 3, 25 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β (πΈ β Word β β§ πΈ β β
)) |
27 | 26 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΄ Β· π΅) < 0) β (πΈ β Word β β§ πΈ β β
)) |
28 | | lennncl 14480 |
. . . . . . . . . . . . 13
β’ ((πΈ β Word β β§ πΈ β β
) β
(β―βπΈ) β
β) |
29 | | fzo0end 13720 |
. . . . . . . . . . . . 13
β’
((β―βπΈ)
β β β ((β―βπΈ) β 1) β
(0..^(β―βπΈ))) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ (π΄ Β· π΅) < 0) β ((β―βπΈ) β 1) β
(0..^(β―βπΈ))) |
31 | 6, 7, 8, 9 | signstlen 33566 |
. . . . . . . . . . . . . 14
β’ (πΈ β Word β β
(β―β(πβπΈ)) = (β―βπΈ)) |
32 | 21, 31 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΄ Β· π΅) < 0) β (β―β(πβπΈ)) = (β―βπΈ)) |
33 | 32 | oveq2d 7421 |
. . . . . . . . . . . 12
β’ ((π β§ (π΄ Β· π΅) < 0) β (0..^(β―β(πβπΈ))) = (0..^(β―βπΈ))) |
34 | 30, 33 | eleqtrrd 2836 |
. . . . . . . . . . 11
β’ ((π β§ (π΄ Β· π΅) < 0) β ((β―βπΈ) β 1) β
(0..^(β―β(πβπΈ)))) |
35 | 24, 34 | ffvelcdmd 7084 |
. . . . . . . . . 10
β’ ((π β§ (π΄ Β· π΅) < 0) β ((πβπΈ)β((β―βπΈ) β 1)) β
β) |
36 | 18, 35 | eqeltrid 2837 |
. . . . . . . . 9
β’ ((π β§ (π΄ Β· π΅) < 0) β π΅ β β) |
37 | 36 | recnd 11238 |
. . . . . . . 8
β’ ((π β§ (π΄ Β· π΅) < 0) β π΅ β β) |
38 | 5 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π΄ Β· π΅) < 0) β π΄ β β) |
39 | 38 | recnd 11238 |
. . . . . . . 8
β’ ((π β§ (π΄ Β· π΅) < 0) β π΄ β β) |
40 | 37, 39 | mulcomd 11231 |
. . . . . . 7
β’ ((π β§ (π΄ Β· π΅) < 0) β (π΅ Β· π΄) = (π΄ Β· π΅)) |
41 | | simpr 485 |
. . . . . . 7
β’ ((π β§ (π΄ Β· π΅) < 0) β (π΄ Β· π΅) < 0) |
42 | 40, 41 | eqbrtrd 5169 |
. . . . . 6
β’ ((π β§ (π΄ Β· π΅) < 0) β (π΅ Β· π΄) < 0) |
43 | 19, 42 | eqbrtrrid 5183 |
. . . . 5
β’ ((π β§ (π΄ Β· π΅) < 0) β (((πβπΈ)β((β―βπΈ) β 1)) Β· π΄) < 0) |
44 | 43 | iftrued 4535 |
. . . 4
β’ ((π β§ (π΄ Β· π΅) < 0) β if((((πβπΈ)β((β―βπΈ) β 1)) Β· π΄) < 0, 1, 0) = 1) |
45 | 44 | oveq2d 7421 |
. . 3
β’ ((π β§ (π΄ Β· π΅) < 0) β ((πβπΈ) + if((((πβπΈ)β((β―βπΈ) β 1)) Β· π΄) < 0, 1, 0)) = ((πβπΈ) + 1)) |
46 | 13, 45 | eqtr2d 2773 |
. 2
β’ ((π β§ (π΄ Β· π΅) < 0) β ((πβπΈ) + 1) = (πβπΉ)) |
47 | 6, 7, 8, 9 | signsvvf 33578 |
. . . . . 6
β’ π:Word
ββΆβ0 |
48 | 47 | a1i 11 |
. . . . 5
β’ ((π β§ (π΄ Β· π΅) < 0) β π:Word
ββΆβ0) |
49 | 1 | adantr 481 |
. . . . . 6
β’ ((π β§ (π΄ Β· π΅) < 0) β πΉ = (πΈ ++ β¨βπ΄ββ©)) |
50 | 38 | s1cld 14549 |
. . . . . . 7
β’ ((π β§ (π΄ Β· π΅) < 0) β β¨βπ΄ββ© β Word
β) |
51 | | ccatcl 14520 |
. . . . . . 7
β’ ((πΈ β Word β β§
β¨βπ΄ββ©
β Word β) β (πΈ ++ β¨βπ΄ββ©) β Word
β) |
52 | 21, 50, 51 | syl2anc 584 |
. . . . . 6
β’ ((π β§ (π΄ Β· π΅) < 0) β (πΈ ++ β¨βπ΄ββ©) β Word
β) |
53 | 49, 52 | eqeltrd 2833 |
. . . . 5
β’ ((π β§ (π΄ Β· π΅) < 0) β πΉ β Word β) |
54 | 48, 53 | ffvelcdmd 7084 |
. . . 4
β’ ((π β§ (π΄ Β· π΅) < 0) β (πβπΉ) β
β0) |
55 | 54 | nn0cnd 12530 |
. . 3
β’ ((π β§ (π΄ Β· π΅) < 0) β (πβπΉ) β β) |
56 | 48, 21 | ffvelcdmd 7084 |
. . . 4
β’ ((π β§ (π΄ Β· π΅) < 0) β (πβπΈ) β
β0) |
57 | 56 | nn0cnd 12530 |
. . 3
β’ ((π β§ (π΄ Β· π΅) < 0) β (πβπΈ) β β) |
58 | | 1cnd 11205 |
. . 3
β’ ((π β§ (π΄ Β· π΅) < 0) β 1 β
β) |
59 | 55, 57, 58 | subaddd 11585 |
. 2
β’ ((π β§ (π΄ Β· π΅) < 0) β (((πβπΉ) β (πβπΈ)) = 1 β ((πβπΈ) + 1) = (πβπΉ))) |
60 | 46, 59 | mpbird 256 |
1
β’ ((π β§ (π΄ Β· π΅) < 0) β ((πβπΉ) β (πβπΈ)) = 1) |