MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chpdifbndlem1 Structured version   Visualization version   GIF version

Theorem chpdifbndlem1 25287
Description: Lemma for chpdifbnd 25289. (Contributed by Mario Carneiro, 25-May-2016.)
Hypotheses
Ref Expression
chpdifbnd.a (𝜑𝐴 ∈ ℝ+)
chpdifbnd.1 (𝜑 → 1 ≤ 𝐴)
chpdifbnd.b (𝜑𝐵 ∈ ℝ+)
chpdifbnd.2 (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)
chpdifbnd.c 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))
chpdifbnd.x (𝜑𝑋 ∈ (1(,)+∞))
chpdifbnd.y (𝜑𝑌 ∈ (𝑋[,](𝐴 · 𝑋)))
Assertion
Ref Expression
chpdifbndlem1 (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))))
Distinct variable groups:   𝑧,𝑚,𝐶   𝑧,𝑋   𝑧,𝑌   𝑧,𝐵
Allowed substitution hints:   𝜑(𝑧,𝑚)   𝐴(𝑧,𝑚)   𝐵(𝑚)   𝑋(𝑚)   𝑌(𝑚)

Proof of Theorem chpdifbndlem1
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 chpdifbnd.y . . . . . . . . 9 (𝜑𝑌 ∈ (𝑋[,](𝐴 · 𝑋)))
2 ioossre 12273 . . . . . . . . . . 11 (1(,)+∞) ⊆ ℝ
3 chpdifbnd.x . . . . . . . . . . 11 (𝜑𝑋 ∈ (1(,)+∞))
42, 3sseldi 3634 . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
5 chpdifbnd.a . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ+)
65rpred 11910 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
76, 4remulcld 10108 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝑋) ∈ ℝ)
8 elicc2 12276 . . . . . . . . . 10 ((𝑋 ∈ ℝ ∧ (𝐴 · 𝑋) ∈ ℝ) → (𝑌 ∈ (𝑋[,](𝐴 · 𝑋)) ↔ (𝑌 ∈ ℝ ∧ 𝑋𝑌𝑌 ≤ (𝐴 · 𝑋))))
94, 7, 8syl2anc 694 . . . . . . . . 9 (𝜑 → (𝑌 ∈ (𝑋[,](𝐴 · 𝑋)) ↔ (𝑌 ∈ ℝ ∧ 𝑋𝑌𝑌 ≤ (𝐴 · 𝑋))))
101, 9mpbid 222 . . . . . . . 8 (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋𝑌𝑌 ≤ (𝐴 · 𝑋)))
1110simp1d 1093 . . . . . . 7 (𝜑𝑌 ∈ ℝ)
12 chpcl 24895 . . . . . . 7 (𝑌 ∈ ℝ → (ψ‘𝑌) ∈ ℝ)
1311, 12syl 17 . . . . . 6 (𝜑 → (ψ‘𝑌) ∈ ℝ)
14 chpcl 24895 . . . . . . 7 (𝑋 ∈ ℝ → (ψ‘𝑋) ∈ ℝ)
154, 14syl 17 . . . . . 6 (𝜑 → (ψ‘𝑋) ∈ ℝ)
1613, 15resubcld 10496 . . . . 5 (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ∈ ℝ)
17 0red 10079 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
18 1re 10077 . . . . . . . . 9 1 ∈ ℝ
1918a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
20 0lt1 10588 . . . . . . . . 9 0 < 1
2120a1i 11 . . . . . . . 8 (𝜑 → 0 < 1)
22 eliooord 12271 . . . . . . . . . 10 (𝑋 ∈ (1(,)+∞) → (1 < 𝑋𝑋 < +∞))
233, 22syl 17 . . . . . . . . 9 (𝜑 → (1 < 𝑋𝑋 < +∞))
2423simpld 474 . . . . . . . 8 (𝜑 → 1 < 𝑋)
2517, 19, 4, 21, 24lttrd 10236 . . . . . . 7 (𝜑 → 0 < 𝑋)
264, 25elrpd 11907 . . . . . 6 (𝜑𝑋 ∈ ℝ+)
2726relogcld 24414 . . . . 5 (𝜑 → (log‘𝑋) ∈ ℝ)
2816, 27remulcld 10108 . . . 4 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ∈ ℝ)
29 2re 11128 . . . . . . 7 2 ∈ ℝ
3011, 4resubcld 10496 . . . . . . 7 (𝜑 → (𝑌𝑋) ∈ ℝ)
31 remulcl 10059 . . . . . . 7 ((2 ∈ ℝ ∧ (𝑌𝑋) ∈ ℝ) → (2 · (𝑌𝑋)) ∈ ℝ)
3229, 30, 31sylancr 696 . . . . . 6 (𝜑 → (2 · (𝑌𝑋)) ∈ ℝ)
3332, 27remulcld 10108 . . . . 5 (𝜑 → ((2 · (𝑌𝑋)) · (log‘𝑋)) ∈ ℝ)
34 chpdifbnd.b . . . . . . . 8 (𝜑𝐵 ∈ ℝ+)
3534rpred 11910 . . . . . . 7 (𝜑𝐵 ∈ ℝ)
3611, 4readdcld 10107 . . . . . . 7 (𝜑 → (𝑌 + 𝑋) ∈ ℝ)
3735, 36remulcld 10108 . . . . . 6 (𝜑 → (𝐵 · (𝑌 + 𝑋)) ∈ ℝ)
385relogcld 24414 . . . . . . . 8 (𝜑 → (log‘𝐴) ∈ ℝ)
39 remulcl 10059 . . . . . . . 8 ((2 ∈ ℝ ∧ (log‘𝐴) ∈ ℝ) → (2 · (log‘𝐴)) ∈ ℝ)
4029, 38, 39sylancr 696 . . . . . . 7 (𝜑 → (2 · (log‘𝐴)) ∈ ℝ)
4140, 11remulcld 10108 . . . . . 6 (𝜑 → ((2 · (log‘𝐴)) · 𝑌) ∈ ℝ)
4237, 41readdcld 10107 . . . . 5 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ∈ ℝ)
4333, 42readdcld 10107 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) ∈ ℝ)
44 chpdifbnd.c . . . . . . 7 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))
45 peano2re 10247 . . . . . . . . . 10 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
466, 45syl 17 . . . . . . . . 9 (𝜑 → (𝐴 + 1) ∈ ℝ)
4735, 46remulcld 10108 . . . . . . . 8 (𝜑 → (𝐵 · (𝐴 + 1)) ∈ ℝ)
48 remulcl 10059 . . . . . . . . . 10 ((2 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (2 · 𝐴) ∈ ℝ)
4929, 6, 48sylancr 696 . . . . . . . . 9 (𝜑 → (2 · 𝐴) ∈ ℝ)
5049, 38remulcld 10108 . . . . . . . 8 (𝜑 → ((2 · 𝐴) · (log‘𝐴)) ∈ ℝ)
5147, 50readdcld 10107 . . . . . . 7 (𝜑 → ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) ∈ ℝ)
5244, 51syl5eqel 2734 . . . . . 6 (𝜑𝐶 ∈ ℝ)
5352, 4remulcld 10108 . . . . 5 (𝜑 → (𝐶 · 𝑋) ∈ ℝ)
5433, 53readdcld 10107 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)) ∈ ℝ)
5513, 27remulcld 10108 . . . . . . 7 (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ∈ ℝ)
56 fzfid 12812 . . . . . . . 8 (𝜑 → (1...(⌊‘𝑋)) ∈ Fin)
5710simp2d 1094 . . . . . . . . . . . 12 (𝜑𝑋𝑌)
58 flword2 12654 . . . . . . . . . . . 12 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋𝑌) → (⌊‘𝑌) ∈ (ℤ‘(⌊‘𝑋)))
594, 11, 57, 58syl3anc 1366 . . . . . . . . . . 11 (𝜑 → (⌊‘𝑌) ∈ (ℤ‘(⌊‘𝑋)))
60 fzss2 12419 . . . . . . . . . . 11 ((⌊‘𝑌) ∈ (ℤ‘(⌊‘𝑋)) → (1...(⌊‘𝑋)) ⊆ (1...(⌊‘𝑌)))
6159, 60syl 17 . . . . . . . . . 10 (𝜑 → (1...(⌊‘𝑋)) ⊆ (1...(⌊‘𝑌)))
6261sselda 3636 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑋))) → 𝑛 ∈ (1...(⌊‘𝑌)))
63 elfznn 12408 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑌)) → 𝑛 ∈ ℕ)
6463adantl 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑛 ∈ ℕ)
65 vmacl 24889 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
6664, 65syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (Λ‘𝑛) ∈ ℝ)
67 nndivre 11094 . . . . . . . . . . . 12 ((𝑋 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑋 / 𝑛) ∈ ℝ)
684, 63, 67syl2an 493 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (𝑋 / 𝑛) ∈ ℝ)
69 chpcl 24895 . . . . . . . . . . 11 ((𝑋 / 𝑛) ∈ ℝ → (ψ‘(𝑋 / 𝑛)) ∈ ℝ)
7068, 69syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑋 / 𝑛)) ∈ ℝ)
7166, 70remulcld 10108 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ)
7262, 71syldan 486 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝑋))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ)
7356, 72fsumrecl 14509 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ)
7455, 73readdcld 10107 . . . . . 6 (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ∈ ℝ)
75 remulcl 10059 . . . . . . . . 9 ((2 ∈ ℝ ∧ (log‘𝑋) ∈ ℝ) → (2 · (log‘𝑋)) ∈ ℝ)
7629, 27, 75sylancr 696 . . . . . . . 8 (𝜑 → (2 · (log‘𝑋)) ∈ ℝ)
7776, 35resubcld 10496 . . . . . . 7 (𝜑 → ((2 · (log‘𝑋)) − 𝐵) ∈ ℝ)
7877, 4remulcld 10108 . . . . . 6 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) · 𝑋) ∈ ℝ)
795, 26rpmulcld 11926 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝑋) ∈ ℝ+)
8079relogcld 24414 . . . . . . . . 9 (𝜑 → (log‘(𝐴 · 𝑋)) ∈ ℝ)
81 remulcl 10059 . . . . . . . . 9 ((2 ∈ ℝ ∧ (log‘(𝐴 · 𝑋)) ∈ ℝ) → (2 · (log‘(𝐴 · 𝑋))) ∈ ℝ)
8229, 80, 81sylancr 696 . . . . . . . 8 (𝜑 → (2 · (log‘(𝐴 · 𝑋))) ∈ ℝ)
8335, 82readdcld 10107 . . . . . . 7 (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) ∈ ℝ)
8483, 11remulcld 10108 . . . . . 6 (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) ∈ ℝ)
8515, 27remulcld 10108 . . . . . . 7 (𝜑 → ((ψ‘𝑋) · (log‘𝑋)) ∈ ℝ)
8685, 73readdcld 10107 . . . . . 6 (𝜑 → (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ∈ ℝ)
8717, 4, 11, 25, 57ltletrd 10235 . . . . . . . . . . 11 (𝜑 → 0 < 𝑌)
8811, 87elrpd 11907 . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ+)
8988relogcld 24414 . . . . . . . . 9 (𝜑 → (log‘𝑌) ∈ ℝ)
9013, 89remulcld 10108 . . . . . . . 8 (𝜑 → ((ψ‘𝑌) · (log‘𝑌)) ∈ ℝ)
91 fzfid 12812 . . . . . . . . 9 (𝜑 → (1...(⌊‘𝑌)) ∈ Fin)
92 nndivre 11094 . . . . . . . . . . . 12 ((𝑌 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑌 / 𝑛) ∈ ℝ)
9311, 63, 92syl2an 493 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (𝑌 / 𝑛) ∈ ℝ)
94 chpcl 24895 . . . . . . . . . . 11 ((𝑌 / 𝑛) ∈ ℝ → (ψ‘(𝑌 / 𝑛)) ∈ ℝ)
9593, 94syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑌 / 𝑛)) ∈ ℝ)
9666, 95remulcld 10108 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))) ∈ ℝ)
9791, 96fsumrecl 14509 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))) ∈ ℝ)
9890, 97readdcld 10107 . . . . . . 7 (𝜑 → (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ∈ ℝ)
99 chpge0 24897 . . . . . . . . . 10 (𝑌 ∈ ℝ → 0 ≤ (ψ‘𝑌))
10011, 99syl 17 . . . . . . . . 9 (𝜑 → 0 ≤ (ψ‘𝑌))
10126, 88logled 24418 . . . . . . . . . 10 (𝜑 → (𝑋𝑌 ↔ (log‘𝑋) ≤ (log‘𝑌)))
10257, 101mpbid 222 . . . . . . . . 9 (𝜑 → (log‘𝑋) ≤ (log‘𝑌))
10327, 89, 13, 100, 102lemul2ad 11002 . . . . . . . 8 (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ≤ ((ψ‘𝑌) · (log‘𝑌)))
10491, 71fsumrecl 14509 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ)
105 vmage0 24892 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
10664, 105syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ (Λ‘𝑛))
107 chpge0 24897 . . . . . . . . . . . 12 ((𝑋 / 𝑛) ∈ ℝ → 0 ≤ (ψ‘(𝑋 / 𝑛)))
10868, 107syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ (ψ‘(𝑋 / 𝑛)))
10966, 70, 106, 108mulge0d 10642 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
11091, 71, 109, 61fsumless 14572 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
1114adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑋 ∈ ℝ)
11211adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑌 ∈ ℝ)
11364nnrpd 11908 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑛 ∈ ℝ+)
11457adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑋𝑌)
115111, 112, 113, 114lediv1dd 11968 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (𝑋 / 𝑛) ≤ (𝑌 / 𝑛))
116 chpwordi 24928 . . . . . . . . . . . 12 (((𝑋 / 𝑛) ∈ ℝ ∧ (𝑌 / 𝑛) ∈ ℝ ∧ (𝑋 / 𝑛) ≤ (𝑌 / 𝑛)) → (ψ‘(𝑋 / 𝑛)) ≤ (ψ‘(𝑌 / 𝑛)))
11768, 93, 115, 116syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑋 / 𝑛)) ≤ (ψ‘(𝑌 / 𝑛)))
11870, 95, 66, 106, 117lemul2ad 11002 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
11991, 71, 96, 118fsumle 14575 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
12073, 104, 97, 110, 119letrd 10232 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
12155, 73, 90, 97, 103, 120le2addd 10684 . . . . . . 7 (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ≤ (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))))
12298, 88rerpdivcld 11941 . . . . . . . . 9 (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ∈ ℝ)
123 remulcl 10059 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (2 · (log‘𝑌)) ∈ ℝ)
12429, 89, 123sylancr 696 . . . . . . . . . 10 (𝜑 → (2 · (log‘𝑌)) ∈ ℝ)
12535, 124readdcld 10107 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘𝑌))) ∈ ℝ)
126122, 124resubcld 10496 . . . . . . . . . . 11 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ∈ ℝ)
127126recnd 10106 . . . . . . . . . . . 12 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ∈ ℂ)
128127abscld 14219 . . . . . . . . . . 11 (𝜑 → (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ∈ ℝ)
129126leabsd 14197 . . . . . . . . . . 11 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤ (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))))
13019, 4, 24ltled 10223 . . . . . . . . . . . . . 14 (𝜑 → 1 ≤ 𝑋)
13119, 4, 11, 130, 57letrd 10232 . . . . . . . . . . . . 13 (𝜑 → 1 ≤ 𝑌)
132 elicopnf 12307 . . . . . . . . . . . . . 14 (1 ∈ ℝ → (𝑌 ∈ (1[,)+∞) ↔ (𝑌 ∈ ℝ ∧ 1 ≤ 𝑌)))
13318, 132ax-mp 5 . . . . . . . . . . . . 13 (𝑌 ∈ (1[,)+∞) ↔ (𝑌 ∈ ℝ ∧ 1 ≤ 𝑌))
13411, 131, 133sylanbrc 699 . . . . . . . . . . . 12 (𝜑𝑌 ∈ (1[,)+∞))
135 chpdifbnd.2 . . . . . . . . . . . 12 (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)
136 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑌 → (ψ‘𝑧) = (ψ‘𝑌))
137 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑌 → (log‘𝑧) = (log‘𝑌))
138136, 137oveq12d 6708 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑌 → ((ψ‘𝑧) · (log‘𝑧)) = ((ψ‘𝑌) · (log‘𝑌)))
139 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (Λ‘𝑚) = (Λ‘𝑛))
140 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 → (𝑧 / 𝑚) = (𝑧 / 𝑛))
141140fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (ψ‘(𝑧 / 𝑚)) = (ψ‘(𝑧 / 𝑛)))
142139, 141oveq12d 6708 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → ((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))))
143142cbvsumv 14470 . . . . . . . . . . . . . . . . . . 19 Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛)))
144 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑌 → (⌊‘𝑧) = (⌊‘𝑌))
145144oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑌 → (1...(⌊‘𝑧)) = (1...(⌊‘𝑌)))
146 simpl 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑌𝑛 ∈ (1...(⌊‘𝑌))) → 𝑧 = 𝑌)
147146oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑌𝑛 ∈ (1...(⌊‘𝑌))) → (𝑧 / 𝑛) = (𝑌 / 𝑛))
148147fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑌𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑧 / 𝑛)) = (ψ‘(𝑌 / 𝑛)))
149148oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑌𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
150145, 149sumeq12rdv 14482 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑌 → Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
151143, 150syl5eq 2697 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑌 → Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
152138, 151oveq12d 6708 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑌 → (((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) = (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))))
153 id 22 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑌𝑧 = 𝑌)
154152, 153oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑌 → ((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) = ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌))
155137oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑌 → (2 · (log‘𝑧)) = (2 · (log‘𝑌)))
156154, 155oveq12d 6708 . . . . . . . . . . . . . . 15 (𝑧 = 𝑌 → (((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧))) = (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))))
157156fveq2d 6233 . . . . . . . . . . . . . 14 (𝑧 = 𝑌 → (abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) = (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))))
158157breq1d 4695 . . . . . . . . . . . . 13 (𝑧 = 𝑌 → ((abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 ↔ (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵))
159158rspcv 3336 . . . . . . . . . . . 12 (𝑌 ∈ (1[,)+∞) → (∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 → (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵))
160134, 135, 159sylc 65 . . . . . . . . . . 11 (𝜑 → (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵)
161126, 128, 35, 129, 160letrd 10232 . . . . . . . . . 10 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤ 𝐵)
162122, 124, 35lesubaddd 10662 . . . . . . . . . 10 (𝜑 → ((((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤ 𝐵 ↔ ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘𝑌)))))
163161, 162mpbid 222 . . . . . . . . 9 (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘𝑌))))
16410simp3d 1095 . . . . . . . . . . . 12 (𝜑𝑌 ≤ (𝐴 · 𝑋))
16588, 79logled 24418 . . . . . . . . . . . 12 (𝜑 → (𝑌 ≤ (𝐴 · 𝑋) ↔ (log‘𝑌) ≤ (log‘(𝐴 · 𝑋))))
166164, 165mpbid 222 . . . . . . . . . . 11 (𝜑 → (log‘𝑌) ≤ (log‘(𝐴 · 𝑋)))
167 2pos 11150 . . . . . . . . . . . . . 14 0 < 2
16829, 167pm3.2i 470 . . . . . . . . . . . . 13 (2 ∈ ℝ ∧ 0 < 2)
169168a1i 11 . . . . . . . . . . . 12 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
170 lemul2 10914 . . . . . . . . . . . 12 (((log‘𝑌) ∈ ℝ ∧ (log‘(𝐴 · 𝑋)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((log‘𝑌) ≤ (log‘(𝐴 · 𝑋)) ↔ (2 · (log‘𝑌)) ≤ (2 · (log‘(𝐴 · 𝑋)))))
17189, 80, 169, 170syl3anc 1366 . . . . . . . . . . 11 (𝜑 → ((log‘𝑌) ≤ (log‘(𝐴 · 𝑋)) ↔ (2 · (log‘𝑌)) ≤ (2 · (log‘(𝐴 · 𝑋)))))
172166, 171mpbid 222 . . . . . . . . . 10 (𝜑 → (2 · (log‘𝑌)) ≤ (2 · (log‘(𝐴 · 𝑋))))
173124, 82, 35, 172leadd2dd 10680 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘𝑌))) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋)))))
174122, 125, 83, 163, 173letrd 10232 . . . . . . . 8 (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋)))))
17598, 83, 88ledivmul2d 11964 . . . . . . . 8 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) ↔ (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌)))
176174, 175mpbid 222 . . . . . . 7 (𝜑 → (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌))
17774, 98, 84, 121, 176letrd 10232 . . . . . 6 (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌))
178 elicopnf 12307 . . . . . . . . . . . 12 (1 ∈ ℝ → (𝑋 ∈ (1[,)+∞) ↔ (𝑋 ∈ ℝ ∧ 1 ≤ 𝑋)))
17918, 178ax-mp 5 . . . . . . . . . . 11 (𝑋 ∈ (1[,)+∞) ↔ (𝑋 ∈ ℝ ∧ 1 ≤ 𝑋))
1804, 130, 179sylanbrc 699 . . . . . . . . . 10 (𝜑𝑋 ∈ (1[,)+∞))
181 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑋 → (ψ‘𝑧) = (ψ‘𝑋))
182 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑋 → (log‘𝑧) = (log‘𝑋))
183181, 182oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑋 → ((ψ‘𝑧) · (log‘𝑧)) = ((ψ‘𝑋) · (log‘𝑋)))
184 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑋 → (⌊‘𝑧) = (⌊‘𝑋))
185184oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑋 → (1...(⌊‘𝑧)) = (1...(⌊‘𝑋)))
186 simpl 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑋𝑛 ∈ (1...(⌊‘𝑋))) → 𝑧 = 𝑋)
187186oveq1d 6705 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑋𝑛 ∈ (1...(⌊‘𝑋))) → (𝑧 / 𝑛) = (𝑋 / 𝑛))
188187fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = 𝑋𝑛 ∈ (1...(⌊‘𝑋))) → (ψ‘(𝑧 / 𝑛)) = (ψ‘(𝑋 / 𝑛)))
189188oveq2d 6706 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑋𝑛 ∈ (1...(⌊‘𝑋))) → ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
190185, 189sumeq12rdv 14482 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑋 → Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
191143, 190syl5eq 2697 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑋 → Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
192183, 191oveq12d 6708 . . . . . . . . . . . . . . 15 (𝑧 = 𝑋 → (((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) = (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))))
193 id 22 . . . . . . . . . . . . . . 15 (𝑧 = 𝑋𝑧 = 𝑋)
194192, 193oveq12d 6708 . . . . . . . . . . . . . 14 (𝑧 = 𝑋 → ((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) = ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋))
195182oveq2d 6706 . . . . . . . . . . . . . 14 (𝑧 = 𝑋 → (2 · (log‘𝑧)) = (2 · (log‘𝑋)))
196194, 195oveq12d 6708 . . . . . . . . . . . . 13 (𝑧 = 𝑋 → (((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧))) = (((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋))))
197196fveq2d 6233 . . . . . . . . . . . 12 (𝑧 = 𝑋 → (abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) = (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))))
198197breq1d 4695 . . . . . . . . . . 11 (𝑧 = 𝑋 → ((abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 ↔ (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵))
199198rspcv 3336 . . . . . . . . . 10 (𝑋 ∈ (1[,)+∞) → (∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 → (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵))
200180, 135, 199sylc 65 . . . . . . . . 9 (𝜑 → (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵)
20186, 26rerpdivcld 11941 . . . . . . . . . 10 (𝜑 → ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∈ ℝ)
202201, 76, 35absdifled 14217 . . . . . . . . 9 (𝜑 → ((abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵 ↔ (((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∧ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ≤ ((2 · (log‘𝑋)) + 𝐵))))
203200, 202mpbid 222 . . . . . . . 8 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∧ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ≤ ((2 · (log‘𝑋)) + 𝐵)))
204203simpld 474 . . . . . . 7 (𝜑 → ((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋))
20577, 86, 26lemuldivd 11959 . . . . . . 7 (𝜑 → ((((2 · (log‘𝑋)) − 𝐵) · 𝑋) ≤ (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ↔ ((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋)))
206204, 205mpbird 247 . . . . . 6 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) · 𝑋) ≤ (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))))
20774, 78, 84, 86, 177, 206le2subd 10685 . . . . 5 (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) ≤ (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋)))
20855recnd 10106 . . . . . . 7 (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ∈ ℂ)
20985recnd 10106 . . . . . . 7 (𝜑 → ((ψ‘𝑋) · (log‘𝑋)) ∈ ℂ)
21073recnd 10106 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℂ)
211208, 209, 210pnpcan2d 10468 . . . . . 6 (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) = (((ψ‘𝑌) · (log‘𝑋)) − ((ψ‘𝑋) · (log‘𝑋))))
21213recnd 10106 . . . . . . 7 (𝜑 → (ψ‘𝑌) ∈ ℂ)
21315recnd 10106 . . . . . . 7 (𝜑 → (ψ‘𝑋) ∈ ℂ)
21427recnd 10106 . . . . . . 7 (𝜑 → (log‘𝑋) ∈ ℂ)
215212, 213, 214subdird 10525 . . . . . 6 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) = (((ψ‘𝑌) · (log‘𝑋)) − ((ψ‘𝑋) · (log‘𝑋))))
216211, 215eqtr4d 2688 . . . . 5 (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) = (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)))
21776, 11remulcld 10108 . . . . . . . 8 (𝜑 → ((2 · (log‘𝑋)) · 𝑌) ∈ ℝ)
218217recnd 10106 . . . . . . 7 (𝜑 → ((2 · (log‘𝑋)) · 𝑌) ∈ ℂ)
21935, 40readdcld 10107 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘𝐴))) ∈ ℝ)
220219, 11remulcld 10108 . . . . . . . 8 (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) ∈ ℝ)
221220recnd 10106 . . . . . . 7 (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) ∈ ℂ)
22276, 4remulcld 10108 . . . . . . . 8 (𝜑 → ((2 · (log‘𝑋)) · 𝑋) ∈ ℝ)
223222recnd 10106 . . . . . . 7 (𝜑 → ((2 · (log‘𝑋)) · 𝑋) ∈ ℂ)
22435, 4remulcld 10108 . . . . . . . . 9 (𝜑 → (𝐵 · 𝑋) ∈ ℝ)
225224recnd 10106 . . . . . . . 8 (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
226225negcld 10417 . . . . . . 7 (𝜑 → -(𝐵 · 𝑋) ∈ ℂ)
227218, 221, 223, 226addsub4d 10477 . . . . . 6 (𝜑 → ((((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)) − (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋))) = ((((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)) + (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋))))
2285, 26relogmuld 24416 . . . . . . . . . . . . . 14 (𝜑 → (log‘(𝐴 · 𝑋)) = ((log‘𝐴) + (log‘𝑋)))
22938recnd 10106 . . . . . . . . . . . . . . 15 (𝜑 → (log‘𝐴) ∈ ℂ)
230229, 214addcomd 10276 . . . . . . . . . . . . . 14 (𝜑 → ((log‘𝐴) + (log‘𝑋)) = ((log‘𝑋) + (log‘𝐴)))
231228, 230eqtrd 2685 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝐴 · 𝑋)) = ((log‘𝑋) + (log‘𝐴)))
232231oveq2d 6706 . . . . . . . . . . . 12 (𝜑 → (2 · (log‘(𝐴 · 𝑋))) = (2 · ((log‘𝑋) + (log‘𝐴))))
233 2cnd 11131 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℂ)
234233, 214, 229adddid 10102 . . . . . . . . . . . 12 (𝜑 → (2 · ((log‘𝑋) + (log‘𝐴))) = ((2 · (log‘𝑋)) + (2 · (log‘𝐴))))
235232, 234eqtrd 2685 . . . . . . . . . . 11 (𝜑 → (2 · (log‘(𝐴 · 𝑋))) = ((2 · (log‘𝑋)) + (2 · (log‘𝐴))))
236235oveq2d 6706 . . . . . . . . . 10 (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) = (𝐵 + ((2 · (log‘𝑋)) + (2 · (log‘𝐴)))))
23735recnd 10106 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
23876recnd 10106 . . . . . . . . . . 11 (𝜑 → (2 · (log‘𝑋)) ∈ ℂ)
23940recnd 10106 . . . . . . . . . . 11 (𝜑 → (2 · (log‘𝐴)) ∈ ℂ)
240237, 238, 239add12d 10300 . . . . . . . . . 10 (𝜑 → (𝐵 + ((2 · (log‘𝑋)) + (2 · (log‘𝐴)))) = ((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))))
241236, 240eqtrd 2685 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) = ((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))))
242241oveq1d 6705 . . . . . . . 8 (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) = (((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))) · 𝑌))
243219recnd 10106 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘𝐴))) ∈ ℂ)
24411recnd 10106 . . . . . . . . 9 (𝜑𝑌 ∈ ℂ)
245238, 243, 244adddird 10103 . . . . . . . 8 (𝜑 → (((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))) · 𝑌) = (((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)))
246242, 245eqtrd 2685 . . . . . . 7 (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) = (((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)))
2474recnd 10106 . . . . . . . . 9 (𝜑𝑋 ∈ ℂ)
248238, 237, 247subdird 10525 . . . . . . . 8 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) · 𝑋) = (((2 · (log‘𝑋)) · 𝑋) − (𝐵 · 𝑋)))
249223, 225negsubd 10436 . . . . . . . 8 (𝜑 → (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋)) = (((2 · (log‘𝑋)) · 𝑋) − (𝐵 · 𝑋)))
250248, 249eqtr4d 2688 . . . . . . 7 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) · 𝑋) = (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋)))
251246, 250oveq12d 6708 . . . . . 6 (𝜑 → (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋)) = ((((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)) − (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋))))
25230recnd 10106 . . . . . . . . 9 (𝜑 → (𝑌𝑋) ∈ ℂ)
253233, 252, 214mul32d 10284 . . . . . . . 8 (𝜑 → ((2 · (𝑌𝑋)) · (log‘𝑋)) = ((2 · (log‘𝑋)) · (𝑌𝑋)))
254238, 244, 247subdid 10524 . . . . . . . 8 (𝜑 → ((2 · (log‘𝑋)) · (𝑌𝑋)) = (((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)))
255253, 254eqtrd 2685 . . . . . . 7 (𝜑 → ((2 · (𝑌𝑋)) · (log‘𝑋)) = (((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)))
25635, 11remulcld 10108 . . . . . . . . . . 11 (𝜑 → (𝐵 · 𝑌) ∈ ℝ)
257256recnd 10106 . . . . . . . . . 10 (𝜑 → (𝐵 · 𝑌) ∈ ℂ)
25841recnd 10106 . . . . . . . . . 10 (𝜑 → ((2 · (log‘𝐴)) · 𝑌) ∈ ℂ)
259257, 225, 258add32d 10301 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝑌) + (𝐵 · 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌)) + (𝐵 · 𝑋)))
260237, 244, 247adddid 10102 . . . . . . . . . 10 (𝜑 → (𝐵 · (𝑌 + 𝑋)) = ((𝐵 · 𝑌) + (𝐵 · 𝑋)))
261260oveq1d 6705 . . . . . . . . 9 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 · 𝑌) + (𝐵 · 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)))
262237, 239, 244adddird 10103 . . . . . . . . . 10 (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) = ((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌)))
263262oveq1d 6705 . . . . . . . . 9 (𝜑 → (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋)) = (((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌)) + (𝐵 · 𝑋)))
264259, 261, 2633eqtr4d 2695 . . . . . . . 8 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋)))
265221, 225subnegd 10437 . . . . . . . 8 (𝜑 → (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋)))
266264, 265eqtr4d 2688 . . . . . . 7 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋)))
267255, 266oveq12d 6708 . . . . . 6 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) = ((((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)) + (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋))))
268227, 251, 2673eqtr4d 2695 . . . . 5 (𝜑 → (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋)) = (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))))
269207, 216, 2683brtr3d 4716 . . . 4 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))))
27047, 4remulcld 10108 . . . . . . 7 (𝜑 → ((𝐵 · (𝐴 + 1)) · 𝑋) ∈ ℝ)
27150, 4remulcld 10108 . . . . . . 7 (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) ∈ ℝ)
27211, 7, 4, 164leadd1dd 10679 . . . . . . . . . 10 (𝜑 → (𝑌 + 𝑋) ≤ ((𝐴 · 𝑋) + 𝑋))
2736recnd 10106 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
27419recnd 10106 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
275273, 274, 247adddird 10103 . . . . . . . . . . 11 (𝜑 → ((𝐴 + 1) · 𝑋) = ((𝐴 · 𝑋) + (1 · 𝑋)))
276247mulid2d 10096 . . . . . . . . . . . 12 (𝜑 → (1 · 𝑋) = 𝑋)
277276oveq2d 6706 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝑋) + (1 · 𝑋)) = ((𝐴 · 𝑋) + 𝑋))
278275, 277eqtrd 2685 . . . . . . . . . 10 (𝜑 → ((𝐴 + 1) · 𝑋) = ((𝐴 · 𝑋) + 𝑋))
279272, 278breqtrrd 4713 . . . . . . . . 9 (𝜑 → (𝑌 + 𝑋) ≤ ((𝐴 + 1) · 𝑋))
28046, 4remulcld 10108 . . . . . . . . . 10 (𝜑 → ((𝐴 + 1) · 𝑋) ∈ ℝ)
28136, 280, 34lemul2d 11954 . . . . . . . . 9 (𝜑 → ((𝑌 + 𝑋) ≤ ((𝐴 + 1) · 𝑋) ↔ (𝐵 · (𝑌 + 𝑋)) ≤ (𝐵 · ((𝐴 + 1) · 𝑋))))
282279, 281mpbid 222 . . . . . . . 8 (𝜑 → (𝐵 · (𝑌 + 𝑋)) ≤ (𝐵 · ((𝐴 + 1) · 𝑋)))
28346recnd 10106 . . . . . . . . 9 (𝜑 → (𝐴 + 1) ∈ ℂ)
284237, 283, 247mulassd 10101 . . . . . . . 8 (𝜑 → ((𝐵 · (𝐴 + 1)) · 𝑋) = (𝐵 · ((𝐴 + 1) · 𝑋)))
285282, 284breqtrrd 4713 . . . . . . 7 (𝜑 → (𝐵 · (𝑌 + 𝑋)) ≤ ((𝐵 · (𝐴 + 1)) · 𝑋))
28629a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ)
287 0le2 11149 . . . . . . . . . . 11 0 ≤ 2
288287a1i 11 . . . . . . . . . 10 (𝜑 → 0 ≤ 2)
289 log1 24377 . . . . . . . . . . 11 (log‘1) = 0
290 chpdifbnd.1 . . . . . . . . . . . 12 (𝜑 → 1 ≤ 𝐴)
291 1rp 11874 . . . . . . . . . . . . 13 1 ∈ ℝ+
292 logleb 24394 . . . . . . . . . . . . 13 ((1 ∈ ℝ+𝐴 ∈ ℝ+) → (1 ≤ 𝐴 ↔ (log‘1) ≤ (log‘𝐴)))
293291, 5, 292sylancr 696 . . . . . . . . . . . 12 (𝜑 → (1 ≤ 𝐴 ↔ (log‘1) ≤ (log‘𝐴)))
294290, 293mpbid 222 . . . . . . . . . . 11 (𝜑 → (log‘1) ≤ (log‘𝐴))
295289, 294syl5eqbrr 4721 . . . . . . . . . 10 (𝜑 → 0 ≤ (log‘𝐴))
296286, 38, 288, 295mulge0d 10642 . . . . . . . . 9 (𝜑 → 0 ≤ (2 · (log‘𝐴)))
29711, 7, 40, 296, 164lemul2ad 11002 . . . . . . . 8 (𝜑 → ((2 · (log‘𝐴)) · 𝑌) ≤ ((2 · (log‘𝐴)) · (𝐴 · 𝑋)))
29849recnd 10106 . . . . . . . . . 10 (𝜑 → (2 · 𝐴) ∈ ℂ)
299298, 229, 247mulassd 10101 . . . . . . . . 9 (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) = ((2 · 𝐴) · ((log‘𝐴) · 𝑋)))
300233, 273, 229, 247mul4d 10286 . . . . . . . . 9 (𝜑 → ((2 · 𝐴) · ((log‘𝐴) · 𝑋)) = ((2 · (log‘𝐴)) · (𝐴 · 𝑋)))
301299, 300eqtrd 2685 . . . . . . . 8 (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) = ((2 · (log‘𝐴)) · (𝐴 · 𝑋)))
302297, 301breqtrrd 4713 . . . . . . 7 (𝜑 → ((2 · (log‘𝐴)) · 𝑌) ≤ (((2 · 𝐴) · (log‘𝐴)) · 𝑋))
30337, 41, 270, 271, 285, 302le2addd 10684 . . . . . 6 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ≤ (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋)))
30444oveq1i 6700 . . . . . . 7 (𝐶 · 𝑋) = (((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) · 𝑋)
30547recnd 10106 . . . . . . . 8 (𝜑 → (𝐵 · (𝐴 + 1)) ∈ ℂ)
30650recnd 10106 . . . . . . . 8 (𝜑 → ((2 · 𝐴) · (log‘𝐴)) ∈ ℂ)
307305, 306, 247adddird 10103 . . . . . . 7 (𝜑 → (((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) · 𝑋) = (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋)))
308304, 307syl5eq 2697 . . . . . 6 (𝜑 → (𝐶 · 𝑋) = (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋)))
309303, 308breqtrrd 4713 . . . . 5 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ≤ (𝐶 · 𝑋))
31042, 53, 33, 309leadd2dd 10680 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) ≤ (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)))
31128, 43, 54, 269, 310letrd 10232 . . 3 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)))
31232recnd 10106 . . . . 5 (𝜑 → (2 · (𝑌𝑋)) ∈ ℂ)
3134, 24rplogcld 24420 . . . . . . . 8 (𝜑 → (log‘𝑋) ∈ ℝ+)
3144, 313rerpdivcld 11941 . . . . . . 7 (𝜑 → (𝑋 / (log‘𝑋)) ∈ ℝ)
31552, 314remulcld 10108 . . . . . 6 (𝜑 → (𝐶 · (𝑋 / (log‘𝑋))) ∈ ℝ)
316315recnd 10106 . . . . 5 (𝜑 → (𝐶 · (𝑋 / (log‘𝑋))) ∈ ℂ)
317312, 316, 214adddird 10103 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)) = (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋))))
31852recnd 10106 . . . . . . 7 (𝜑𝐶 ∈ ℂ)
319314recnd 10106 . . . . . . 7 (𝜑 → (𝑋 / (log‘𝑋)) ∈ ℂ)
320318, 319, 214mulassd 10101 . . . . . 6 (𝜑 → ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋)) = (𝐶 · ((𝑋 / (log‘𝑋)) · (log‘𝑋))))
321313rpne0d 11915 . . . . . . . 8 (𝜑 → (log‘𝑋) ≠ 0)
322247, 214, 321divcan1d 10840 . . . . . . 7 (𝜑 → ((𝑋 / (log‘𝑋)) · (log‘𝑋)) = 𝑋)
323322oveq2d 6706 . . . . . 6 (𝜑 → (𝐶 · ((𝑋 / (log‘𝑋)) · (log‘𝑋))) = (𝐶 · 𝑋))
324320, 323eqtrd 2685 . . . . 5 (𝜑 → ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋)) = (𝐶 · 𝑋))
325324oveq2d 6706 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋))) = (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)))
326317, 325eqtrd 2685 . . 3 (𝜑 → (((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)) = (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)))
327311, 326breqtrrd 4713 . 2 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)))
32832, 315readdcld 10107 . . 3 (𝜑 → ((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) ∈ ℝ)
32916, 328, 313lemul1d 11953 . 2 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) ↔ (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋))))
330327, 329mpbird 247 1 (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wss 3607   class class class wbr 4685  cfv 5926  (class class class)co 6690  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109   < clt 10112  cle 10113  cmin 10304  -cneg 10305   / cdiv 10722  cn 11058  2c2 11108  cuz 11725  +crp 11870  (,)cioo 12213  [,)cico 12215  [,]cicc 12216  ...cfz 12364  cfl 12631  abscabs 14018  Σcsu 14460  logclog 24346  Λcvma 24863  ψcchp 24864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-vma 24869  df-chp 24870
This theorem is referenced by:  chpdifbndlem2  25288
  Copyright terms: Public domain W3C validator