Theorem chpwordi

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

	Ref	Expression
Assertion	chpwordi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ψ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐵 ) )

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		flword2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝐴 ) ) )
9		fzss2	⊢ ( ( ⌊ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝐴 ) ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐵 ) ) )
10	8 9	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐵 ) ) )
11	1 5 7 10	fsumless	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐵 ) ) ( Λ ‘ 𝑛 ) )
12		chpval	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
13	12	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
14		chpval	⊢ ( 𝐵 ∈ ℝ → ( ψ ‘ 𝐵 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐵 ) ) ( Λ ‘ 𝑛 ) )
15	14	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ψ ‘ 𝐵 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐵 ) ) ( Λ ‘ 𝑛 ) )
16	11 13 15	3brtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ψ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐵 ) )