Step |
Hyp |
Ref |
Expression |
1 |
|
lgsval4.1 |
โข ๐น = ( ๐ โ โ โฆ if ( ๐ โ โ , ( ( ๐ด /L ๐ ) โ ( ๐ pCnt ๐ ) ) , 1 ) ) |
2 |
|
simpl |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ๐ด โ โค ) |
3 |
|
nnz |
โข ( ๐ โ โ โ ๐ โ โค ) |
4 |
3
|
adantl |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ๐ โ โค ) |
5 |
|
nnne0 |
โข ( ๐ โ โ โ ๐ โ 0 ) |
6 |
5
|
adantl |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ๐ โ 0 ) |
7 |
1
|
lgsval4 |
โข ( ( ๐ด โ โค โง ๐ โ โค โง ๐ โ 0 ) โ ( ๐ด /L ๐ ) = ( if ( ( ๐ < 0 โง ๐ด < 0 ) , - 1 , 1 ) ยท ( seq 1 ( ยท , ๐น ) โ ( abs โ ๐ ) ) ) ) |
8 |
2 4 6 7
|
syl3anc |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( ๐ด /L ๐ ) = ( if ( ( ๐ < 0 โง ๐ด < 0 ) , - 1 , 1 ) ยท ( seq 1 ( ยท , ๐น ) โ ( abs โ ๐ ) ) ) ) |
9 |
|
nngt0 |
โข ( ๐ โ โ โ 0 < ๐ ) |
10 |
9
|
adantl |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ 0 < ๐ ) |
11 |
|
0re |
โข 0 โ โ |
12 |
|
nnre |
โข ( ๐ โ โ โ ๐ โ โ ) |
13 |
12
|
adantl |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ๐ โ โ ) |
14 |
|
ltnsym |
โข ( ( 0 โ โ โง ๐ โ โ ) โ ( 0 < ๐ โ ยฌ ๐ < 0 ) ) |
15 |
11 13 14
|
sylancr |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( 0 < ๐ โ ยฌ ๐ < 0 ) ) |
16 |
10 15
|
mpd |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ยฌ ๐ < 0 ) |
17 |
16
|
intnanrd |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ยฌ ( ๐ < 0 โง ๐ด < 0 ) ) |
18 |
17
|
iffalsed |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ if ( ( ๐ < 0 โง ๐ด < 0 ) , - 1 , 1 ) = 1 ) |
19 |
|
nnnn0 |
โข ( ๐ โ โ โ ๐ โ โ0 ) |
20 |
19
|
adantl |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ๐ โ โ0 ) |
21 |
20
|
nn0ge0d |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ 0 โค ๐ ) |
22 |
13 21
|
absidd |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( abs โ ๐ ) = ๐ ) |
23 |
22
|
fveq2d |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( seq 1 ( ยท , ๐น ) โ ( abs โ ๐ ) ) = ( seq 1 ( ยท , ๐น ) โ ๐ ) ) |
24 |
18 23
|
oveq12d |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( if ( ( ๐ < 0 โง ๐ด < 0 ) , - 1 , 1 ) ยท ( seq 1 ( ยท , ๐น ) โ ( abs โ ๐ ) ) ) = ( 1 ยท ( seq 1 ( ยท , ๐น ) โ ๐ ) ) ) |
25 |
|
simpr |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ๐ โ โ ) |
26 |
|
nnuz |
โข โ = ( โคโฅ โ 1 ) |
27 |
25 26
|
eleqtrdi |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ๐ โ ( โคโฅ โ 1 ) ) |
28 |
1
|
lgsfcl3 |
โข ( ( ๐ด โ โค โง ๐ โ โค โง ๐ โ 0 ) โ ๐น : โ โถ โค ) |
29 |
2 4 6 28
|
syl3anc |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ๐น : โ โถ โค ) |
30 |
|
elfznn |
โข ( ๐ฅ โ ( 1 ... ๐ ) โ ๐ฅ โ โ ) |
31 |
|
ffvelcdm |
โข ( ( ๐น : โ โถ โค โง ๐ฅ โ โ ) โ ( ๐น โ ๐ฅ ) โ โค ) |
32 |
29 30 31
|
syl2an |
โข ( ( ( ๐ด โ โค โง ๐ โ โ ) โง ๐ฅ โ ( 1 ... ๐ ) ) โ ( ๐น โ ๐ฅ ) โ โค ) |
33 |
|
zmulcl |
โข ( ( ๐ฅ โ โค โง ๐ฆ โ โค ) โ ( ๐ฅ ยท ๐ฆ ) โ โค ) |
34 |
33
|
adantl |
โข ( ( ( ๐ด โ โค โง ๐ โ โ ) โง ( ๐ฅ โ โค โง ๐ฆ โ โค ) ) โ ( ๐ฅ ยท ๐ฆ ) โ โค ) |
35 |
27 32 34
|
seqcl |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( seq 1 ( ยท , ๐น ) โ ๐ ) โ โค ) |
36 |
35
|
zcnd |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( seq 1 ( ยท , ๐น ) โ ๐ ) โ โ ) |
37 |
36
|
mullidd |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( 1 ยท ( seq 1 ( ยท , ๐น ) โ ๐ ) ) = ( seq 1 ( ยท , ๐น ) โ ๐ ) ) |
38 |
8 24 37
|
3eqtrd |
โข ( ( ๐ด โ โค โง ๐ โ โ ) โ ( ๐ด /L ๐ ) = ( seq 1 ( ยท , ๐น ) โ ๐ ) ) |