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