Metamath Proof Explorer

Theorem efchpcl

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

Ref Expression
Assertion efchpcl 
|- ( A e. RR -> ( exp ` ( psi ` A ) ) e. NN )

Proof

Step Hyp Ref Expression
1 chpval 
 |-  ( A e. RR -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) )
2 1 fveq2d 
 |-  ( A e. RR -> ( exp ` ( psi ` A ) ) = ( exp ` sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) ) )
3 fzfid 
 |-  ( A e. RR -> ( 1 ... ( |_ ` A ) ) e. Fin )
4 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
5 4 adantl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
6 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
7 5 6 syl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` n ) e. RR )
8 efvmacl 
 |-  ( n e. NN -> ( exp ` ( Lam ` n ) ) e. NN )
9 5 8 syl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( exp ` ( Lam ` n ) ) e. NN )
10 3 7 9 efnnfsumcl 
 |-  ( A e. RR -> ( exp ` sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) ) e. NN )
11 2 10 eqeltrd 
 |-  ( A e. RR -> ( exp ` ( psi ` A ) ) e. NN )