Metamath Proof Explorer


Theorem efchtcl

Description: The Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 22-Sep-2014) (Revised by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion efchtcl
|- ( A e. RR -> ( exp ` ( theta ` A ) ) e. NN )

Proof

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 )