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 ∈ x A ⁢ x ψ ⁡ y − ψ ⁡ x ≤ 2 ⁢ y − x + c ⁢ x log ⁡ x

Proof

Step Hyp Ref Expression
1 selberg2b ⊢ ∃ b ∈ ℝ + ∀ z ∈ 1 +∞ ψ ⁡ z ⁢ log ⁡ z + ∑ n = 1 z Λ ⁡ n ⁢ ψ ⁡ z n z − 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 = 1 z Λ ⁡ n ⁢ ψ ⁡ z n z − 2 ⁢ log ⁡ z ≤ b → A ∈ ℝ +
11 simplr ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ b ∈ ℝ + ∧ ∀ z ∈ 1 +∞ ψ ⁡ z ⁢ log ⁡ z + ∑ n = 1 z Λ ⁡ n ⁢ ψ ⁡ z n z − 2 ⁢ log ⁡ z ≤ b → 1 ≤ A
12 simprl ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ b ∈ ℝ + ∧ ∀ z ∈ 1 +∞ ψ ⁡ z ⁢ log ⁡ z + ∑ n = 1 z Λ ⁡ n ⁢ ψ ⁡ z n z − 2 ⁢ log ⁡ z ≤ b → b ∈ ℝ +
13 simprr ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ b ∈ ℝ + ∧ ∀ z ∈ 1 +∞ ψ ⁡ z ⁢ log ⁡ z + ∑ n = 1 z Λ ⁡ n ⁢ ψ ⁡ z n z − 2 ⁢ log ⁡ z ≤ b → ∀ z ∈ 1 +∞ ψ ⁡ z ⁢ log ⁡ z + ∑ n = 1 z Λ ⁡ n ⁢ ψ ⁡ z n z − 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 = 1 z Λ ⁡ n ⁢ ψ ⁡ z n z − 2 ⁢ log ⁡ z ≤ b → ∃ c ∈ ℝ + ∀ x ∈ 1 +∞ ∀ y ∈ x A ⁢ x ψ ⁡ y − ψ ⁡ x ≤ 2 ⁢ y − x + c ⁢ x log ⁡ x
16 15 rexlimdvaa ⊢ A ∈ ℝ ∧ 1 ≤ A → ∃ b ∈ ℝ + ∀ z ∈ 1 +∞ ψ ⁡ z ⁢ log ⁡ z + ∑ n = 1 z Λ ⁡ n ⁢ ψ ⁡ z n z − 2 ⁢ log ⁡ z ≤ b → ∃ c ∈ ℝ + ∀ x ∈ 1 +∞ ∀ y ∈ x A ⁢ x ψ ⁡ y − ψ ⁡ x ≤ 2 ⁢ y − x + c ⁢ x log ⁡ x
17 1 16 mpi ⊢ A ∈ ℝ ∧ 1 ≤ A → ∃ c ∈ ℝ + ∀ x ∈ 1 +∞ ∀ y ∈ x A ⁢ x ψ ⁡ y − ψ ⁡ x ≤ 2 ⁢ y − x + c ⁢ x log ⁡ x