Metamath Proof Explorer

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 ⊢A∈ℝ∧1≤A→∃c∈ℝ+∀x∈1+∞∀y∈xA⁢xψ⁡y−ψ⁡x≤2⁢y−x+c⁢xlog⁡x

Proof

Step Hyp Ref Expression
1 selberg2b ⊢∃b∈ℝ+∀z∈1+∞ψ⁡z⁢log⁡z+∑n=1zΛ⁡n⁢ψ⁡znz−2⁢log⁡z≤b
2 simpl ⊢A∈ℝ∧1≤A→A∈ℝ
3 0red ⊢A∈ℝ∧1≤A→0∈ℝ
4 1red ⊢A∈ℝ∧1≤A→1∈ℝ
5 0lt1 ⊢0<1
6 5 a1i ⊢A∈ℝ∧1≤A→0<1
7 simpr ⊢A∈ℝ∧1≤A→1≤A
8 3 4 2 6 7 ltletrd ⊢A∈ℝ∧1≤A→0<A
9 2 8 elrpd ⊢A∈ℝ∧1≤A→A∈ℝ+
10 9 adantr ⊢A∈ℝ∧1≤A∧b∈ℝ+∧∀z∈1+∞ψ⁡z⁢log⁡z+∑n=1zΛ⁡n⁢ψ⁡znz−2⁢log⁡z≤b→A∈ℝ+
11 simplr ⊢A∈ℝ∧1≤A∧b∈ℝ+∧∀z∈1+∞ψ⁡z⁢log⁡z+∑n=1zΛ⁡n⁢ψ⁡znz−2⁢log⁡z≤b→1≤A
12 simprl ⊢A∈ℝ∧1≤A∧b∈ℝ+∧∀z∈1+∞ψ⁡z⁢log⁡z+∑n=1zΛ⁡n⁢ψ⁡znz−2⁢log⁡z≤b→b∈ℝ+
13 simprr ⊢A∈ℝ∧1≤A∧b∈ℝ+∧∀z∈1+∞ψ⁡z⁢log⁡z+∑n=1zΛ⁡n⁢ψ⁡znz−2⁢log⁡z≤b→∀z∈1+∞ψ⁡z⁢log⁡z+∑n=1zΛ⁡n⁢ψ⁡znz−2⁢log⁡z≤b
14 eqid ⊢b⁢A+1+2⁢A⁢log⁡A=b⁢A+1+2⁢A⁢log⁡A
15 10 11 12 13 14 chpdifbndlem2 ⊢A∈ℝ∧1≤A∧b∈ℝ+∧∀z∈1+∞ψ⁡z⁢log⁡z+∑n=1zΛ⁡n⁢ψ⁡znz−2⁢log⁡z≤b→∃c∈ℝ+∀x∈1+∞∀y∈xA⁢xψ⁡y−ψ⁡x≤2⁢y−x+c⁢xlog⁡x
16 15 rexlimdvaa ⊢A∈ℝ∧1≤A→∃b∈ℝ+∀z∈1+∞ψ⁡z⁢log⁡z+∑n=1zΛ⁡n⁢ψ⁡znz−2⁢log⁡z≤b→∃c∈ℝ+∀x∈1+∞∀y∈xA⁢xψ⁡y−ψ⁡x≤2⁢y−x+c⁢xlog⁡x
17 1 16 mpi ⊢A∈ℝ∧1≤A→∃c∈ℝ+∀x∈1+∞∀y∈xA⁢xψ⁡y−ψ⁡x≤2⁢y−x+c⁢xlog⁡x