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 ( 𝐴 ∈ ℝ → ( 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 ‘ ( ψ ‘ 𝐴 ) ) ∈ ℕ )