Step |
Hyp |
Ref |
Expression |
1 |
|
rpvmasum.z |
โข ๐ = ( โค/nโค โ ๐ ) |
2 |
|
rpvmasum.l |
โข ๐ฟ = ( โคRHom โ ๐ ) |
3 |
|
rpvmasum.a |
โข ( ๐ โ ๐ โ โ ) |
4 |
|
dchrmusum.g |
โข ๐บ = ( DChr โ ๐ ) |
5 |
|
dchrmusum.d |
โข ๐ท = ( Base โ ๐บ ) |
6 |
|
dchrmusum.1 |
โข 1 = ( 0g โ ๐บ ) |
7 |
|
dchrmusum.b |
โข ( ๐ โ ๐ โ ๐ท ) |
8 |
|
dchrmusum.n1 |
โข ( ๐ โ ๐ โ 1 ) |
9 |
|
eqid |
โข ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) = ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) |
10 |
1 2 3 4 5 6 7 8 9
|
dchrmusumlema |
โข ( ๐ โ โ ๐ก โ ๐ โ ( 0 [,) +โ ) ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) ) |
11 |
3
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( 0 [,) +โ ) โง ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) ) ) โ ๐ โ โ ) |
12 |
7
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( 0 [,) +โ ) โง ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) ) ) โ ๐ โ ๐ท ) |
13 |
8
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( 0 [,) +โ ) โง ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) ) ) โ ๐ โ 1 ) |
14 |
|
simprl |
โข ( ( ๐ โง ( ๐ โ ( 0 [,) +โ ) โง ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) ) ) โ ๐ โ ( 0 [,) +โ ) ) |
15 |
|
simprrl |
โข ( ( ๐ โง ( ๐ โ ( 0 [,) +โ ) โง ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) ) ) โ seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก ) |
16 |
|
simprrr |
โข ( ( ๐ โง ( ๐ โ ( 0 [,) +โ ) โง ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) ) ) โ โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) |
17 |
1 2 11 4 5 6 12 13 9 14 15 16
|
dchrvmasumlem |
โข ( ( ๐ โง ( ๐ โ ( 0 [,) +โ ) โง ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) ) ) โ ( ๐ฅ โ โ+ โฆ ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฅ ) ) ( ( ๐ โ ( ๐ฟ โ ๐ ) ) ยท ( ( ฮ โ ๐ ) / ๐ ) ) ) โ ๐(1) ) |
18 |
17
|
rexlimdvaa |
โข ( ๐ โ ( โ ๐ โ ( 0 [,) +โ ) ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) โ ( ๐ฅ โ โ+ โฆ ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฅ ) ) ( ( ๐ โ ( ๐ฟ โ ๐ ) ) ยท ( ( ฮ โ ๐ ) / ๐ ) ) ) โ ๐(1) ) ) |
19 |
18
|
exlimdv |
โข ( ๐ โ ( โ ๐ก โ ๐ โ ( 0 [,) +โ ) ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ๐ก โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ( seq 1 ( + , ( ๐ โ โ โฆ ( ( ๐ โ ( ๐ฟ โ ๐ ) ) / ๐ ) ) ) โ ( โ โ ๐ฆ ) ) โ ๐ก ) ) โค ( ๐ / ๐ฆ ) ) โ ( ๐ฅ โ โ+ โฆ ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฅ ) ) ( ( ๐ โ ( ๐ฟ โ ๐ ) ) ยท ( ( ฮ โ ๐ ) / ๐ ) ) ) โ ๐(1) ) ) |
20 |
10 19
|
mpd |
โข ( ๐ โ ( ๐ฅ โ โ+ โฆ ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฅ ) ) ( ( ๐ โ ( ๐ฟ โ ๐ ) ) ยท ( ( ฮ โ ๐ ) / ๐ ) ) ) โ ๐(1) ) |