Step |
Hyp |
Ref |
Expression |
1 |
|
df-cht |
|- theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) ) |
2 |
|
ppifi |
|- ( x e. RR -> ( ( 0 [,] x ) i^i Prime ) e. Fin ) |
3 |
|
simpr |
|- ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> p e. ( ( 0 [,] x ) i^i Prime ) ) |
4 |
3
|
elin2d |
|- ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> p e. Prime ) |
5 |
|
prmnn |
|- ( p e. Prime -> p e. NN ) |
6 |
4 5
|
syl |
|- ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> p e. NN ) |
7 |
6
|
nnrpd |
|- ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> p e. RR+ ) |
8 |
7
|
relogcld |
|- ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> ( log ` p ) e. RR ) |
9 |
2 8
|
fsumrecl |
|- ( x e. RR -> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) e. RR ) |
10 |
1 9
|
fmpti |
|- theta : RR --> RR |