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

Theorem chpdifbndlem1 24986
Description: Lemma for chpdifbnd 24988. (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 12064 . . . . . . . . . . 11 (1(,)+∞) ⊆ ℝ
3 chpdifbnd.x . . . . . . . . . . 11 (𝜑𝑋 ∈ (1(,)+∞))
42, 3sseldi 3565 . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
5 chpdifbnd.a . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ+)
65rpred 11706 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
76, 4remulcld 9926 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝑋) ∈ ℝ)
8 elicc2 12067 . . . . . . . . . 10 ((𝑋 ∈ ℝ ∧ (𝐴 · 𝑋) ∈ ℝ) → (𝑌 ∈ (𝑋[,](𝐴 · 𝑋)) ↔ (𝑌 ∈ ℝ ∧ 𝑋𝑌𝑌 ≤ (𝐴 · 𝑋))))
94, 7, 8syl2anc 690 . . . . . . . . 9 (𝜑 → (𝑌 ∈ (𝑋[,](𝐴 · 𝑋)) ↔ (𝑌 ∈ ℝ ∧ 𝑋𝑌𝑌 ≤ (𝐴 · 𝑋))))
101, 9mpbid 220 . . . . . . . 8 (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋𝑌𝑌 ≤ (𝐴 · 𝑋)))
1110simp1d 1065 . . . . . . 7 (𝜑𝑌 ∈ ℝ)
12 chpcl 24594 . . . . . . 7 (𝑌 ∈ ℝ → (ψ‘𝑌) ∈ ℝ)
1311, 12syl 17 . . . . . 6 (𝜑 → (ψ‘𝑌) ∈ ℝ)
14 chpcl 24594 . . . . . . 7 (𝑋 ∈ ℝ → (ψ‘𝑋) ∈ ℝ)
154, 14syl 17 . . . . . 6 (𝜑 → (ψ‘𝑋) ∈ ℝ)
1613, 15resubcld 10309 . . . . 5 (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ∈ ℝ)
17 0red 9897 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
18 1re 9895 . . . . . . . . 9 1 ∈ ℝ
1918a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
20 0lt1 10401 . . . . . . . . 9 0 < 1
2120a1i 11 . . . . . . . 8 (𝜑 → 0 < 1)
22 eliooord 12062 . . . . . . . . . 10 (𝑋 ∈ (1(,)+∞) → (1 < 𝑋𝑋 < +∞))
233, 22syl 17 . . . . . . . . 9 (𝜑 → (1 < 𝑋𝑋 < +∞))
2423simpld 473 . . . . . . . 8 (𝜑 → 1 < 𝑋)
2517, 19, 4, 21, 24lttrd 10049 . . . . . . 7 (𝜑 → 0 < 𝑋)
264, 25elrpd 11703 . . . . . 6 (𝜑𝑋 ∈ ℝ+)
2726relogcld 24117 . . . . 5 (𝜑 → (log‘𝑋) ∈ ℝ)
2816, 27remulcld 9926 . . . 4 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ∈ ℝ)
29 2re 10939 . . . . . . 7 2 ∈ ℝ
3011, 4resubcld 10309 . . . . . . 7 (𝜑 → (𝑌𝑋) ∈ ℝ)
31 remulcl 9877 . . . . . . 7 ((2 ∈ ℝ ∧ (𝑌𝑋) ∈ ℝ) → (2 · (𝑌𝑋)) ∈ ℝ)
3229, 30, 31sylancr 693 . . . . . 6 (𝜑 → (2 · (𝑌𝑋)) ∈ ℝ)
3332, 27remulcld 9926 . . . . 5 (𝜑 → ((2 · (𝑌𝑋)) · (log‘𝑋)) ∈ ℝ)
34 chpdifbnd.b . . . . . . . 8 (𝜑𝐵 ∈ ℝ+)
3534rpred 11706 . . . . . . 7 (𝜑𝐵 ∈ ℝ)
3611, 4readdcld 9925 . . . . . . 7 (𝜑 → (𝑌 + 𝑋) ∈ ℝ)
3735, 36remulcld 9926 . . . . . 6 (𝜑 → (𝐵 · (𝑌 + 𝑋)) ∈ ℝ)
385relogcld 24117 . . . . . . . 8 (𝜑 → (log‘𝐴) ∈ ℝ)
39 remulcl 9877 . . . . . . . 8 ((2 ∈ ℝ ∧ (log‘𝐴) ∈ ℝ) → (2 · (log‘𝐴)) ∈ ℝ)
4029, 38, 39sylancr 693 . . . . . . 7 (𝜑 → (2 · (log‘𝐴)) ∈ ℝ)
4140, 11remulcld 9926 . . . . . 6 (𝜑 → ((2 · (log‘𝐴)) · 𝑌) ∈ ℝ)
4237, 41readdcld 9925 . . . . 5 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ∈ ℝ)
4333, 42readdcld 9925 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) ∈ ℝ)
44 chpdifbnd.c . . . . . . 7 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))
45 peano2re 10060 . . . . . . . . . 10 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
466, 45syl 17 . . . . . . . . 9 (𝜑 → (𝐴 + 1) ∈ ℝ)
4735, 46remulcld 9926 . . . . . . . 8 (𝜑 → (𝐵 · (𝐴 + 1)) ∈ ℝ)
48 remulcl 9877 . . . . . . . . . 10 ((2 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (2 · 𝐴) ∈ ℝ)
4929, 6, 48sylancr 693 . . . . . . . . 9 (𝜑 → (2 · 𝐴) ∈ ℝ)
5049, 38remulcld 9926 . . . . . . . 8 (𝜑 → ((2 · 𝐴) · (log‘𝐴)) ∈ ℝ)
5147, 50readdcld 9925 . . . . . . 7 (𝜑 → ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) ∈ ℝ)
5244, 51syl5eqel 2691 . . . . . 6 (𝜑𝐶 ∈ ℝ)
5352, 4remulcld 9926 . . . . 5 (𝜑 → (𝐶 · 𝑋) ∈ ℝ)
5433, 53readdcld 9925 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)) ∈ ℝ)
5513, 27remulcld 9926 . . . . . . 7 (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ∈ ℝ)
56 fzfid 12591 . . . . . . . 8 (𝜑 → (1...(⌊‘𝑋)) ∈ Fin)
5710simp2d 1066 . . . . . . . . . . . 12 (𝜑𝑋𝑌)
58 flword2 12433 . . . . . . . . . . . 12 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋𝑌) → (⌊‘𝑌) ∈ (ℤ‘(⌊‘𝑋)))
594, 11, 57, 58syl3anc 1317 . . . . . . . . . . 11 (𝜑 → (⌊‘𝑌) ∈ (ℤ‘(⌊‘𝑋)))
60 fzss2 12209 . . . . . . . . . . 11 ((⌊‘𝑌) ∈ (ℤ‘(⌊‘𝑋)) → (1...(⌊‘𝑋)) ⊆ (1...(⌊‘𝑌)))
6159, 60syl 17 . . . . . . . . . 10 (𝜑 → (1...(⌊‘𝑋)) ⊆ (1...(⌊‘𝑌)))
6261sselda 3567 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑋))) → 𝑛 ∈ (1...(⌊‘𝑌)))
63 elfznn 12198 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑌)) → 𝑛 ∈ ℕ)
6463adantl 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑛 ∈ ℕ)
65 vmacl 24588 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
6664, 65syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (Λ‘𝑛) ∈ ℝ)
67 nndivre 10905 . . . . . . . . . . . 12 ((𝑋 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑋 / 𝑛) ∈ ℝ)
684, 63, 67syl2an 492 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (𝑋 / 𝑛) ∈ ℝ)
69 chpcl 24594 . . . . . . . . . . 11 ((𝑋 / 𝑛) ∈ ℝ → (ψ‘(𝑋 / 𝑛)) ∈ ℝ)
7068, 69syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑋 / 𝑛)) ∈ ℝ)
7166, 70remulcld 9926 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ)
7262, 71syldan 485 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝑋))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ)
7356, 72fsumrecl 14260 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ)
7455, 73readdcld 9925 . . . . . 6 (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ∈ ℝ)
75 remulcl 9877 . . . . . . . . 9 ((2 ∈ ℝ ∧ (log‘𝑋) ∈ ℝ) → (2 · (log‘𝑋)) ∈ ℝ)
7629, 27, 75sylancr 693 . . . . . . . 8 (𝜑 → (2 · (log‘𝑋)) ∈ ℝ)
7776, 35resubcld 10309 . . . . . . 7 (𝜑 → ((2 · (log‘𝑋)) − 𝐵) ∈ ℝ)
7877, 4remulcld 9926 . . . . . 6 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) · 𝑋) ∈ ℝ)
795, 26rpmulcld 11722 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝑋) ∈ ℝ+)
8079relogcld 24117 . . . . . . . . 9 (𝜑 → (log‘(𝐴 · 𝑋)) ∈ ℝ)
81 remulcl 9877 . . . . . . . . 9 ((2 ∈ ℝ ∧ (log‘(𝐴 · 𝑋)) ∈ ℝ) → (2 · (log‘(𝐴 · 𝑋))) ∈ ℝ)
8229, 80, 81sylancr 693 . . . . . . . 8 (𝜑 → (2 · (log‘(𝐴 · 𝑋))) ∈ ℝ)
8335, 82readdcld 9925 . . . . . . 7 (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) ∈ ℝ)
8483, 11remulcld 9926 . . . . . 6 (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) ∈ ℝ)
8515, 27remulcld 9926 . . . . . . 7 (𝜑 → ((ψ‘𝑋) · (log‘𝑋)) ∈ ℝ)
8685, 73readdcld 9925 . . . . . 6 (𝜑 → (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ∈ ℝ)
8717, 4, 11, 25, 57ltletrd 10048 . . . . . . . . . . 11 (𝜑 → 0 < 𝑌)
8811, 87elrpd 11703 . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ+)
8988relogcld 24117 . . . . . . . . 9 (𝜑 → (log‘𝑌) ∈ ℝ)
9013, 89remulcld 9926 . . . . . . . 8 (𝜑 → ((ψ‘𝑌) · (log‘𝑌)) ∈ ℝ)
91 fzfid 12591 . . . . . . . . 9 (𝜑 → (1...(⌊‘𝑌)) ∈ Fin)
92 nndivre 10905 . . . . . . . . . . . 12 ((𝑌 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑌 / 𝑛) ∈ ℝ)
9311, 63, 92syl2an 492 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (𝑌 / 𝑛) ∈ ℝ)
94 chpcl 24594 . . . . . . . . . . 11 ((𝑌 / 𝑛) ∈ ℝ → (ψ‘(𝑌 / 𝑛)) ∈ ℝ)
9593, 94syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑌 / 𝑛)) ∈ ℝ)
9666, 95remulcld 9926 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))) ∈ ℝ)
9791, 96fsumrecl 14260 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))) ∈ ℝ)
9890, 97readdcld 9925 . . . . . . 7 (𝜑 → (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ∈ ℝ)
99 chpge0 24596 . . . . . . . . . 10 (𝑌 ∈ ℝ → 0 ≤ (ψ‘𝑌))
10011, 99syl 17 . . . . . . . . 9 (𝜑 → 0 ≤ (ψ‘𝑌))
10126, 88logled 24121 . . . . . . . . . 10 (𝜑 → (𝑋𝑌 ↔ (log‘𝑋) ≤ (log‘𝑌)))
10257, 101mpbid 220 . . . . . . . . 9 (𝜑 → (log‘𝑋) ≤ (log‘𝑌))
10327, 89, 13, 100, 102lemul2ad 10815 . . . . . . . 8 (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ≤ ((ψ‘𝑌) · (log‘𝑌)))
10491, 71fsumrecl 14260 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ)
105 vmage0 24591 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
10664, 105syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ (Λ‘𝑛))
107 chpge0 24596 . . . . . . . . . . . 12 ((𝑋 / 𝑛) ∈ ℝ → 0 ≤ (ψ‘(𝑋 / 𝑛)))
10868, 107syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ (ψ‘(𝑋 / 𝑛)))
10966, 70, 106, 108mulge0d 10455 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
11091, 71, 109, 61fsumless 14317 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
1114adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑋 ∈ ℝ)
11211adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑌 ∈ ℝ)
11364nnrpd 11704 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑛 ∈ ℝ+)
11457adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → 𝑋𝑌)
115111, 112, 113, 114lediv1dd 11764 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (𝑋 / 𝑛) ≤ (𝑌 / 𝑛))
116 chpwordi 24627 . . . . . . . . . . . 12 (((𝑋 / 𝑛) ∈ ℝ ∧ (𝑌 / 𝑛) ∈ ℝ ∧ (𝑋 / 𝑛) ≤ (𝑌 / 𝑛)) → (ψ‘(𝑋 / 𝑛)) ≤ (ψ‘(𝑌 / 𝑛)))
11768, 93, 115, 116syl3anc 1317 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑋 / 𝑛)) ≤ (ψ‘(𝑌 / 𝑛)))
11870, 95, 66, 106, 117lemul2ad 10815 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
11991, 71, 96, 118fsumle 14320 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
12073, 104, 97, 110, 119letrd 10045 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
12155, 73, 90, 97, 103, 120le2addd 10497 . . . . . . 7 (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ≤ (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))))
12298, 88rerpdivcld 11737 . . . . . . . . 9 (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ∈ ℝ)
123 remulcl 9877 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (2 · (log‘𝑌)) ∈ ℝ)
12429, 89, 123sylancr 693 . . . . . . . . . 10 (𝜑 → (2 · (log‘𝑌)) ∈ ℝ)
12535, 124readdcld 9925 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘𝑌))) ∈ ℝ)
126122, 124resubcld 10309 . . . . . . . . . . 11 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ∈ ℝ)
127126recnd 9924 . . . . . . . . . . . 12 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ∈ ℂ)
128127abscld 13971 . . . . . . . . . . 11 (𝜑 → (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ∈ ℝ)
129126leabsd 13949 . . . . . . . . . . 11 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤ (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))))
13019, 4, 24ltled 10036 . . . . . . . . . . . . . 14 (𝜑 → 1 ≤ 𝑋)
13119, 4, 11, 130, 57letrd 10045 . . . . . . . . . . . . 13 (𝜑 → 1 ≤ 𝑌)
132 elicopnf 12098 . . . . . . . . . . . . . 14 (1 ∈ ℝ → (𝑌 ∈ (1[,)+∞) ↔ (𝑌 ∈ ℝ ∧ 1 ≤ 𝑌)))
13318, 132ax-mp 5 . . . . . . . . . . . . 13 (𝑌 ∈ (1[,)+∞) ↔ (𝑌 ∈ ℝ ∧ 1 ≤ 𝑌))
13411, 131, 133sylanbrc 694 . . . . . . . . . . . 12 (𝜑𝑌 ∈ (1[,)+∞))
135 chpdifbnd.2 . . . . . . . . . . . 12 (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)
136 fveq2 6087 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑌 → (ψ‘𝑧) = (ψ‘𝑌))
137 fveq2 6087 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑌 → (log‘𝑧) = (log‘𝑌))
138136, 137oveq12d 6544 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑌 → ((ψ‘𝑧) · (log‘𝑧)) = ((ψ‘𝑌) · (log‘𝑌)))
139 fveq2 6087 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (Λ‘𝑚) = (Λ‘𝑛))
140 oveq2 6534 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 → (𝑧 / 𝑚) = (𝑧 / 𝑛))
141140fveq2d 6091 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (ψ‘(𝑧 / 𝑚)) = (ψ‘(𝑧 / 𝑛)))
142139, 141oveq12d 6544 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → ((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))))
143142cbvsumv 14222 . . . . . . . . . . . . . . . . . . 19 Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛)))
144 fveq2 6087 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑌 → (⌊‘𝑧) = (⌊‘𝑌))
145144oveq2d 6542 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑌 → (1...(⌊‘𝑧)) = (1...(⌊‘𝑌)))
146 simpl 471 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑌𝑛 ∈ (1...(⌊‘𝑌))) → 𝑧 = 𝑌)
147146oveq1d 6541 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑌𝑛 ∈ (1...(⌊‘𝑌))) → (𝑧 / 𝑛) = (𝑌 / 𝑛))
148147fveq2d 6091 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑌𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑧 / 𝑛)) = (ψ‘(𝑌 / 𝑛)))
149148oveq2d 6542 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑌𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
150145, 149sumeq12rdv 14233 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑌 → Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
151143, 150syl5eq 2655 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑌 → Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))
152138, 151oveq12d 6544 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑌 → (((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) = (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))))
153 id 22 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑌𝑧 = 𝑌)
154152, 153oveq12d 6544 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑌 → ((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) = ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌))
155137oveq2d 6542 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑌 → (2 · (log‘𝑧)) = (2 · (log‘𝑌)))
156154, 155oveq12d 6544 . . . . . . . . . . . . . . 15 (𝑧 = 𝑌 → (((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧))) = (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))))
157156fveq2d 6091 . . . . . . . . . . . . . 14 (𝑧 = 𝑌 → (abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) = (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))))
158157breq1d 4587 . . . . . . . . . . . . 13 (𝑧 = 𝑌 → ((abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 ↔ (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵))
159158rspcv 3277 . . . . . . . . . . . 12 (𝑌 ∈ (1[,)+∞) → (∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 → (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵))
160134, 135, 159sylc 62 . . . . . . . . . . 11 (𝜑 → (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵)
161126, 128, 35, 129, 160letrd 10045 . . . . . . . . . 10 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤ 𝐵)
162122, 124, 35lesubaddd 10475 . . . . . . . . . 10 (𝜑 → ((((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤ 𝐵 ↔ ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘𝑌)))))
163161, 162mpbid 220 . . . . . . . . 9 (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘𝑌))))
16410simp3d 1067 . . . . . . . . . . . 12 (𝜑𝑌 ≤ (𝐴 · 𝑋))
16588, 79logled 24121 . . . . . . . . . . . 12 (𝜑 → (𝑌 ≤ (𝐴 · 𝑋) ↔ (log‘𝑌) ≤ (log‘(𝐴 · 𝑋))))
166164, 165mpbid 220 . . . . . . . . . . 11 (𝜑 → (log‘𝑌) ≤ (log‘(𝐴 · 𝑋)))
167 2pos 10961 . . . . . . . . . . . . . 14 0 < 2
16829, 167pm3.2i 469 . . . . . . . . . . . . 13 (2 ∈ ℝ ∧ 0 < 2)
169168a1i 11 . . . . . . . . . . . 12 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
170 lemul2 10727 . . . . . . . . . . . 12 (((log‘𝑌) ∈ ℝ ∧ (log‘(𝐴 · 𝑋)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((log‘𝑌) ≤ (log‘(𝐴 · 𝑋)) ↔ (2 · (log‘𝑌)) ≤ (2 · (log‘(𝐴 · 𝑋)))))
17189, 80, 169, 170syl3anc 1317 . . . . . . . . . . 11 (𝜑 → ((log‘𝑌) ≤ (log‘(𝐴 · 𝑋)) ↔ (2 · (log‘𝑌)) ≤ (2 · (log‘(𝐴 · 𝑋)))))
172166, 171mpbid 220 . . . . . . . . . 10 (𝜑 → (2 · (log‘𝑌)) ≤ (2 · (log‘(𝐴 · 𝑋))))
173124, 82, 35, 172leadd2dd 10493 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘𝑌))) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋)))))
174122, 125, 83, 163, 173letrd 10045 . . . . . . . 8 (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋)))))
17598, 83, 88ledivmul2d 11760 . . . . . . . 8 (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) ↔ (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌)))
176174, 175mpbid 220 . . . . . . 7 (𝜑 → (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌))
17774, 98, 84, 121, 176letrd 10045 . . . . . 6 (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌))
178 elicopnf 12098 . . . . . . . . . . . 12 (1 ∈ ℝ → (𝑋 ∈ (1[,)+∞) ↔ (𝑋 ∈ ℝ ∧ 1 ≤ 𝑋)))
17918, 178ax-mp 5 . . . . . . . . . . 11 (𝑋 ∈ (1[,)+∞) ↔ (𝑋 ∈ ℝ ∧ 1 ≤ 𝑋))
1804, 130, 179sylanbrc 694 . . . . . . . . . 10 (𝜑𝑋 ∈ (1[,)+∞))
181 fveq2 6087 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑋 → (ψ‘𝑧) = (ψ‘𝑋))
182 fveq2 6087 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑋 → (log‘𝑧) = (log‘𝑋))
183181, 182oveq12d 6544 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑋 → ((ψ‘𝑧) · (log‘𝑧)) = ((ψ‘𝑋) · (log‘𝑋)))
184 fveq2 6087 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑋 → (⌊‘𝑧) = (⌊‘𝑋))
185184oveq2d 6542 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑋 → (1...(⌊‘𝑧)) = (1...(⌊‘𝑋)))
186 simpl 471 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑋𝑛 ∈ (1...(⌊‘𝑋))) → 𝑧 = 𝑋)
187186oveq1d 6541 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑋𝑛 ∈ (1...(⌊‘𝑋))) → (𝑧 / 𝑛) = (𝑋 / 𝑛))
188187fveq2d 6091 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = 𝑋𝑛 ∈ (1...(⌊‘𝑋))) → (ψ‘(𝑧 / 𝑛)) = (ψ‘(𝑋 / 𝑛)))
189188oveq2d 6542 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑋𝑛 ∈ (1...(⌊‘𝑋))) → ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
190185, 189sumeq12rdv 14233 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑋 → Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
191143, 190syl5eq 2655 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑋 → Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))
192183, 191oveq12d 6544 . . . . . . . . . . . . . . 15 (𝑧 = 𝑋 → (((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) = (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))))
193 id 22 . . . . . . . . . . . . . . 15 (𝑧 = 𝑋𝑧 = 𝑋)
194192, 193oveq12d 6544 . . . . . . . . . . . . . 14 (𝑧 = 𝑋 → ((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) = ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋))
195182oveq2d 6542 . . . . . . . . . . . . . 14 (𝑧 = 𝑋 → (2 · (log‘𝑧)) = (2 · (log‘𝑋)))
196194, 195oveq12d 6544 . . . . . . . . . . . . 13 (𝑧 = 𝑋 → (((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧))) = (((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋))))
197196fveq2d 6091 . . . . . . . . . . . 12 (𝑧 = 𝑋 → (abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) = (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))))
198197breq1d 4587 . . . . . . . . . . 11 (𝑧 = 𝑋 → ((abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 ↔ (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵))
199198rspcv 3277 . . . . . . . . . 10 (𝑋 ∈ (1[,)+∞) → (∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 → (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵))
200180, 135, 199sylc 62 . . . . . . . . 9 (𝜑 → (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵)
20186, 26rerpdivcld 11737 . . . . . . . . . 10 (𝜑 → ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∈ ℝ)
202201, 76, 35absdifled 13969 . . . . . . . . 9 (𝜑 → ((abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵 ↔ (((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∧ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ≤ ((2 · (log‘𝑋)) + 𝐵))))
203200, 202mpbid 220 . . . . . . . 8 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∧ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ≤ ((2 · (log‘𝑋)) + 𝐵)))
204203simpld 473 . . . . . . 7 (𝜑 → ((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋))
20577, 86, 26lemuldivd 11755 . . . . . . 7 (𝜑 → ((((2 · (log‘𝑋)) − 𝐵) · 𝑋) ≤ (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ↔ ((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋)))
206204, 205mpbird 245 . . . . . 6 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) · 𝑋) ≤ (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))))
20774, 78, 84, 86, 177, 206le2subd 10498 . . . . 5 (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) ≤ (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋)))
20855recnd 9924 . . . . . . 7 (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ∈ ℂ)
20985recnd 9924 . . . . . . 7 (𝜑 → ((ψ‘𝑋) · (log‘𝑋)) ∈ ℂ)
21073recnd 9924 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℂ)
211208, 209, 210pnpcan2d 10281 . . . . . 6 (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) = (((ψ‘𝑌) · (log‘𝑋)) − ((ψ‘𝑋) · (log‘𝑋))))
21213recnd 9924 . . . . . . 7 (𝜑 → (ψ‘𝑌) ∈ ℂ)
21315recnd 9924 . . . . . . 7 (𝜑 → (ψ‘𝑋) ∈ ℂ)
21427recnd 9924 . . . . . . 7 (𝜑 → (log‘𝑋) ∈ ℂ)
215212, 213, 214subdird 10338 . . . . . 6 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) = (((ψ‘𝑌) · (log‘𝑋)) − ((ψ‘𝑋) · (log‘𝑋))))
216211, 215eqtr4d 2646 . . . . 5 (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) = (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)))
21776, 11remulcld 9926 . . . . . . . 8 (𝜑 → ((2 · (log‘𝑋)) · 𝑌) ∈ ℝ)
218217recnd 9924 . . . . . . 7 (𝜑 → ((2 · (log‘𝑋)) · 𝑌) ∈ ℂ)
21935, 40readdcld 9925 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘𝐴))) ∈ ℝ)
220219, 11remulcld 9926 . . . . . . . 8 (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) ∈ ℝ)
221220recnd 9924 . . . . . . 7 (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) ∈ ℂ)
22276, 4remulcld 9926 . . . . . . . 8 (𝜑 → ((2 · (log‘𝑋)) · 𝑋) ∈ ℝ)
223222recnd 9924 . . . . . . 7 (𝜑 → ((2 · (log‘𝑋)) · 𝑋) ∈ ℂ)
22435, 4remulcld 9926 . . . . . . . . 9 (𝜑 → (𝐵 · 𝑋) ∈ ℝ)
225224recnd 9924 . . . . . . . 8 (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
226225negcld 10230 . . . . . . 7 (𝜑 → -(𝐵 · 𝑋) ∈ ℂ)
227218, 221, 223, 226addsub4d 10290 . . . . . 6 (𝜑 → ((((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)) − (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋))) = ((((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)) + (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋))))
2285, 26relogmuld 24119 . . . . . . . . . . . . . 14 (𝜑 → (log‘(𝐴 · 𝑋)) = ((log‘𝐴) + (log‘𝑋)))
22938recnd 9924 . . . . . . . . . . . . . . 15 (𝜑 → (log‘𝐴) ∈ ℂ)
230229, 214addcomd 10089 . . . . . . . . . . . . . 14 (𝜑 → ((log‘𝐴) + (log‘𝑋)) = ((log‘𝑋) + (log‘𝐴)))
231228, 230eqtrd 2643 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝐴 · 𝑋)) = ((log‘𝑋) + (log‘𝐴)))
232231oveq2d 6542 . . . . . . . . . . . 12 (𝜑 → (2 · (log‘(𝐴 · 𝑋))) = (2 · ((log‘𝑋) + (log‘𝐴))))
233 2cnd 10942 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℂ)
234233, 214, 229adddid 9920 . . . . . . . . . . . 12 (𝜑 → (2 · ((log‘𝑋) + (log‘𝐴))) = ((2 · (log‘𝑋)) + (2 · (log‘𝐴))))
235232, 234eqtrd 2643 . . . . . . . . . . 11 (𝜑 → (2 · (log‘(𝐴 · 𝑋))) = ((2 · (log‘𝑋)) + (2 · (log‘𝐴))))
236235oveq2d 6542 . . . . . . . . . 10 (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) = (𝐵 + ((2 · (log‘𝑋)) + (2 · (log‘𝐴)))))
23735recnd 9924 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
23876recnd 9924 . . . . . . . . . . 11 (𝜑 → (2 · (log‘𝑋)) ∈ ℂ)
23940recnd 9924 . . . . . . . . . . 11 (𝜑 → (2 · (log‘𝐴)) ∈ ℂ)
240237, 238, 239add12d 10113 . . . . . . . . . 10 (𝜑 → (𝐵 + ((2 · (log‘𝑋)) + (2 · (log‘𝐴)))) = ((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))))
241236, 240eqtrd 2643 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) = ((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))))
242241oveq1d 6541 . . . . . . . 8 (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) = (((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))) · 𝑌))
243219recnd 9924 . . . . . . . . 9 (𝜑 → (𝐵 + (2 · (log‘𝐴))) ∈ ℂ)
24411recnd 9924 . . . . . . . . 9 (𝜑𝑌 ∈ ℂ)
245238, 243, 244adddird 9921 . . . . . . . 8 (𝜑 → (((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))) · 𝑌) = (((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)))
246242, 245eqtrd 2643 . . . . . . 7 (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) = (((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)))
2474recnd 9924 . . . . . . . . 9 (𝜑𝑋 ∈ ℂ)
248238, 237, 247subdird 10338 . . . . . . . 8 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) · 𝑋) = (((2 · (log‘𝑋)) · 𝑋) − (𝐵 · 𝑋)))
249223, 225negsubd 10249 . . . . . . . 8 (𝜑 → (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋)) = (((2 · (log‘𝑋)) · 𝑋) − (𝐵 · 𝑋)))
250248, 249eqtr4d 2646 . . . . . . 7 (𝜑 → (((2 · (log‘𝑋)) − 𝐵) · 𝑋) = (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋)))
251246, 250oveq12d 6544 . . . . . 6 (𝜑 → (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋)) = ((((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)) − (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋))))
25230recnd 9924 . . . . . . . . 9 (𝜑 → (𝑌𝑋) ∈ ℂ)
253233, 252, 214mul32d 10097 . . . . . . . 8 (𝜑 → ((2 · (𝑌𝑋)) · (log‘𝑋)) = ((2 · (log‘𝑋)) · (𝑌𝑋)))
254238, 244, 247subdid 10337 . . . . . . . 8 (𝜑 → ((2 · (log‘𝑋)) · (𝑌𝑋)) = (((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)))
255253, 254eqtrd 2643 . . . . . . 7 (𝜑 → ((2 · (𝑌𝑋)) · (log‘𝑋)) = (((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)))
25635, 11remulcld 9926 . . . . . . . . . . 11 (𝜑 → (𝐵 · 𝑌) ∈ ℝ)
257256recnd 9924 . . . . . . . . . 10 (𝜑 → (𝐵 · 𝑌) ∈ ℂ)
25841recnd 9924 . . . . . . . . . 10 (𝜑 → ((2 · (log‘𝐴)) · 𝑌) ∈ ℂ)
259257, 225, 258add32d 10114 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝑌) + (𝐵 · 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌)) + (𝐵 · 𝑋)))
260237, 244, 247adddid 9920 . . . . . . . . . 10 (𝜑 → (𝐵 · (𝑌 + 𝑋)) = ((𝐵 · 𝑌) + (𝐵 · 𝑋)))
261260oveq1d 6541 . . . . . . . . 9 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 · 𝑌) + (𝐵 · 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)))
262237, 239, 244adddird 9921 . . . . . . . . . 10 (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) = ((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌)))
263262oveq1d 6541 . . . . . . . . 9 (𝜑 → (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋)) = (((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌)) + (𝐵 · 𝑋)))
264259, 261, 2633eqtr4d 2653 . . . . . . . 8 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋)))
265221, 225subnegd 10250 . . . . . . . 8 (𝜑 → (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋)))
266264, 265eqtr4d 2646 . . . . . . 7 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋)))
267255, 266oveq12d 6544 . . . . . 6 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) = ((((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)) + (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋))))
268227, 251, 2673eqtr4d 2653 . . . . 5 (𝜑 → (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋)) = (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))))
269207, 216, 2683brtr3d 4608 . . . 4 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))))
27047, 4remulcld 9926 . . . . . . 7 (𝜑 → ((𝐵 · (𝐴 + 1)) · 𝑋) ∈ ℝ)
27150, 4remulcld 9926 . . . . . . 7 (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) ∈ ℝ)
27211, 7, 4, 164leadd1dd 10492 . . . . . . . . . 10 (𝜑 → (𝑌 + 𝑋) ≤ ((𝐴 · 𝑋) + 𝑋))
2736recnd 9924 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
27419recnd 9924 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
275273, 274, 247adddird 9921 . . . . . . . . . . 11 (𝜑 → ((𝐴 + 1) · 𝑋) = ((𝐴 · 𝑋) + (1 · 𝑋)))
276247mulid2d 9914 . . . . . . . . . . . 12 (𝜑 → (1 · 𝑋) = 𝑋)
277276oveq2d 6542 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝑋) + (1 · 𝑋)) = ((𝐴 · 𝑋) + 𝑋))
278275, 277eqtrd 2643 . . . . . . . . . 10 (𝜑 → ((𝐴 + 1) · 𝑋) = ((𝐴 · 𝑋) + 𝑋))
279272, 278breqtrrd 4605 . . . . . . . . 9 (𝜑 → (𝑌 + 𝑋) ≤ ((𝐴 + 1) · 𝑋))
28046, 4remulcld 9926 . . . . . . . . . 10 (𝜑 → ((𝐴 + 1) · 𝑋) ∈ ℝ)
28136, 280, 34lemul2d 11750 . . . . . . . . 9 (𝜑 → ((𝑌 + 𝑋) ≤ ((𝐴 + 1) · 𝑋) ↔ (𝐵 · (𝑌 + 𝑋)) ≤ (𝐵 · ((𝐴 + 1) · 𝑋))))
282279, 281mpbid 220 . . . . . . . 8 (𝜑 → (𝐵 · (𝑌 + 𝑋)) ≤ (𝐵 · ((𝐴 + 1) · 𝑋)))
28346recnd 9924 . . . . . . . . 9 (𝜑 → (𝐴 + 1) ∈ ℂ)
284237, 283, 247mulassd 9919 . . . . . . . 8 (𝜑 → ((𝐵 · (𝐴 + 1)) · 𝑋) = (𝐵 · ((𝐴 + 1) · 𝑋)))
285282, 284breqtrrd 4605 . . . . . . 7 (𝜑 → (𝐵 · (𝑌 + 𝑋)) ≤ ((𝐵 · (𝐴 + 1)) · 𝑋))
28629a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ)
287 0le2 10960 . . . . . . . . . . 11 0 ≤ 2
288287a1i 11 . . . . . . . . . 10 (𝜑 → 0 ≤ 2)
289 log1 24080 . . . . . . . . . . 11 (log‘1) = 0
290 chpdifbnd.1 . . . . . . . . . . . 12 (𝜑 → 1 ≤ 𝐴)
291 1rp 11670 . . . . . . . . . . . . 13 1 ∈ ℝ+
292 logleb 24097 . . . . . . . . . . . . 13 ((1 ∈ ℝ+𝐴 ∈ ℝ+) → (1 ≤ 𝐴 ↔ (log‘1) ≤ (log‘𝐴)))
293291, 5, 292sylancr 693 . . . . . . . . . . . 12 (𝜑 → (1 ≤ 𝐴 ↔ (log‘1) ≤ (log‘𝐴)))
294290, 293mpbid 220 . . . . . . . . . . 11 (𝜑 → (log‘1) ≤ (log‘𝐴))
295289, 294syl5eqbrr 4613 . . . . . . . . . 10 (𝜑 → 0 ≤ (log‘𝐴))
296286, 38, 288, 295mulge0d 10455 . . . . . . . . 9 (𝜑 → 0 ≤ (2 · (log‘𝐴)))
29711, 7, 40, 296, 164lemul2ad 10815 . . . . . . . 8 (𝜑 → ((2 · (log‘𝐴)) · 𝑌) ≤ ((2 · (log‘𝐴)) · (𝐴 · 𝑋)))
29849recnd 9924 . . . . . . . . . 10 (𝜑 → (2 · 𝐴) ∈ ℂ)
299298, 229, 247mulassd 9919 . . . . . . . . 9 (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) = ((2 · 𝐴) · ((log‘𝐴) · 𝑋)))
300233, 273, 229, 247mul4d 10099 . . . . . . . . 9 (𝜑 → ((2 · 𝐴) · ((log‘𝐴) · 𝑋)) = ((2 · (log‘𝐴)) · (𝐴 · 𝑋)))
301299, 300eqtrd 2643 . . . . . . . 8 (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) = ((2 · (log‘𝐴)) · (𝐴 · 𝑋)))
302297, 301breqtrrd 4605 . . . . . . 7 (𝜑 → ((2 · (log‘𝐴)) · 𝑌) ≤ (((2 · 𝐴) · (log‘𝐴)) · 𝑋))
30337, 41, 270, 271, 285, 302le2addd 10497 . . . . . 6 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ≤ (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋)))
30444oveq1i 6536 . . . . . . 7 (𝐶 · 𝑋) = (((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) · 𝑋)
30547recnd 9924 . . . . . . . 8 (𝜑 → (𝐵 · (𝐴 + 1)) ∈ ℂ)
30650recnd 9924 . . . . . . . 8 (𝜑 → ((2 · 𝐴) · (log‘𝐴)) ∈ ℂ)
307305, 306, 247adddird 9921 . . . . . . 7 (𝜑 → (((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) · 𝑋) = (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋)))
308304, 307syl5eq 2655 . . . . . 6 (𝜑 → (𝐶 · 𝑋) = (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋)))
309303, 308breqtrrd 4605 . . . . 5 (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ≤ (𝐶 · 𝑋))
31042, 53, 33, 309leadd2dd 10493 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) ≤ (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)))
31128, 43, 54, 269, 310letrd 10045 . . 3 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)))
31232recnd 9924 . . . . 5 (𝜑 → (2 · (𝑌𝑋)) ∈ ℂ)
3134, 24rplogcld 24123 . . . . . . . 8 (𝜑 → (log‘𝑋) ∈ ℝ+)
3144, 313rerpdivcld 11737 . . . . . . 7 (𝜑 → (𝑋 / (log‘𝑋)) ∈ ℝ)
31552, 314remulcld 9926 . . . . . 6 (𝜑 → (𝐶 · (𝑋 / (log‘𝑋))) ∈ ℝ)
316315recnd 9924 . . . . 5 (𝜑 → (𝐶 · (𝑋 / (log‘𝑋))) ∈ ℂ)
317312, 316, 214adddird 9921 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)) = (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋))))
31852recnd 9924 . . . . . . 7 (𝜑𝐶 ∈ ℂ)
319314recnd 9924 . . . . . . 7 (𝜑 → (𝑋 / (log‘𝑋)) ∈ ℂ)
320318, 319, 214mulassd 9919 . . . . . 6 (𝜑 → ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋)) = (𝐶 · ((𝑋 / (log‘𝑋)) · (log‘𝑋))))
321313rpne0d 11711 . . . . . . . 8 (𝜑 → (log‘𝑋) ≠ 0)
322247, 214, 321divcan1d 10653 . . . . . . 7 (𝜑 → ((𝑋 / (log‘𝑋)) · (log‘𝑋)) = 𝑋)
323322oveq2d 6542 . . . . . 6 (𝜑 → (𝐶 · ((𝑋 / (log‘𝑋)) · (log‘𝑋))) = (𝐶 · 𝑋))
324320, 323eqtrd 2643 . . . . 5 (𝜑 → ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋)) = (𝐶 · 𝑋))
325324oveq2d 6542 . . . 4 (𝜑 → (((2 · (𝑌𝑋)) · (log‘𝑋)) + ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋))) = (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)))
326317, 325eqtrd 2643 . . 3 (𝜑 → (((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)) = (((2 · (𝑌𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)))
327311, 326breqtrrd 4605 . 2 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)))
32832, 315readdcld 9925 . . 3 (𝜑 → ((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) ∈ ℝ)
32916, 328, 313lemul1d 11749 . 2 (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) ↔ (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋))))
330327, 329mpbird 245 1 (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  wss 3539   class class class wbr 4577  cfv 5789  (class class class)co 6526  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797  +∞cpnf 9927   < clt 9930  cle 9931  cmin 10117  -cneg 10118   / cdiv 10535  cn 10869  2c2 10919  cuz 11521  +crp 11666  (,)cioo 12004  [,)cico 12006  [,]cicc 12007  ...cfz 12154  cfl 12410  abscabs 13770  Σcsu 14212  logclog 24049  Λcvma 24562  ψcchp 24563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-se 4987  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-isom 5798  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-4 10930  df-5 10931  df-6 10932  df-7 10933  df-8 10934  df-9 10935  df-n0 11142  df-z 11213  df-dec 11328  df-uz 11522  df-q 11623  df-rp 11667  df-xneg 11780  df-xadd 11781  df-xmul 11782  df-ioo 12008  df-ioc 12009  df-ico 12010  df-icc 12011  df-fz 12155  df-fzo 12292  df-fl 12412  df-mod 12488  df-seq 12621  df-exp 12680  df-fac 12880  df-bc 12909  df-hash 12937  df-shft 13603  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772  df-limsup 13998  df-clim 14015  df-rlim 14016  df-sum 14213  df-ef 14585  df-sin 14587  df-cos 14588  df-pi 14590  df-dvds 14770  df-gcd 15003  df-prm 15172  df-pc 15328  df-struct 15645  df-ndx 15646  df-slot 15647  df-base 15648  df-sets 15649  df-ress 15650  df-plusg 15729  df-mulr 15730  df-starv 15731  df-sca 15732  df-vsca 15733  df-ip 15734  df-tset 15735  df-ple 15736  df-ds 15739  df-unif 15740  df-hom 15741  df-cco 15742  df-rest 15854  df-topn 15855  df-0g 15873  df-gsum 15874  df-topgen 15875  df-pt 15876  df-prds 15879  df-xrs 15933  df-qtop 15938  df-imas 15939  df-xps 15941  df-mre 16017  df-mrc 16018  df-acs 16020  df-mgm 17013  df-sgrp 17055  df-mnd 17066  df-submnd 17107  df-mulg 17312  df-cntz 17521  df-cmn 17966  df-psmet 19507  df-xmet 19508  df-met 19509  df-bl 19510  df-mopn 19511  df-fbas 19512  df-fg 19513  df-cnfld 19516  df-top 20468  df-bases 20469  df-topon 20470  df-topsp 20471  df-cld 20580  df-ntr 20581  df-cls 20582  df-nei 20659  df-lp 20697  df-perf 20698  df-cn 20788  df-cnp 20789  df-haus 20876  df-tx 21122  df-hmeo 21315  df-fil 21407  df-fm 21499  df-flim 21500  df-flf 21501  df-xms 21882  df-ms 21883  df-tms 21884  df-cncf 22436  df-limc 23380  df-dv 23381  df-log 24051  df-vma 24568  df-chp 24569
This theorem is referenced by:  chpdifbndlem2  24987
  Copyright terms: Public domain W3C validator