Metamath Proof Explorer

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 ‘ 𝑥 ) ) ) ) )