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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐴 ) )