Theorem chtlepsi

Description: The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	chtlepsi	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( 𝐴 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
2		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
3	2	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
4		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
5	3 4	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
6		vmage0	⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
7	3 6	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
8		ppisval	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
9		inss1	⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) )
10		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
11		fzss1	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
12	10 11	mp1i	⊢ ( 𝐴 ∈ ℝ → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
13	9 12	sstrid	⊢ ( 𝐴 ∈ ℝ → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
14	8 13	eqsstrd	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
15	1 5 7 14	fsumless	⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( Λ ‘ 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
16		chtval	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑛 ) )
17		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
18	17	elin2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑛 ∈ ℙ )
19		vmaprm	⊢ ( 𝑛 ∈ ℙ → ( Λ ‘ 𝑛 ) = ( log ‘ 𝑛 ) )
20	18 19	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( Λ ‘ 𝑛 ) = ( log ‘ 𝑛 ) )
21	20	sumeq2dv	⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( Λ ‘ 𝑛 ) = Σ 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑛 ) )
22	16 21	eqtr4d	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑛 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( Λ ‘ 𝑛 ) )
23		chpval	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
24	15 22 23	3brtr4d	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐴 ) )