Theorem efchpcl

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

	Ref	Expression
Assertion	efchpcl	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( ψ ‘ 𝐴 ) ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		chpval	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
2	1	fveq2d	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( ψ ‘ 𝐴 ) ) = ( exp ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) ) )
3		fzfid	⊢ ( 𝐴 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
4		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
6		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
7	5 6	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
8		efvmacl	⊢ ( 𝑛 ∈ ℕ → ( exp ‘ ( Λ ‘ 𝑛 ) ) ∈ ℕ )
9	5 8	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( exp ‘ ( Λ ‘ 𝑛 ) ) ∈ ℕ )
10	3 7 9	efnnfsumcl	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) ) ∈ ℕ )
11	2 10	eqeltrd	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( ψ ‘ 𝐴 ) ) ∈ ℕ )