Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
|- ( x = A -> ( 0 [,] x ) = ( 0 [,] A ) ) |
2 |
1
|
ineq1d |
|- ( x = A -> ( ( 0 [,] x ) i^i Prime ) = ( ( 0 [,] A ) i^i Prime ) ) |
3 |
2
|
sumeq1d |
|- ( x = A -> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) ) |
4 |
|
df-cht |
|- theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) ) |
5 |
|
sumex |
|- sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) e. _V |
6 |
3 4 5
|
fvmpt |
|- ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) ) |