Step | Hyp | Ref
| Expression |
1 | | chpdifbnd.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ (𝑋[,](𝐴 · 𝑋))) |
2 | | ioossre 12235 |
. . . . . . . . . . 11
⊢
(1(,)+∞) ⊆ ℝ |
3 | | chpdifbnd.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (1(,)+∞)) |
4 | 2, 3 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
5 | | chpdifbnd.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
6 | 5 | rpred 11872 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
7 | 6, 4 | remulcld 10070 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 · 𝑋) ∈ ℝ) |
8 | | elicc2 12238 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℝ ∧ (𝐴 · 𝑋) ∈ ℝ) → (𝑌 ∈ (𝑋[,](𝐴 · 𝑋)) ↔ (𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ (𝐴 · 𝑋)))) |
9 | 4, 7, 8 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 ∈ (𝑋[,](𝐴 · 𝑋)) ↔ (𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ (𝐴 · 𝑋)))) |
10 | 1, 9 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ (𝐴 · 𝑋))) |
11 | 10 | simp1d 1073 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) |
12 | | chpcl 24850 |
. . . . . . 7
⊢ (𝑌 ∈ ℝ →
(ψ‘𝑌) ∈
ℝ) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ψ‘𝑌) ∈
ℝ) |
14 | | chpcl 24850 |
. . . . . . 7
⊢ (𝑋 ∈ ℝ →
(ψ‘𝑋) ∈
ℝ) |
15 | 4, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ψ‘𝑋) ∈
ℝ) |
16 | 13, 15 | resubcld 10458 |
. . . . 5
⊢ (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ∈
ℝ) |
17 | | 0red 10041 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
18 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
20 | | 0lt1 10550 |
. . . . . . . . 9
⊢ 0 <
1 |
21 | 20 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 < 1) |
22 | | eliooord 12233 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (1(,)+∞) → (1
< 𝑋 ∧ 𝑋 <
+∞)) |
23 | 3, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1 < 𝑋 ∧ 𝑋 < +∞)) |
24 | 23 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → 1 < 𝑋) |
25 | 17, 19, 4, 21, 24 | lttrd 10198 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑋) |
26 | 4, 25 | elrpd 11869 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
27 | 26 | relogcld 24369 |
. . . . 5
⊢ (𝜑 → (log‘𝑋) ∈
ℝ) |
28 | 16, 27 | remulcld 10070 |
. . . 4
⊢ (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ∈
ℝ) |
29 | | 2re 11090 |
. . . . . . 7
⊢ 2 ∈
ℝ |
30 | 11, 4 | resubcld 10458 |
. . . . . . 7
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℝ) |
31 | | remulcl 10021 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ (𝑌
− 𝑋) ∈ ℝ)
→ (2 · (𝑌
− 𝑋)) ∈
ℝ) |
32 | 29, 30, 31 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → (2 · (𝑌 − 𝑋)) ∈ ℝ) |
33 | 32, 27 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((2 · (𝑌 − 𝑋)) · (log‘𝑋)) ∈ ℝ) |
34 | | chpdifbnd.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
35 | 34 | rpred 11872 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
36 | 11, 4 | readdcld 10069 |
. . . . . . 7
⊢ (𝜑 → (𝑌 + 𝑋) ∈ ℝ) |
37 | 35, 36 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → (𝐵 · (𝑌 + 𝑋)) ∈ ℝ) |
38 | 5 | relogcld 24369 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝐴) ∈
ℝ) |
39 | | remulcl 10021 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ (log‘𝐴) ∈ ℝ) → (2 ·
(log‘𝐴)) ∈
ℝ) |
40 | 29, 38, 39 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → (2 ·
(log‘𝐴)) ∈
ℝ) |
41 | 40, 11 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → ((2 ·
(log‘𝐴)) ·
𝑌) ∈
ℝ) |
42 | 37, 41 | readdcld 10069 |
. . . . 5
⊢ (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ∈ ℝ) |
43 | 33, 42 | readdcld 10069 |
. . . 4
⊢ (𝜑 → (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) ∈ ℝ) |
44 | | chpdifbnd.c |
. . . . . . 7
⊢ 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) |
45 | | peano2re 10209 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
46 | 6, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 1) ∈ ℝ) |
47 | 35, 46 | remulcld 10070 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (𝐴 + 1)) ∈ ℝ) |
48 | | remulcl 10021 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ 𝐴
∈ ℝ) → (2 · 𝐴) ∈ ℝ) |
49 | 29, 6, 48 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 𝐴) ∈
ℝ) |
50 | 49, 38 | remulcld 10070 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝐴) · (log‘𝐴)) ∈
ℝ) |
51 | 47, 50 | readdcld 10069 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) ∈ ℝ) |
52 | 44, 51 | syl5eqel 2705 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
53 | 52, 4 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → (𝐶 · 𝑋) ∈ ℝ) |
54 | 33, 53 | readdcld 10069 |
. . . 4
⊢ (𝜑 → (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋)) ∈ ℝ) |
55 | 13, 27 | remulcld 10070 |
. . . . . . 7
⊢ (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ∈
ℝ) |
56 | | fzfid 12772 |
. . . . . . . 8
⊢ (𝜑 → (1...(⌊‘𝑋)) ∈ Fin) |
57 | 10 | simp2d 1074 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
58 | | flword2 12614 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌) → (⌊‘𝑌) ∈
(ℤ≥‘(⌊‘𝑋))) |
59 | 4, 11, 57, 58 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘𝑌) ∈
(ℤ≥‘(⌊‘𝑋))) |
60 | | fzss2 12381 |
. . . . . . . . . . 11
⊢
((⌊‘𝑌)
∈ (ℤ≥‘(⌊‘𝑋)) → (1...(⌊‘𝑋)) ⊆
(1...(⌊‘𝑌))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1...(⌊‘𝑋)) ⊆
(1...(⌊‘𝑌))) |
62 | 61 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑋))) → 𝑛 ∈ (1...(⌊‘𝑌))) |
63 | | elfznn 12370 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑌))
→ 𝑛 ∈
ℕ) |
64 | 63 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 𝑛 ∈ ℕ) |
65 | | vmacl 24844 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (Λ‘𝑛) ∈
ℝ) |
67 | | nndivre 11056 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑋 / 𝑛) ∈ ℝ) |
68 | 4, 63, 67 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (𝑋 / 𝑛) ∈ ℝ) |
69 | | chpcl 24850 |
. . . . . . . . . . 11
⊢ ((𝑋 / 𝑛) ∈ ℝ → (ψ‘(𝑋 / 𝑛)) ∈ ℝ) |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑋 / 𝑛)) ∈ ℝ) |
71 | 66, 70 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ) |
72 | 62, 71 | syldan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑋))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ) |
73 | 56, 72 | fsumrecl 14465 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ) |
74 | 55, 73 | readdcld 10069 |
. . . . . 6
⊢ (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ∈ ℝ) |
75 | | remulcl 10021 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ (log‘𝑋) ∈ ℝ) → (2 ·
(log‘𝑋)) ∈
ℝ) |
76 | 29, 27, 75 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → (2 ·
(log‘𝑋)) ∈
ℝ) |
77 | 76, 35 | resubcld 10458 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(log‘𝑋)) −
𝐵) ∈
ℝ) |
78 | 77, 4 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → (((2 ·
(log‘𝑋)) −
𝐵) · 𝑋) ∈
ℝ) |
79 | 5, 26 | rpmulcld 11888 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 · 𝑋) ∈
ℝ+) |
80 | 79 | relogcld 24369 |
. . . . . . . . 9
⊢ (𝜑 → (log‘(𝐴 · 𝑋)) ∈ ℝ) |
81 | | remulcl 10021 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ (log‘(𝐴 · 𝑋)) ∈ ℝ) → (2 ·
(log‘(𝐴 ·
𝑋))) ∈
ℝ) |
82 | 29, 80, 81 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → (2 ·
(log‘(𝐴 ·
𝑋))) ∈
ℝ) |
83 | 35, 82 | readdcld 10069 |
. . . . . . 7
⊢ (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) ∈ ℝ) |
84 | 83, 11 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) ∈ ℝ) |
85 | 15, 27 | remulcld 10070 |
. . . . . . 7
⊢ (𝜑 → ((ψ‘𝑋) · (log‘𝑋)) ∈
ℝ) |
86 | 85, 73 | readdcld 10069 |
. . . . . 6
⊢ (𝜑 → (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ∈ ℝ) |
87 | 17, 4, 11, 25, 57 | ltletrd 10197 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝑌) |
88 | 11, 87 | elrpd 11869 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈
ℝ+) |
89 | 88 | relogcld 24369 |
. . . . . . . . 9
⊢ (𝜑 → (log‘𝑌) ∈
ℝ) |
90 | 13, 89 | remulcld 10070 |
. . . . . . . 8
⊢ (𝜑 → ((ψ‘𝑌) · (log‘𝑌)) ∈
ℝ) |
91 | | fzfid 12772 |
. . . . . . . . 9
⊢ (𝜑 → (1...(⌊‘𝑌)) ∈ Fin) |
92 | | nndivre 11056 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑌 / 𝑛) ∈ ℝ) |
93 | 11, 63, 92 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (𝑌 / 𝑛) ∈ ℝ) |
94 | | chpcl 24850 |
. . . . . . . . . . 11
⊢ ((𝑌 / 𝑛) ∈ ℝ → (ψ‘(𝑌 / 𝑛)) ∈ ℝ) |
95 | 93, 94 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑌 / 𝑛)) ∈ ℝ) |
96 | 66, 95 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))) ∈ ℝ) |
97 | 91, 96 | fsumrecl 14465 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))) ∈ ℝ) |
98 | 90, 97 | readdcld 10069 |
. . . . . . 7
⊢ (𝜑 → (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ∈ ℝ) |
99 | | chpge0 24852 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℝ → 0 ≤
(ψ‘𝑌)) |
100 | 11, 99 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (ψ‘𝑌)) |
101 | 26, 88 | logled 24373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (log‘𝑋) ≤ (log‘𝑌))) |
102 | 57, 101 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → (log‘𝑋) ≤ (log‘𝑌)) |
103 | 27, 89, 13, 100, 102 | lemul2ad 10964 |
. . . . . . . 8
⊢ (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ≤ ((ψ‘𝑌) · (log‘𝑌))) |
104 | 91, 71 | fsumrecl 14465 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℝ) |
105 | | vmage0 24847 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
106 | 64, 105 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ (Λ‘𝑛)) |
107 | | chpge0 24852 |
. . . . . . . . . . . 12
⊢ ((𝑋 / 𝑛) ∈ ℝ → 0 ≤
(ψ‘(𝑋 / 𝑛))) |
108 | 68, 107 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ (ψ‘(𝑋 / 𝑛))) |
109 | 66, 70, 106, 108 | mulge0d 10604 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 0 ≤ ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) |
110 | 91, 71, 109, 61 | fsumless 14528 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) |
111 | 4 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 𝑋 ∈ ℝ) |
112 | 11 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 𝑌 ∈ ℝ) |
113 | 64 | nnrpd 11870 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 𝑛 ∈ ℝ+) |
114 | 57 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 𝑋 ≤ 𝑌) |
115 | 111, 112,
113, 114 | lediv1dd 11930 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (𝑋 / 𝑛) ≤ (𝑌 / 𝑛)) |
116 | | chpwordi 24883 |
. . . . . . . . . . . 12
⊢ (((𝑋 / 𝑛) ∈ ℝ ∧ (𝑌 / 𝑛) ∈ ℝ ∧ (𝑋 / 𝑛) ≤ (𝑌 / 𝑛)) → (ψ‘(𝑋 / 𝑛)) ≤ (ψ‘(𝑌 / 𝑛))) |
117 | 68, 93, 115, 116 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑋 / 𝑛)) ≤ (ψ‘(𝑌 / 𝑛))) |
118 | 70, 95, 66, 106, 117 | lemul2ad 10964 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) |
119 | 91, 71, 96, 118 | fsumle 14531 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) |
120 | 73, 104, 97, 110, 119 | letrd 10194 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) |
121 | 55, 73, 90, 97, 103, 120 | le2addd 10646 |
. . . . . . 7
⊢ (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ≤ (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))) |
122 | 98, 88 | rerpdivcld 11903 |
. . . . . . . . 9
⊢ (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ∈ ℝ) |
123 | | remulcl 10021 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (2 ·
(log‘𝑌)) ∈
ℝ) |
124 | 29, 89, 123 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (2 ·
(log‘𝑌)) ∈
ℝ) |
125 | 35, 124 | readdcld 10069 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 + (2 · (log‘𝑌))) ∈ ℝ) |
126 | 122, 124 | resubcld 10458 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ∈
ℝ) |
127 | 126 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ∈
ℂ) |
128 | 127 | abscld 14175 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ∈
ℝ) |
129 | 126 | leabsd 14153 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤
(abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))))) |
130 | 19, 4, 24 | ltled 10185 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≤ 𝑋) |
131 | 19, 4, 11, 130, 57 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ≤ 𝑌) |
132 | | elicopnf 12269 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℝ → (𝑌 ∈
(1[,)+∞) ↔ (𝑌
∈ ℝ ∧ 1 ≤ 𝑌))) |
133 | 18, 132 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ (1[,)+∞) ↔
(𝑌 ∈ ℝ ∧ 1
≤ 𝑌)) |
134 | 11, 131, 133 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ (1[,)+∞)) |
135 | | chpdifbnd.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑧 ∈
(1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵) |
136 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑌 → (ψ‘𝑧) = (ψ‘𝑌)) |
137 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑌 → (log‘𝑧) = (log‘𝑌)) |
138 | 136, 137 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑌 → ((ψ‘𝑧) · (log‘𝑧)) = ((ψ‘𝑌) · (log‘𝑌))) |
139 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (Λ‘𝑚) = (Λ‘𝑛)) |
140 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (𝑧 / 𝑚) = (𝑧 / 𝑛)) |
141 | 140 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (ψ‘(𝑧 / 𝑚)) = (ψ‘(𝑧 / 𝑛))) |
142 | 139, 141 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → ((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛)))) |
143 | 142 | cbvsumv 14426 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ𝑚 ∈
(1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) |
144 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑌 → (⌊‘𝑧) = (⌊‘𝑌)) |
145 | 144 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑌 → (1...(⌊‘𝑧)) = (1...(⌊‘𝑌))) |
146 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 = 𝑌 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → 𝑧 = 𝑌) |
147 | 146 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 = 𝑌 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (𝑧 / 𝑛) = (𝑌 / 𝑛)) |
148 | 147 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 = 𝑌 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → (ψ‘(𝑧 / 𝑛)) = (ψ‘(𝑌 / 𝑛))) |
149 | 148 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 = 𝑌 ∧ 𝑛 ∈ (1...(⌊‘𝑌))) → ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = ((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) |
150 | 145, 149 | sumeq12rdv 14438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑌 → Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) |
151 | 143, 150 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑌 → Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) |
152 | 138, 151 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑌 → (((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) = (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛))))) |
153 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑌 → 𝑧 = 𝑌) |
154 | 152, 153 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑌 → ((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) = ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌)) |
155 | 137 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑌 → (2 · (log‘𝑧)) = (2 ·
(log‘𝑌))) |
156 | 154, 155 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑌 → (((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧))) = (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) |
157 | 156 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑌 → (abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) =
(abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))))) |
158 | 157 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑌 → ((abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 ↔ (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵)) |
159 | 158 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ (1[,)+∞) →
(∀𝑧 ∈
(1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 → (abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵)) |
160 | 134, 135,
159 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌)))) ≤ 𝐵) |
161 | 126, 128,
35, 129, 160 | letrd 10194 |
. . . . . . . . . 10
⊢ (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤ 𝐵) |
162 | 122, 124,
35 | lesubaddd 10624 |
. . . . . . . . . 10
⊢ (𝜑 → ((((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) − (2 · (log‘𝑌))) ≤ 𝐵 ↔ ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘𝑌))))) |
163 | 161, 162 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘𝑌)))) |
164 | 10 | simp3d 1075 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ≤ (𝐴 · 𝑋)) |
165 | 88, 79 | logled 24373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ≤ (𝐴 · 𝑋) ↔ (log‘𝑌) ≤ (log‘(𝐴 · 𝑋)))) |
166 | 164, 165 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘𝑌) ≤ (log‘(𝐴 · 𝑋))) |
167 | | 2pos 11112 |
. . . . . . . . . . . . . 14
⊢ 0 <
2 |
168 | 29, 167 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℝ ∧ 0 < 2) |
169 | 168 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
170 | | lemul2 10876 |
. . . . . . . . . . . 12
⊢
(((log‘𝑌)
∈ ℝ ∧ (log‘(𝐴 · 𝑋)) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((log‘𝑌) ≤ (log‘(𝐴 · 𝑋)) ↔ (2 · (log‘𝑌)) ≤ (2 ·
(log‘(𝐴 ·
𝑋))))) |
171 | 89, 80, 169, 170 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝑌) ≤ (log‘(𝐴 · 𝑋)) ↔ (2 · (log‘𝑌)) ≤ (2 ·
(log‘(𝐴 ·
𝑋))))) |
172 | 166, 171 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (2 ·
(log‘𝑌)) ≤ (2
· (log‘(𝐴
· 𝑋)))) |
173 | 124, 82, 35, 172 | leadd2dd 10642 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 + (2 · (log‘𝑌))) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋))))) |
174 | 122, 125,
83, 163, 173 | letrd 10194 |
. . . . . . . 8
⊢ (𝜑 → ((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋))))) |
175 | 98, 83, 88 | ledivmul2d 11926 |
. . . . . . . 8
⊢ (𝜑 → (((((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) / 𝑌) ≤ (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) ↔ (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌))) |
176 | 174, 175 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (((ψ‘𝑌) · (log‘𝑌)) + Σ𝑛 ∈ (1...(⌊‘𝑌))((Λ‘𝑛) · (ψ‘(𝑌 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌)) |
177 | 74, 98, 84, 121, 176 | letrd 10194 |
. . . . . 6
⊢ (𝜑 → (((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ≤ ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌)) |
178 | | elicopnf 12269 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ → (𝑋 ∈
(1[,)+∞) ↔ (𝑋
∈ ℝ ∧ 1 ≤ 𝑋))) |
179 | 18, 178 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (1[,)+∞) ↔
(𝑋 ∈ ℝ ∧ 1
≤ 𝑋)) |
180 | 4, 130, 179 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (1[,)+∞)) |
181 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑋 → (ψ‘𝑧) = (ψ‘𝑋)) |
182 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑋 → (log‘𝑧) = (log‘𝑋)) |
183 | 181, 182 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑋 → ((ψ‘𝑧) · (log‘𝑧)) = ((ψ‘𝑋) · (log‘𝑋))) |
184 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑋 → (⌊‘𝑧) = (⌊‘𝑋)) |
185 | 184 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑋 → (1...(⌊‘𝑧)) = (1...(⌊‘𝑋))) |
186 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 = 𝑋 ∧ 𝑛 ∈ (1...(⌊‘𝑋))) → 𝑧 = 𝑋) |
187 | 186 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 = 𝑋 ∧ 𝑛 ∈ (1...(⌊‘𝑋))) → (𝑧 / 𝑛) = (𝑋 / 𝑛)) |
188 | 187 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 = 𝑋 ∧ 𝑛 ∈ (1...(⌊‘𝑋))) → (ψ‘(𝑧 / 𝑛)) = (ψ‘(𝑋 / 𝑛))) |
189 | 188 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 = 𝑋 ∧ 𝑛 ∈ (1...(⌊‘𝑋))) → ((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = ((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) |
190 | 185, 189 | sumeq12rdv 14438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑋 → Σ𝑛 ∈ (1...(⌊‘𝑧))((Λ‘𝑛) · (ψ‘(𝑧 / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) |
191 | 143, 190 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑋 → Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) |
192 | 183, 191 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑋 → (((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) = (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) |
193 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑋 → 𝑧 = 𝑋) |
194 | 192, 193 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑋 → ((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) = ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋)) |
195 | 182 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑋 → (2 · (log‘𝑧)) = (2 ·
(log‘𝑋))) |
196 | 194, 195 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑋 → (((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧))) = (((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) |
197 | 196 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑋 → (abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) =
(abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋))))) |
198 | 197 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑋 → ((abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 ↔ (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵)) |
199 | 198 | rspcv 3305 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (1[,)+∞) →
(∀𝑧 ∈
(1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵 → (abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵)) |
200 | 180, 135,
199 | sylc 65 |
. . . . . . . . 9
⊢ (𝜑 →
(abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵) |
201 | 86, 26 | rerpdivcld 11903 |
. . . . . . . . . 10
⊢ (𝜑 → ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∈ ℝ) |
202 | 201, 76, 35 | absdifled 14173 |
. . . . . . . . 9
⊢ (𝜑 →
((abs‘(((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) − (2 · (log‘𝑋)))) ≤ 𝐵 ↔ (((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∧ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ≤ ((2 · (log‘𝑋)) + 𝐵)))) |
203 | 200, 202 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → (((2 ·
(log‘𝑋)) −
𝐵) ≤
((((ψ‘𝑋) ·
(log‘𝑋)) +
Σ𝑛 ∈
(1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ∧ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋) ≤ ((2 · (log‘𝑋)) + 𝐵))) |
204 | 203 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(log‘𝑋)) −
𝐵) ≤
((((ψ‘𝑋) ·
(log‘𝑋)) +
Σ𝑛 ∈
(1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋)) |
205 | 77, 86, 26 | lemuldivd 11921 |
. . . . . . 7
⊢ (𝜑 → ((((2 ·
(log‘𝑋)) −
𝐵) · 𝑋) ≤ (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) ↔ ((2 · (log‘𝑋)) − 𝐵) ≤ ((((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) / 𝑋))) |
206 | 204, 205 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → (((2 ·
(log‘𝑋)) −
𝐵) · 𝑋) ≤ (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) |
207 | 74, 78, 84, 86, 177, 206 | le2subd 10647 |
. . . . 5
⊢ (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) ≤ (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋))) |
208 | 55 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → ((ψ‘𝑌) · (log‘𝑋)) ∈
ℂ) |
209 | 85 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → ((ψ‘𝑋) · (log‘𝑋)) ∈
ℂ) |
210 | 73 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))) ∈ ℂ) |
211 | 208, 209,
210 | pnpcan2d 10430 |
. . . . . 6
⊢ (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) = (((ψ‘𝑌) · (log‘𝑋)) − ((ψ‘𝑋) · (log‘𝑋)))) |
212 | 13 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (ψ‘𝑌) ∈
ℂ) |
213 | 15 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (ψ‘𝑋) ∈
ℂ) |
214 | 27 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (log‘𝑋) ∈
ℂ) |
215 | 212, 213,
214 | subdird 10487 |
. . . . . 6
⊢ (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) = (((ψ‘𝑌) · (log‘𝑋)) − ((ψ‘𝑋) · (log‘𝑋)))) |
216 | 211, 215 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → ((((ψ‘𝑌) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛)))) − (((ψ‘𝑋) · (log‘𝑋)) + Σ𝑛 ∈ (1...(⌊‘𝑋))((Λ‘𝑛) · (ψ‘(𝑋 / 𝑛))))) = (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋))) |
217 | 76, 11 | remulcld 10070 |
. . . . . . . 8
⊢ (𝜑 → ((2 ·
(log‘𝑋)) ·
𝑌) ∈
ℝ) |
218 | 217 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(log‘𝑋)) ·
𝑌) ∈
ℂ) |
219 | 35, 40 | readdcld 10069 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 + (2 · (log‘𝐴))) ∈ ℝ) |
220 | 219, 11 | remulcld 10070 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) ∈ ℝ) |
221 | 220 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) ∈ ℂ) |
222 | 76, 4 | remulcld 10070 |
. . . . . . . 8
⊢ (𝜑 → ((2 ·
(log‘𝑋)) ·
𝑋) ∈
ℝ) |
223 | 222 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(log‘𝑋)) ·
𝑋) ∈
ℂ) |
224 | 35, 4 | remulcld 10070 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℝ) |
225 | 224 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ) |
226 | 225 | negcld 10379 |
. . . . . . 7
⊢ (𝜑 → -(𝐵 · 𝑋) ∈ ℂ) |
227 | 218, 221,
223, 226 | addsub4d 10439 |
. . . . . 6
⊢ (𝜑 → ((((2 ·
(log‘𝑋)) ·
𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)) − (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋))) = ((((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)) + (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋)))) |
228 | 5, 26 | relogmuld 24371 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (log‘(𝐴 · 𝑋)) = ((log‘𝐴) + (log‘𝑋))) |
229 | 38 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) |
230 | 229, 214 | addcomd 10238 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((log‘𝐴) + (log‘𝑋)) = ((log‘𝑋) + (log‘𝐴))) |
231 | 228, 230 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (log‘(𝐴 · 𝑋)) = ((log‘𝑋) + (log‘𝐴))) |
232 | 231 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ·
(log‘(𝐴 ·
𝑋))) = (2 ·
((log‘𝑋) +
(log‘𝐴)))) |
233 | | 2cnd 11093 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℂ) |
234 | 233, 214,
229 | adddid 10064 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ·
((log‘𝑋) +
(log‘𝐴))) = ((2
· (log‘𝑋)) +
(2 · (log‘𝐴)))) |
235 | 232, 234 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ·
(log‘(𝐴 ·
𝑋))) = ((2 ·
(log‘𝑋)) + (2
· (log‘𝐴)))) |
236 | 235 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) = (𝐵 + ((2 · (log‘𝑋)) + (2 · (log‘𝐴))))) |
237 | 35 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
238 | 76 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ·
(log‘𝑋)) ∈
ℂ) |
239 | 40 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ·
(log‘𝐴)) ∈
ℂ) |
240 | 237, 238,
239 | add12d 10262 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 + ((2 · (log‘𝑋)) + (2 · (log‘𝐴)))) = ((2 ·
(log‘𝑋)) + (𝐵 + (2 · (log‘𝐴))))) |
241 | 236, 240 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 + (2 · (log‘(𝐴 · 𝑋)))) = ((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴))))) |
242 | 241 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) = (((2 · (log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))) · 𝑌)) |
243 | 219 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 + (2 · (log‘𝐴))) ∈ ℂ) |
244 | 11 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ ℂ) |
245 | 238, 243,
244 | adddird 10065 |
. . . . . . . 8
⊢ (𝜑 → (((2 ·
(log‘𝑋)) + (𝐵 + (2 · (log‘𝐴)))) · 𝑌) = (((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌))) |
246 | 242, 245 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) = (((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌))) |
247 | 4 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℂ) |
248 | 238, 237,
247 | subdird 10487 |
. . . . . . . 8
⊢ (𝜑 → (((2 ·
(log‘𝑋)) −
𝐵) · 𝑋) = (((2 ·
(log‘𝑋)) ·
𝑋) − (𝐵 · 𝑋))) |
249 | 223, 225 | negsubd 10398 |
. . . . . . . 8
⊢ (𝜑 → (((2 ·
(log‘𝑋)) ·
𝑋) + -(𝐵 · 𝑋)) = (((2 · (log‘𝑋)) · 𝑋) − (𝐵 · 𝑋))) |
250 | 248, 249 | eqtr4d 2659 |
. . . . . . 7
⊢ (𝜑 → (((2 ·
(log‘𝑋)) −
𝐵) · 𝑋) = (((2 ·
(log‘𝑋)) ·
𝑋) + -(𝐵 · 𝑋))) |
251 | 246, 250 | oveq12d 6668 |
. . . . . 6
⊢ (𝜑 → (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋)) = ((((2 · (log‘𝑋)) · 𝑌) + ((𝐵 + (2 · (log‘𝐴))) · 𝑌)) − (((2 · (log‘𝑋)) · 𝑋) + -(𝐵 · 𝑋)))) |
252 | 30 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℂ) |
253 | 233, 252,
214 | mul32d 10246 |
. . . . . . . 8
⊢ (𝜑 → ((2 · (𝑌 − 𝑋)) · (log‘𝑋)) = ((2 · (log‘𝑋)) · (𝑌 − 𝑋))) |
254 | 238, 244,
247 | subdid 10486 |
. . . . . . . 8
⊢ (𝜑 → ((2 ·
(log‘𝑋)) ·
(𝑌 − 𝑋)) = (((2 ·
(log‘𝑋)) ·
𝑌) − ((2 ·
(log‘𝑋)) ·
𝑋))) |
255 | 253, 254 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((2 · (𝑌 − 𝑋)) · (log‘𝑋)) = (((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋))) |
256 | 35, 11 | remulcld 10070 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 · 𝑌) ∈ ℝ) |
257 | 256 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 · 𝑌) ∈ ℂ) |
258 | 41 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 ·
(log‘𝐴)) ·
𝑌) ∈
ℂ) |
259 | 257, 225,
258 | add32d 10263 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐵 · 𝑌) + (𝐵 · 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌)) + (𝐵 · 𝑋))) |
260 | 237, 244,
247 | adddid 10064 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 · (𝑌 + 𝑋)) = ((𝐵 · 𝑌) + (𝐵 · 𝑋))) |
261 | 260 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 · 𝑌) + (𝐵 · 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) |
262 | 237, 239,
244 | adddird 10065 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 + (2 · (log‘𝐴))) · 𝑌) = ((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌))) |
263 | 262 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋)) = (((𝐵 · 𝑌) + ((2 · (log‘𝐴)) · 𝑌)) + (𝐵 · 𝑋))) |
264 | 259, 261,
263 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋))) |
265 | 221, 225 | subnegd 10399 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) + (𝐵 · 𝑋))) |
266 | 264, 265 | eqtr4d 2659 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) = (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋))) |
267 | 255, 266 | oveq12d 6668 |
. . . . . 6
⊢ (𝜑 → (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) = ((((2 · (log‘𝑋)) · 𝑌) − ((2 · (log‘𝑋)) · 𝑋)) + (((𝐵 + (2 · (log‘𝐴))) · 𝑌) − -(𝐵 · 𝑋)))) |
268 | 227, 251,
267 | 3eqtr4d 2666 |
. . . . 5
⊢ (𝜑 → (((𝐵 + (2 · (log‘(𝐴 · 𝑋)))) · 𝑌) − (((2 · (log‘𝑋)) − 𝐵) · 𝑋)) = (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)))) |
269 | 207, 216,
268 | 3brtr3d 4684 |
. . . 4
⊢ (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)))) |
270 | 47, 4 | remulcld 10070 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 · (𝐴 + 1)) · 𝑋) ∈ ℝ) |
271 | 50, 4 | remulcld 10070 |
. . . . . . 7
⊢ (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) ∈ ℝ) |
272 | 11, 7, 4, 164 | leadd1dd 10641 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 + 𝑋) ≤ ((𝐴 · 𝑋) + 𝑋)) |
273 | 6 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
274 | 19 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
275 | 273, 274,
247 | adddird 10065 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 + 1) · 𝑋) = ((𝐴 · 𝑋) + (1 · 𝑋))) |
276 | 247 | mulid2d 10058 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 · 𝑋) = 𝑋) |
277 | 276 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝑋) + (1 · 𝑋)) = ((𝐴 · 𝑋) + 𝑋)) |
278 | 275, 277 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 1) · 𝑋) = ((𝐴 · 𝑋) + 𝑋)) |
279 | 272, 278 | breqtrrd 4681 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 + 𝑋) ≤ ((𝐴 + 1) · 𝑋)) |
280 | 46, 4 | remulcld 10070 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 1) · 𝑋) ∈ ℝ) |
281 | 36, 280, 34 | lemul2d 11916 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 + 𝑋) ≤ ((𝐴 + 1) · 𝑋) ↔ (𝐵 · (𝑌 + 𝑋)) ≤ (𝐵 · ((𝐴 + 1) · 𝑋)))) |
282 | 279, 281 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (𝑌 + 𝑋)) ≤ (𝐵 · ((𝐴 + 1) · 𝑋))) |
283 | 46 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 1) ∈ ℂ) |
284 | 237, 283,
247 | mulassd 10063 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 · (𝐴 + 1)) · 𝑋) = (𝐵 · ((𝐴 + 1) · 𝑋))) |
285 | 282, 284 | breqtrrd 4681 |
. . . . . . 7
⊢ (𝜑 → (𝐵 · (𝑌 + 𝑋)) ≤ ((𝐵 · (𝐴 + 1)) · 𝑋)) |
286 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℝ) |
287 | | 0le2 11111 |
. . . . . . . . . . 11
⊢ 0 ≤
2 |
288 | 287 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 2) |
289 | | log1 24332 |
. . . . . . . . . . 11
⊢
(log‘1) = 0 |
290 | | chpdifbnd.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ≤ 𝐴) |
291 | | 1rp 11836 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
292 | | logleb 24349 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ+ ∧ 𝐴 ∈ ℝ+) → (1 ≤
𝐴 ↔ (log‘1) ≤
(log‘𝐴))) |
293 | 291, 5, 292 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 ≤ 𝐴 ↔ (log‘1) ≤ (log‘𝐴))) |
294 | 290, 293 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘1) ≤
(log‘𝐴)) |
295 | 289, 294 | syl5eqbrr 4689 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (log‘𝐴)) |
296 | 286, 38, 288, 295 | mulge0d 10604 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (2 ·
(log‘𝐴))) |
297 | 11, 7, 40, 296, 164 | lemul2ad 10964 |
. . . . . . . 8
⊢ (𝜑 → ((2 ·
(log‘𝐴)) ·
𝑌) ≤ ((2 ·
(log‘𝐴)) ·
(𝐴 · 𝑋))) |
298 | 49 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝐴) ∈
ℂ) |
299 | 298, 229,
247 | mulassd 10063 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) = ((2 · 𝐴) · ((log‘𝐴) · 𝑋))) |
300 | 233, 273,
229, 247 | mul4d 10248 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝐴) · ((log‘𝐴) · 𝑋)) = ((2 · (log‘𝐴)) · (𝐴 · 𝑋))) |
301 | 299, 300 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝐴) · (log‘𝐴)) · 𝑋) = ((2 · (log‘𝐴)) · (𝐴 · 𝑋))) |
302 | 297, 301 | breqtrrd 4681 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(log‘𝐴)) ·
𝑌) ≤ (((2 · 𝐴) · (log‘𝐴)) · 𝑋)) |
303 | 37, 41, 270, 271, 285, 302 | le2addd 10646 |
. . . . . 6
⊢ (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ≤ (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋))) |
304 | 44 | oveq1i 6660 |
. . . . . . 7
⊢ (𝐶 · 𝑋) = (((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) · 𝑋) |
305 | 47 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (𝐴 + 1)) ∈ ℂ) |
306 | 50 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝐴) · (log‘𝐴)) ∈
ℂ) |
307 | 305, 306,
247 | adddird 10065 |
. . . . . . 7
⊢ (𝜑 → (((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) · 𝑋) = (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋))) |
308 | 304, 307 | syl5eq 2668 |
. . . . . 6
⊢ (𝜑 → (𝐶 · 𝑋) = (((𝐵 · (𝐴 + 1)) · 𝑋) + (((2 · 𝐴) · (log‘𝐴)) · 𝑋))) |
309 | 303, 308 | breqtrrd 4681 |
. . . . 5
⊢ (𝜑 → ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌)) ≤ (𝐶 · 𝑋)) |
310 | 42, 53, 33, 309 | leadd2dd 10642 |
. . . 4
⊢ (𝜑 → (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + ((𝐵 · (𝑌 + 𝑋)) + ((2 · (log‘𝐴)) · 𝑌))) ≤ (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋))) |
311 | 28, 43, 54, 269, 310 | letrd 10194 |
. . 3
⊢ (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋))) |
312 | 32 | recnd 10068 |
. . . . 5
⊢ (𝜑 → (2 · (𝑌 − 𝑋)) ∈ ℂ) |
313 | 4, 24 | rplogcld 24375 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝑋) ∈
ℝ+) |
314 | 4, 313 | rerpdivcld 11903 |
. . . . . . 7
⊢ (𝜑 → (𝑋 / (log‘𝑋)) ∈ ℝ) |
315 | 52, 314 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → (𝐶 · (𝑋 / (log‘𝑋))) ∈ ℝ) |
316 | 315 | recnd 10068 |
. . . . 5
⊢ (𝜑 → (𝐶 · (𝑋 / (log‘𝑋))) ∈ ℂ) |
317 | 312, 316,
214 | adddird 10065 |
. . . 4
⊢ (𝜑 → (((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)) = (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋)))) |
318 | 52 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
319 | 314 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (𝑋 / (log‘𝑋)) ∈ ℂ) |
320 | 318, 319,
214 | mulassd 10063 |
. . . . . 6
⊢ (𝜑 → ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋)) = (𝐶 · ((𝑋 / (log‘𝑋)) · (log‘𝑋)))) |
321 | 313 | rpne0d 11877 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝑋) ≠ 0) |
322 | 247, 214,
321 | divcan1d 10802 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 / (log‘𝑋)) · (log‘𝑋)) = 𝑋) |
323 | 322 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (𝐶 · ((𝑋 / (log‘𝑋)) · (log‘𝑋))) = (𝐶 · 𝑋)) |
324 | 320, 323 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋)) = (𝐶 · 𝑋)) |
325 | 324 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + ((𝐶 · (𝑋 / (log‘𝑋))) · (log‘𝑋))) = (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋))) |
326 | 317, 325 | eqtrd 2656 |
. . 3
⊢ (𝜑 → (((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)) = (((2 · (𝑌 − 𝑋)) · (log‘𝑋)) + (𝐶 · 𝑋))) |
327 | 311, 326 | breqtrrd 4681 |
. 2
⊢ (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋))) |
328 | 32, 315 | readdcld 10069 |
. . 3
⊢ (𝜑 → ((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) ∈ ℝ) |
329 | 16, 328, 313 | lemul1d 11915 |
. 2
⊢ (𝜑 → (((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) ↔ (((ψ‘𝑌) − (ψ‘𝑋)) · (log‘𝑋)) ≤ (((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))) · (log‘𝑋)))) |
330 | 327, 329 | mpbird 247 |
1
⊢ (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋))))) |