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

Proof

Step Hyp Ref Expression
1 chtval ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
2 1 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( θ ‘ 𝐴 ) ) = ( exp ‘ Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) )
3 ppifi ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
4 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
5 4 elin2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
6 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
7 5 6 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
8 7 nnrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
9 8 relogcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
10 8 reeflogd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝑝 ) ) = 𝑝 )
11 10 7 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝑝 ) ) ∈ ℕ )
12 3 9 11 efnnfsumcl ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) ∈ ℕ )
13 2 12 eqeltrd ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( θ ‘ 𝐴 ) ) ∈ ℕ )