Metamath Proof Explorer

Theorem chpwordi

Description: The second Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Assertion chpwordi ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → ψ ⁡ A ≤ ψ ⁡ B

Proof

Step Hyp Ref Expression
1 fzfid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → 1 … B ∈ Fin
2 elfznn ⊢ n ∈ 1 … B → n ∈ ℕ
3 2 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B ∧ n ∈ 1 … B → n ∈ ℕ
4 vmacl ⊢ n ∈ ℕ → Λ ⁡ n ∈ ℝ
5 3 4 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B ∧ n ∈ 1 … B → Λ ⁡ n ∈ ℝ
6 vmage0 ⊢ n ∈ ℕ → 0 ≤ Λ ⁡ n
7 3 6 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B ∧ n ∈ 1 … B → 0 ≤ Λ ⁡ n
8 flword2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℤ ≥ A
9 fzss2 ⊢ B ∈ ℤ ≥ A → 1 … A ⊆ 1 … B
10 8 9 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → 1 … A ⊆ 1 … B
11 1 5 7 10 fsumless ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → ∑ n = 1 A Λ ⁡ n ≤ ∑ n = 1 B Λ ⁡ n
12 chpval ⊢ A ∈ ℝ → ψ ⁡ A = ∑ n = 1 A Λ ⁡ n
13 12 3ad2ant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → ψ ⁡ A = ∑ n = 1 A Λ ⁡ n
14 chpval ⊢ B ∈ ℝ → ψ ⁡ B = ∑ n = 1 B Λ ⁡ n
15 14 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → ψ ⁡ B = ∑ n = 1 B Λ ⁡ n
16 11 13 15 3brtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → ψ ⁡ A ≤ ψ ⁡ B