Theorem chtge0

Description: The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	chtge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( θ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ppifi	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
2		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
3	2	elin2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
4		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
5	3 4	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
6		eluz2b2	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
7	5 6	sylib	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
8	7	simpld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
9	8	nnrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
10	9	relogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
11	8	nnred	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
12	7	simprd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝑝 )
13	11 12	rplogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
14	13	rpge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ≤ ( log ‘ 𝑝 ) )
15	1 10 14	fsumge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
16		chtval	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
17	15 16	breqtrrd	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( θ ‘ 𝐴 ) )