Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((π΄ β β€ β§ π β β) β π΄ β
β€) |
2 | | nnz 12527 |
. . . 4
β’ (π β β β π β
β€) |
3 | 2 | adantl 483 |
. . 3
β’ ((π΄ β β€ β§ π β β) β π β
β€) |
4 | | nnne0 12194 |
. . . 4
β’ (π β β β π β 0) |
5 | 4 | adantl 483 |
. . 3
β’ ((π΄ β β€ β§ π β β) β π β 0) |
6 | | lgsval4.1 |
. . . 4
β’ πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
7 | 6 | lgsval4 26681 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ)))) |
8 | 1, 3, 5, 7 | syl3anc 1372 |
. 2
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ)))) |
9 | | nngt0 12191 |
. . . . . . 7
β’ (π β β β 0 <
π) |
10 | 9 | adantl 483 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β 0 <
π) |
11 | | 0re 11164 |
. . . . . . 7
β’ 0 β
β |
12 | | nnre 12167 |
. . . . . . . 8
β’ (π β β β π β
β) |
13 | 12 | adantl 483 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β π β
β) |
14 | | ltnsym 11260 |
. . . . . . 7
β’ ((0
β β β§ π
β β) β (0 < π β Β¬ π < 0)) |
15 | 11, 13, 14 | sylancr 588 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β (0 <
π β Β¬ π < 0)) |
16 | 10, 15 | mpd 15 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β Β¬
π < 0) |
17 | 16 | intnanrd 491 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β Β¬
(π < 0 β§ π΄ < 0)) |
18 | 17 | iffalsed 4502 |
. . 3
β’ ((π΄ β β€ β§ π β β) β
if((π < 0 β§ π΄ < 0), -1, 1) =
1) |
19 | | nnnn0 12427 |
. . . . . . 7
β’ (π β β β π β
β0) |
20 | 19 | adantl 483 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β π β
β0) |
21 | 20 | nn0ge0d 12483 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β 0 β€
π) |
22 | 13, 21 | absidd 15314 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β
(absβπ) = π) |
23 | 22 | fveq2d 6851 |
. . 3
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)β(absβπ)) = (seq1( Β· , πΉ)βπ)) |
24 | 18, 23 | oveq12d 7380 |
. 2
β’ ((π΄ β β€ β§ π β β) β
(if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1(
Β· , πΉ)β(absβπ))) = (1 Β· (seq1( Β· , πΉ)βπ))) |
25 | | simpr 486 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β π β
β) |
26 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
27 | 25, 26 | eleqtrdi 2848 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β π β
(β€β₯β1)) |
28 | 6 | lgsfcl3 26682 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆβ€) |
29 | 1, 3, 5, 28 | syl3anc 1372 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β πΉ:ββΆβ€) |
30 | | elfznn 13477 |
. . . . . 6
β’ (π₯ β (1...π) β π₯ β β) |
31 | | ffvelcdm 7037 |
. . . . . 6
β’ ((πΉ:ββΆβ€ β§
π₯ β β) β
(πΉβπ₯) β β€) |
32 | 29, 30, 31 | syl2an 597 |
. . . . 5
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...π)) β (πΉβπ₯) β β€) |
33 | | zmulcl 12559 |
. . . . . 6
β’ ((π₯ β β€ β§ π¦ β β€) β (π₯ Β· π¦) β β€) |
34 | 33 | adantl 483 |
. . . . 5
β’ (((π΄ β β€ β§ π β β) β§ (π₯ β β€ β§ π¦ β β€)) β (π₯ Β· π¦) β β€) |
35 | 27, 32, 34 | seqcl 13935 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)βπ) β
β€) |
36 | 35 | zcnd 12615 |
. . 3
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)βπ) β
β) |
37 | 36 | mulid2d 11180 |
. 2
β’ ((π΄ β β€ β§ π β β) β (1
Β· (seq1( Β· , πΉ)βπ)) = (seq1( Β· , πΉ)βπ)) |
38 | 8, 24, 37 | 3eqtrd 2781 |
1
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = (seq1( Β· , πΉ)βπ)) |