This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )