Step | Hyp | Ref
| Expression |
1 | | simpl 482 |
. . 3
β’ ((π΄ β β€ β§ π β β) β π΄ β
β€) |
2 | | nnz 12583 |
. . . 4
β’ (π β β β π β
β€) |
3 | 2 | adantl 481 |
. . 3
β’ ((π΄ β β€ β§ π β β) β π β
β€) |
4 | | nnne0 12250 |
. . . 4
β’ (π β β β π β 0) |
5 | 4 | adantl 481 |
. . 3
β’ ((π΄ β β€ β§ π β β) β π β 0) |
6 | | lgsval4.1 |
. . . 4
β’ πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
7 | 6 | lgsval4 27205 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ)))) |
8 | 1, 3, 5, 7 | syl3anc 1368 |
. 2
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ)))) |
9 | | nngt0 12247 |
. . . . . . 7
β’ (π β β β 0 <
π) |
10 | 9 | adantl 481 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β 0 <
π) |
11 | | 0re 11220 |
. . . . . . 7
β’ 0 β
β |
12 | | nnre 12223 |
. . . . . . . 8
β’ (π β β β π β
β) |
13 | 12 | adantl 481 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β π β
β) |
14 | | ltnsym 11316 |
. . . . . . 7
β’ ((0
β β β§ π
β β) β (0 < π β Β¬ π < 0)) |
15 | 11, 13, 14 | sylancr 586 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β (0 <
π β Β¬ π < 0)) |
16 | 10, 15 | mpd 15 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β Β¬
π < 0) |
17 | 16 | intnanrd 489 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β Β¬
(π < 0 β§ π΄ < 0)) |
18 | 17 | iffalsed 4534 |
. . 3
β’ ((π΄ β β€ β§ π β β) β
if((π < 0 β§ π΄ < 0), -1, 1) =
1) |
19 | | nnnn0 12483 |
. . . . . . 7
β’ (π β β β π β
β0) |
20 | 19 | adantl 481 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β π β
β0) |
21 | 20 | nn0ge0d 12539 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β 0 β€
π) |
22 | 13, 21 | absidd 15375 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β
(absβπ) = π) |
23 | 22 | fveq2d 6889 |
. . 3
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)β(absβπ)) = (seq1( Β· , πΉ)βπ)) |
24 | 18, 23 | oveq12d 7423 |
. 2
β’ ((π΄ β β€ β§ π β β) β
(if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1(
Β· , πΉ)β(absβπ))) = (1 Β· (seq1( Β· , πΉ)βπ))) |
25 | | simpr 484 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β π β
β) |
26 | | nnuz 12869 |
. . . . . 6
β’ β =
(β€β₯β1) |
27 | 25, 26 | eleqtrdi 2837 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β π β
(β€β₯β1)) |
28 | 6 | lgsfcl3 27206 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆβ€) |
29 | 1, 3, 5, 28 | syl3anc 1368 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β πΉ:ββΆβ€) |
30 | | elfznn 13536 |
. . . . . 6
β’ (π₯ β (1...π) β π₯ β β) |
31 | | ffvelcdm 7077 |
. . . . . 6
β’ ((πΉ:ββΆβ€ β§
π₯ β β) β
(πΉβπ₯) β β€) |
32 | 29, 30, 31 | syl2an 595 |
. . . . 5
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...π)) β (πΉβπ₯) β β€) |
33 | | zmulcl 12615 |
. . . . . 6
β’ ((π₯ β β€ β§ π¦ β β€) β (π₯ Β· π¦) β β€) |
34 | 33 | adantl 481 |
. . . . 5
β’ (((π΄ β β€ β§ π β β) β§ (π₯ β β€ β§ π¦ β β€)) β (π₯ Β· π¦) β β€) |
35 | 27, 32, 34 | seqcl 13993 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)βπ) β
β€) |
36 | 35 | zcnd 12671 |
. . 3
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)βπ) β
β) |
37 | 36 | mullidd 11236 |
. 2
β’ ((π΄ β β€ β§ π β β) β (1
Β· (seq1( Β· , πΉ)βπ)) = (seq1( Β· , πΉ)βπ)) |
38 | 8, 24, 37 | 3eqtrd 2770 |
1
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = (seq1( Β· , πΉ)βπ)) |