Theorem chpdifbnd

Description: A bound on the difference of nearby psi values. Theorem 10.5.2 of Shapiro, p. 427. (Contributed by Mario Carneiro, 25-May-2016)

	Ref	Expression
Assertion	chpdifbnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		selberg2b	⊢ ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝑏
2		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
3		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ∈ ℝ )
4		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ∈ ℝ )
5		0lt1	⊢ 0 < 1
6	5	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 1 )
7		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ≤ 𝐴 )
8	3 4 2 6 7	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 𝐴 )
9	2 8	elrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
10	9	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝑏 ) ) → 𝐴 ∈ ℝ+ )
11		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝑏 ) ) → 1 ≤ 𝐴 )
12		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝑏 ) ) → 𝑏 ∈ ℝ+ )
13		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝑏 ) ) → ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝑏 )
14		eqid	⊢ ( ( 𝑏 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ) = ( ( 𝑏 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) )
15	10 11 12 13 14	chpdifbndlem2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝑏 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝑏 ) ) → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
16	15	rexlimdvaa	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝑏 → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ) )
17	1 16	mpi	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )