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

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