Metamath Proof Explorer

Theorem chtwordi

Description: The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chtwordi ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ 𝐴 ) ≤ ( θ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
2 ppifi ⊢ ( 𝐵 ∈ ℝ → ( ( 0 [,] 𝐵 ) ∩ ℙ ) ∈ Fin )
3 1 2 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 0 [,] 𝐵 ) ∩ ℙ ) ∈ Fin )
4 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) )
5 4 elin2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
6 prmuz2 ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
7 5 6 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
8 eluz2b2 ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
9 7 8 sylib ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
10 9 simpld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
11 10 nnred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
12 9 simprd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → 1 < 𝑝 )
13 11 12 rplogcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
14 13 rpred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
15 13 rpge0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) → 0 ≤ ( log ‘ 𝑝 ) )
16 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 0 ∈ ℝ )
17 0le0 ⊢ 0 ≤ 0
18 17 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 0 ≤ 0 )
19 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
20 iccss ⊢ ( ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 0 [,] 𝐴 ) ⊆ ( 0 [,] 𝐵 ) )
21 16 1 18 19 20 syl22anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 0 [,] 𝐴 ) ⊆ ( 0 [,] 𝐵 ) )
22 21 ssrind ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( ( 0 [,] 𝐵 ) ∩ ℙ ) )
23 3 14 15 22 fsumless ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ≤ Σ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
24 chtval ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
25 24 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
26 chtval ⊢ ( 𝐵 ∈ ℝ → ( θ ‘ 𝐵 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
27 1 26 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ 𝐵 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
28 23 25 27 3brtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ 𝐴 ) ≤ ( θ ‘ 𝐵 ) )