Step |
Hyp |
Ref |
Expression |
1 |
|
stoweidlem30.1 |
โข ๐ = { โ โ ๐ด โฃ ( ( โ โ ๐ ) = 0 โง โ ๐ก โ ๐ ( 0 โค ( โ โ ๐ก ) โง ( โ โ ๐ก ) โค 1 ) ) } |
2 |
|
stoweidlem30.2 |
โข ๐ = ( ๐ก โ ๐ โฆ ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ก ) ) ) |
3 |
|
stoweidlem30.3 |
โข ( ๐ โ ๐ โ โ ) |
4 |
|
stoweidlem30.4 |
โข ( ๐ โ ๐บ : ( 1 ... ๐ ) โถ ๐ ) |
5 |
|
stoweidlem30.5 |
โข ( ( ๐ โง ๐ โ ๐ด ) โ ๐ : ๐ โถ โ ) |
6 |
|
eleq1 |
โข ( ๐ = ๐ โ ( ๐ โ ๐ โ ๐ โ ๐ ) ) |
7 |
6
|
anbi2d |
โข ( ๐ = ๐ โ ( ( ๐ โง ๐ โ ๐ ) โ ( ๐ โง ๐ โ ๐ ) ) ) |
8 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ๐ โ ๐ ) = ( ๐ โ ๐ ) ) |
9 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ( ๐บ โ ๐ ) โ ๐ ) = ( ( ๐บ โ ๐ ) โ ๐ ) ) |
10 |
9
|
sumeq2sdv |
โข ( ๐ = ๐ โ ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) = ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) |
11 |
10
|
oveq2d |
โข ( ๐ = ๐ โ ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) ) |
12 |
8 11
|
eqeq12d |
โข ( ๐ = ๐ โ ( ( ๐ โ ๐ ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) โ ( ๐ โ ๐ ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) ) ) |
13 |
7 12
|
imbi12d |
โข ( ๐ = ๐ โ ( ( ( ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐ ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) ) โ ( ( ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐ ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) ) ) ) |
14 |
|
fveq2 |
โข ( ๐ก = ๐ โ ( ( ๐บ โ ๐ ) โ ๐ก ) = ( ( ๐บ โ ๐ ) โ ๐ ) ) |
15 |
14
|
sumeq2sdv |
โข ( ๐ก = ๐ โ ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ก ) = ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) |
16 |
15
|
oveq2d |
โข ( ๐ก = ๐ โ ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ก ) ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) ) |
17 |
|
simpr |
โข ( ( ๐ โง ๐ โ ๐ ) โ ๐ โ ๐ ) |
18 |
3
|
nnrecred |
โข ( ๐ โ ( 1 / ๐ ) โ โ ) |
19 |
18
|
adantr |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( 1 / ๐ ) โ โ ) |
20 |
|
fzfid |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( 1 ... ๐ ) โ Fin ) |
21 |
1 4 5
|
stoweidlem15 |
โข ( ( ( ๐ โง ๐ โ ( 1 ... ๐ ) ) โง ๐ โ ๐ ) โ ( ( ( ๐บ โ ๐ ) โ ๐ ) โ โ โง 0 โค ( ( ๐บ โ ๐ ) โ ๐ ) โง ( ( ๐บ โ ๐ ) โ ๐ ) โค 1 ) ) |
22 |
21
|
simp1d |
โข ( ( ( ๐ โง ๐ โ ( 1 ... ๐ ) ) โง ๐ โ ๐ ) โ ( ( ๐บ โ ๐ ) โ ๐ ) โ โ ) |
23 |
22
|
an32s |
โข ( ( ( ๐ โง ๐ โ ๐ ) โง ๐ โ ( 1 ... ๐ ) ) โ ( ( ๐บ โ ๐ ) โ ๐ ) โ โ ) |
24 |
20 23
|
fsumrecl |
โข ( ( ๐ โง ๐ โ ๐ ) โ ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) โ โ ) |
25 |
19 24
|
remulcld |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) โ โ ) |
26 |
2 16 17 25
|
fvmptd3 |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐ ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) ) |
27 |
13 26
|
vtoclg |
โข ( ๐ โ ๐ โ ( ( ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐ ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) ) ) |
28 |
27
|
anabsi7 |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐ ) = ( ( 1 / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐บ โ ๐ ) โ ๐ ) ) ) |