Step |
Hyp |
Ref |
Expression |
1 |
|
pntsval.1 |
โข ๐ = ( ๐ โ โ โฆ ฮฃ ๐ โ ( 1 ... ( โ โ ๐ ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) ) |
2 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ฮ โ ๐ ) = ( ฮ โ ๐ ) ) |
3 |
|
fveq2 |
โข ( ๐ = ๐ โ ( log โ ๐ ) = ( log โ ๐ ) ) |
4 |
|
oveq2 |
โข ( ๐ = ๐ โ ( ๐ / ๐ ) = ( ๐ / ๐ ) ) |
5 |
4
|
fveq2d |
โข ( ๐ = ๐ โ ( ฯ โ ( ๐ / ๐ ) ) = ( ฯ โ ( ๐ / ๐ ) ) ) |
6 |
3 5
|
oveq12d |
โข ( ๐ = ๐ โ ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) = ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) |
7 |
2 6
|
oveq12d |
โข ( ๐ = ๐ โ ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) = ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) ) |
8 |
7
|
cbvsumv |
โข ฮฃ ๐ โ ( 1 ... ( โ โ ๐ ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) = ฮฃ ๐ โ ( 1 ... ( โ โ ๐ ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) |
9 |
|
fveq2 |
โข ( ๐ = ๐ด โ ( โ โ ๐ ) = ( โ โ ๐ด ) ) |
10 |
9
|
oveq2d |
โข ( ๐ = ๐ด โ ( 1 ... ( โ โ ๐ ) ) = ( 1 ... ( โ โ ๐ด ) ) ) |
11 |
|
fvoveq1 |
โข ( ๐ = ๐ด โ ( ฯ โ ( ๐ / ๐ ) ) = ( ฯ โ ( ๐ด / ๐ ) ) ) |
12 |
11
|
oveq2d |
โข ( ๐ = ๐ด โ ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) = ( ( log โ ๐ ) + ( ฯ โ ( ๐ด / ๐ ) ) ) ) |
13 |
12
|
oveq2d |
โข ( ๐ = ๐ด โ ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) = ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ด / ๐ ) ) ) ) ) |
14 |
13
|
adantr |
โข ( ( ๐ = ๐ด โง ๐ โ ( 1 ... ( โ โ ๐ ) ) ) โ ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) = ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ด / ๐ ) ) ) ) ) |
15 |
10 14
|
sumeq12dv |
โข ( ๐ = ๐ด โ ฮฃ ๐ โ ( 1 ... ( โ โ ๐ ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) = ฮฃ ๐ โ ( 1 ... ( โ โ ๐ด ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ด / ๐ ) ) ) ) ) |
16 |
8 15
|
eqtrid |
โข ( ๐ = ๐ด โ ฮฃ ๐ โ ( 1 ... ( โ โ ๐ ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ / ๐ ) ) ) ) = ฮฃ ๐ โ ( 1 ... ( โ โ ๐ด ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ด / ๐ ) ) ) ) ) |
17 |
|
sumex |
โข ฮฃ ๐ โ ( 1 ... ( โ โ ๐ด ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ด / ๐ ) ) ) ) โ V |
18 |
16 1 17
|
fvmpt |
โข ( ๐ด โ โ โ ( ๐ โ ๐ด ) = ฮฃ ๐ โ ( 1 ... ( โ โ ๐ด ) ) ( ( ฮ โ ๐ ) ยท ( ( log โ ๐ ) + ( ฯ โ ( ๐ด / ๐ ) ) ) ) ) |