Theorem chpdifbndlem2

Description: Lemma for chpdifbnd . (Contributed by Mario Carneiro, 25-May-2016)

	Ref	Expression
Hypotheses	chpdifbnd.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	chpdifbnd.1	⊢ ( 𝜑 → 1 ≤ 𝐴 )
	chpdifbnd.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	chpdifbnd.2	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝐵 )
	chpdifbnd.c	⊢ 𝐶 = ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) )
Assertion	chpdifbndlem2	⊢ ( 𝜑 → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chpdifbnd.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		chpdifbnd.1	⊢ ( 𝜑 → 1 ≤ 𝐴 )
3		chpdifbnd.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4		chpdifbnd.2	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝐵 )
5		chpdifbnd.c	⊢ 𝐶 = ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) )
6		1rp	⊢ 1 ∈ ℝ+
7		rpaddcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ∈ ℝ+ ) → ( 𝐴 + 1 ) ∈ ℝ+ )
8	1 6 7	sylancl	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ+ )
9	3 8	rpmulcld	⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 + 1 ) ) ∈ ℝ+ )
10	9	rpred	⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 + 1 ) ) ∈ ℝ )
11		2rp	⊢ 2 ∈ ℝ+
12		rpmulcl	⊢ ( ( 2 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 2 · 𝐴 ) ∈ ℝ+ )
13	11 1 12	sylancr	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ+ )
14	13	rpred	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ )
15	1	relogcld	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
16	14 15	remulcld	⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ∈ ℝ )
17	10 16	readdcld	⊢ ( 𝜑 → ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
18	9	rpgt0d	⊢ ( 𝜑 → 0 < ( 𝐵 · ( 𝐴 + 1 ) ) )
19	13	rprege0d	⊢ ( 𝜑 → ( ( 2 · 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝐴 ) ) )
20		log1	⊢ ( log ‘ 1 ) = 0
21		logleb	⊢ ( ( 1 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
22	6 1 21	sylancr	⊢ ( 𝜑 → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
23	2 22	mpbid	⊢ ( 𝜑 → ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) )
24	20 23	eqbrtrrid	⊢ ( 𝜑 → 0 ≤ ( log ‘ 𝐴 ) )
25		mulge0	⊢ ( ( ( ( 2 · 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝐴 ) ) ∧ ( ( log ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( log ‘ 𝐴 ) ) ) → 0 ≤ ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) )
26	19 15 24 25	syl12anc	⊢ ( 𝜑 → 0 ≤ ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) )
27	10 16 18 26	addgtge0d	⊢ ( 𝜑 → 0 < ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ) )
28	17 27	elrpd	⊢ ( 𝜑 → ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ) ∈ ℝ+ )
29	5 28	eqeltrid	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
30	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ) ) → 𝐴 ∈ ℝ+ )
31	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ) ) → 1 ≤ 𝐴 )
32	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ) ) → 𝐵 ∈ ℝ+ )
33	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ) ) → ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝐵 )
34		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ) ) → 𝑥 ∈ ( 1 (,) +∞ ) )
35		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ) ) → 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) )
36	30 31 32 33 5 34 35	chpdifbndlem1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ) ) → ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝐶 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
37	36	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝐶 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
38		oveq1	⊢ ( 𝑐 = 𝐶 → ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( 𝐶 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) )
39	38	oveq2d	⊢ ( 𝑐 = 𝐶 → ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) = ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝐶 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
40	39	breq2d	⊢ ( 𝑐 = 𝐶 → ( ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ↔ ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝐶 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ) )
41	40	2ralbidv	⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝐶 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ) )
42	41	rspcev	⊢ ( ( 𝐶 ∈ ℝ+ ∧ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝐶 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ) → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
43	29 37 42	syl2anc	⊢ ( 𝜑 → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 𝐴 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑐 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )