Step | Hyp | Ref
| Expression |
1 | | iftrue 4529 |
. . . . . . . . 9
β’ (π΄ < 0 β if(π΄ < 0, -1, 1) =
-1) |
2 | 1 | adantl 481 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β if(π΄ < 0, -1, 1) = -1) |
3 | 2 | oveq1d 7419 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (if(π΄ < 0, -1, 1) Β· if((π < 0 β§ π΄ < 0), -1, 1)) = (-1 Β· if((π < 0 β§ π΄ < 0), -1, 1))) |
4 | | oveq2 7412 |
. . . . . . . . . 10
β’ (if(π < 0, -1, 1) = -1 β (-1
Β· if(π < 0, -1,
1)) = (-1 Β· -1)) |
5 | | neg1mulneg1e1 12426 |
. . . . . . . . . 10
β’ (-1
Β· -1) = 1 |
6 | 4, 5 | eqtrdi 2782 |
. . . . . . . . 9
β’ (if(π < 0, -1, 1) = -1 β (-1
Β· if(π < 0, -1,
1)) = 1) |
7 | | oveq2 7412 |
. . . . . . . . . 10
β’ (if(π < 0, -1, 1) = 1 β (-1
Β· if(π < 0, -1,
1)) = (-1 Β· 1)) |
8 | | ax-1cn 11167 |
. . . . . . . . . . 11
β’ 1 β
β |
9 | 8 | mulm1i 11660 |
. . . . . . . . . 10
β’ (-1
Β· 1) = -1 |
10 | 7, 9 | eqtrdi 2782 |
. . . . . . . . 9
β’ (if(π < 0, -1, 1) = 1 β (-1
Β· if(π < 0, -1,
1)) = -1) |
11 | 6, 10 | ifsb 4536 |
. . . . . . . 8
β’ (-1
Β· if(π < 0, -1,
1)) = if(π < 0, 1,
-1) |
12 | | simpr 484 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β π΄ < 0) |
13 | 12 | biantrud 531 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (π < 0 β (π < 0 β§ π΄ < 0))) |
14 | 13 | ifbid 4546 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β if(π < 0, -1, 1) = if((π < 0 β§ π΄ < 0), -1, 1)) |
15 | 14 | oveq2d 7420 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (-1 Β· if(π < 0, -1, 1)) = (-1 Β·
if((π < 0 β§ π΄ < 0), -1,
1))) |
16 | | simpl3 1190 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β π β 0) |
17 | 16 | necomd 2990 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β 0 β π) |
18 | | simpl2 1189 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β π β β€) |
19 | 18 | zred 12667 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β π β β) |
20 | | 0re 11217 |
. . . . . . . . . . . . 13
β’ 0 β
β |
21 | | ltlen 11316 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 0 β
β) β (π < 0
β (π β€ 0 β§ 0
β π))) |
22 | 19, 20, 21 | sylancl 585 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (π < 0 β (π β€ 0 β§ 0 β π))) |
23 | 17, 22 | mpbiran2d 705 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (π < 0 β π β€ 0)) |
24 | 19 | le0neg1d 11786 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (π β€ 0 β 0 β€ -π)) |
25 | 19 | renegcld 11642 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β -π β β) |
26 | | lenlt 11293 |
. . . . . . . . . . . 12
β’ ((0
β β β§ -π
β β) β (0 β€ -π β Β¬ -π < 0)) |
27 | 20, 25, 26 | sylancr 586 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (0 β€ -π β Β¬ -π < 0)) |
28 | 23, 24, 27 | 3bitrd 305 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (π < 0 β Β¬ -π < 0)) |
29 | 28 | ifbid 4546 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β if(π < 0, 1, -1) = if(Β¬ -π < 0, 1,
-1)) |
30 | | ifnot 4575 |
. . . . . . . . 9
β’ if(Β¬
-π < 0, 1, -1) =
if(-π < 0, -1,
1) |
31 | 29, 30 | eqtrdi 2782 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β if(π < 0, 1, -1) = if(-π < 0, -1, 1)) |
32 | 11, 15, 31 | 3eqtr3a 2790 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (-1 Β· if((π < 0 β§ π΄ < 0), -1, 1)) = if(-π < 0, -1, 1)) |
33 | 12 | biantrud 531 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (-π < 0 β (-π < 0 β§ π΄ < 0))) |
34 | 33 | ifbid 4546 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β if(-π < 0, -1, 1) = if((-π < 0 β§ π΄ < 0), -1, 1)) |
35 | 3, 32, 34 | 3eqtrd 2770 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π΄ < 0) β (if(π΄ < 0, -1, 1) Β· if((π < 0 β§ π΄ < 0), -1, 1)) = if((-π < 0 β§ π΄ < 0), -1, 1)) |
36 | | 1t1e1 12375 |
. . . . . . 7
β’ (1
Β· 1) = 1 |
37 | | iffalse 4532 |
. . . . . . . . 9
β’ (Β¬
π΄ < 0 β if(π΄ < 0, -1, 1) =
1) |
38 | 37 | adantl 481 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ Β¬ π΄ < 0) β if(π΄ < 0, -1, 1) =
1) |
39 | | simpr 484 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ Β¬ π΄ < 0) β Β¬ π΄ < 0) |
40 | 39 | intnand 488 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ Β¬ π΄ < 0) β Β¬ (π < 0 β§ π΄ < 0)) |
41 | 40 | iffalsed 4534 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ Β¬ π΄ < 0) β if((π < 0 β§ π΄ < 0), -1, 1) = 1) |
42 | 38, 41 | oveq12d 7422 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ Β¬ π΄ < 0) β (if(π΄ < 0, -1, 1) Β·
if((π < 0 β§ π΄ < 0), -1, 1)) = (1 Β·
1)) |
43 | 39 | intnand 488 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ Β¬ π΄ < 0) β Β¬ (-π < 0 β§ π΄ < 0)) |
44 | 43 | iffalsed 4534 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ Β¬ π΄ < 0) β if((-π < 0 β§ π΄ < 0), -1, 1) = 1) |
45 | 36, 42, 44 | 3eqtr4a 2792 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ Β¬ π΄ < 0) β (if(π΄ < 0, -1, 1) Β·
if((π < 0 β§ π΄ < 0), -1, 1)) = if((-π < 0 β§ π΄ < 0), -1, 1)) |
46 | 35, 45 | pm2.61dan 810 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (if(π΄ < 0, -1, 1) Β·
if((π < 0 β§ π΄ < 0), -1, 1)) = if((-π < 0 β§ π΄ < 0), -1, 1)) |
47 | 46 | eqcomd 2732 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β if((-π < 0 β§ π΄ < 0), -1, 1) = (if(π΄ < 0, -1, 1) Β· if((π < 0 β§ π΄ < 0), -1, 1))) |
48 | | simpr 484 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π β β) β π β
β) |
49 | | simpl2 1189 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π β β) β π β
β€) |
50 | | zq 12939 |
. . . . . . . . . . 11
β’ (π β β€ β π β
β) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π β β) β π β
β) |
52 | | pcneg 16814 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π pCnt -π) = (π pCnt π)) |
53 | 48, 51, 52 | syl2anc 583 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π β β) β (π pCnt -π) = (π pCnt π)) |
54 | 53 | oveq2d 7420 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π β β) β ((π΄ /L π)β(π pCnt -π)) = ((π΄ /L π)β(π pCnt π))) |
55 | 54 | ifeq1da 4554 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β if(π β β, ((π΄ /L π)β(π pCnt -π)), 1) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
56 | 55 | mpteq2dv 5243 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt -π)), 1)) = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))) |
57 | 56 | seqeq3d 13977 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt -π)), 1))) = seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))) |
58 | | zcn 12564 |
. . . . . . 7
β’ (π β β€ β π β
β) |
59 | 58 | 3ad2ant2 1131 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β π β
β) |
60 | 59 | absnegd 15400 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β
(absβ-π) =
(absβπ)) |
61 | 57, 60 | fveq12d 6891 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt -π)), 1)))β(absβ-π)) = (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ))) |
62 | 47, 61 | oveq12d 7422 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (if((-π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt -π)), 1)))β(absβ-π))) = ((if(π΄ < 0, -1, 1) Β· if((π < 0 β§ π΄ < 0), -1, 1)) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)))) |
63 | | neg1cn 12327 |
. . . . . 6
β’ -1 β
β |
64 | 63, 8 | ifcli 4570 |
. . . . 5
β’ if(π΄ < 0, -1, 1) β
β |
65 | 64 | a1i 11 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β if(π΄ < 0, -1, 1) β
β) |
66 | 63, 8 | ifcli 4570 |
. . . . 5
β’ if((π < 0 β§ π΄ < 0), -1, 1) β
β |
67 | 66 | a1i 11 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β if((π < 0 β§ π΄ < 0), -1, 1) β
β) |
68 | | nnabscl 15276 |
. . . . . . . 8
β’ ((π β β€ β§ π β 0) β (absβπ) β
β) |
69 | 68 | 3adant1 1127 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (absβπ) β
β) |
70 | | nnuz 12866 |
. . . . . . 7
β’ β =
(β€β₯β1) |
71 | 69, 70 | eleqtrdi 2837 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (absβπ) β
(β€β₯β1)) |
72 | | eqid 2726 |
. . . . . . . 8
β’ (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
73 | 72 | lgsfcl3 27202 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)),
1)):ββΆβ€) |
74 | | elfznn 13533 |
. . . . . . 7
β’ (π₯ β (1...(absβπ)) β π₯ β β) |
75 | | ffvelcdm 7076 |
. . . . . . 7
β’ (((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)):ββΆβ€ β§ π₯ β β) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ₯) β β€) |
76 | 73, 74, 75 | syl2an 595 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π₯ β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ₯) β β€) |
77 | | zmulcl 12612 |
. . . . . . 7
β’ ((π₯ β β€ β§ π¦ β β€) β (π₯ Β· π¦) β β€) |
78 | 77 | adantl 481 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π₯ β β€ β§ π¦ β β€)) β (π₯ Β· π¦) β β€) |
79 | 71, 76, 78 | seqcl 13991 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) β β€) |
80 | 79 | zcnd 12668 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) β β) |
81 | 65, 67, 80 | mulassd 11238 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((if(π΄ < 0, -1, 1) Β·
if((π < 0 β§ π΄ < 0), -1, 1)) Β·
(seq1( Β· , (π β
β β¦ if(π β
β, ((π΄
/L π)β(π pCnt π)), 1)))β(absβπ))) = (if(π΄ < 0, -1, 1) Β· (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))))) |
82 | 62, 81 | eqtrd 2766 |
. 2
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (if((-π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt -π)), 1)))β(absβ-π))) = (if(π΄ < 0, -1, 1) Β· (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))))) |
83 | | simp1 1133 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β π΄ β
β€) |
84 | | znegcl 12598 |
. . . 4
β’ (π β β€ β -π β
β€) |
85 | 84 | 3ad2ant2 1131 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β -π β
β€) |
86 | | simp3 1135 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β π β 0) |
87 | 59, 86 | negne0d 11570 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β -π β 0) |
88 | | eqid 2726 |
. . . 4
β’ (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt -π)), 1)) = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt -π)), 1)) |
89 | 88 | lgsval4 27201 |
. . 3
β’ ((π΄ β β€ β§ -π β β€ β§ -π β 0) β (π΄ /L -π) = (if((-π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt -π)), 1)))β(absβ-π)))) |
90 | 83, 85, 87, 89 | syl3anc 1368 |
. 2
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L -π) = (if((-π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt -π)), 1)))β(absβ-π)))) |
91 | 72 | lgsval4 27201 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)))) |
92 | 91 | oveq2d 7420 |
. 2
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (if(π΄ < 0, -1, 1) Β· (π΄ /L π)) = (if(π΄ < 0, -1, 1) Β· (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))))) |
93 | 82, 90, 92 | 3eqtr4d 2776 |
1
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L -π) = (if(π΄ < 0, -1, 1) Β· (π΄ /L π))) |