Step |
Hyp |
Ref |
Expression |
1 |
|
chtval |
|- ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) ) |
2 |
1
|
fveq2d |
|- ( A e. RR -> ( exp ` ( theta ` A ) ) = ( exp ` sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) ) ) |
3 |
|
ppifi |
|- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin ) |
4 |
|
simpr |
|- ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ( 0 [,] A ) i^i Prime ) ) |
5 |
4
|
elin2d |
|- ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. Prime ) |
6 |
|
prmnn |
|- ( p e. Prime -> p e. NN ) |
7 |
5 6
|
syl |
|- ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. NN ) |
8 |
7
|
nnrpd |
|- ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR+ ) |
9 |
8
|
relogcld |
|- ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR ) |
10 |
8
|
reeflogd |
|- ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( exp ` ( log ` p ) ) = p ) |
11 |
10 7
|
eqeltrd |
|- ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( exp ` ( log ` p ) ) e. NN ) |
12 |
3 9 11
|
efnnfsumcl |
|- ( A e. RR -> ( exp ` sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) ) e. NN ) |
13 |
2 12
|
eqeltrd |
|- ( A e. RR -> ( exp ` ( theta ` A ) ) e. NN ) |