Step | Hyp | Ref
| Expression |
1 | | ioossre 13021 |
. . 3
⊢
(1(,)+∞) ⊆ ℝ |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (1(,)+∞)
⊆ ℝ) |
3 | | 1red 10859 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 1 ∈
ℝ) |
4 | 2 | sselda 3916 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ) |
5 | | 1rp 12615 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ+) |
7 | | 1red 10859 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ) |
8 | | eliooord 13019 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
9 | 8 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
10 | 9 | simpld 498 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥) |
11 | 7, 4, 10 | ltled 11005 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥) |
12 | 4, 6, 11 | rpgecld 12692 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ+) |
13 | | pntpbnd.r |
. . . . . . . . . 10
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
14 | 13 | pntrf 26468 |
. . . . . . . . 9
⊢ 𝑅:ℝ+⟶ℝ |
15 | 14 | ffvelrni 6922 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
16 | 12, 15 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ) |
17 | 16 | recnd 10886 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ) |
18 | 17 | abscld 15025 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(𝑅‘𝑥)) ∈
ℝ) |
19 | 12 | relogcld 25535 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ) |
20 | 18, 19 | remulcld 10888 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈
ℝ) |
21 | | 2re 11929 |
. . . . . . 7
⊢ 2 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈
ℝ) |
23 | 4, 10 | rplogcld 25541 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ+) |
24 | 22, 23 | rerpdivcld 12684 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → (2 /
(log‘𝑥)) ∈
ℝ) |
25 | | fzfid 13571 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) →
(1...(⌊‘(𝑥 /
𝐴))) ∈
Fin) |
26 | 12 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) → 𝑥 ∈
ℝ+) |
27 | | elfznn 13166 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴))) → 𝑛 ∈
ℕ) |
28 | 27 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) → 𝑛 ∈
ℕ) |
29 | 28 | nnrpd 12651 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) → 𝑛 ∈
ℝ+) |
30 | 26, 29 | rpdivcld 12670 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) → (𝑥 / 𝑛) ∈
ℝ+) |
31 | 14 | ffvelrni 6922 |
. . . . . . . . . 10
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
33 | 32 | recnd 10886 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
34 | 33 | abscld 15025 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) →
(abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
35 | 29 | relogcld 25535 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) →
(log‘𝑛) ∈
ℝ) |
36 | 34, 35 | remulcld 10888 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))) →
((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ) |
37 | 25, 36 | fsumrecl 15323 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ) |
38 | 24, 37 | remulcld 10888 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℝ) |
39 | 20, 38 | resubcld 11285 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ∈ ℝ) |
40 | 39, 12 | rerpdivcld 12684 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) →
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) ∈ ℝ) |
41 | 13 | pntrmax 26469 |
. . 3
⊢
∃𝑐 ∈
ℝ+ ∀𝑦 ∈ ℝ+
(abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝑐 |
42 | | eqid 2738 |
. . . . 5
⊢ (𝑎 ∈ ℝ ↦
Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
43 | | eqid 2738 |
. . . . 5
⊢ (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0)) =
(𝑎 ∈ ℝ ↦
if(𝑎 ∈
ℝ+, (𝑎
· (log‘𝑎)),
0)) |
44 | | simprl 771 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝑐)) → 𝑐 ∈ ℝ+) |
45 | | simprr 773 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝑐)) → ∀𝑦 ∈ ℝ+
(abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝑐) |
46 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝑐)) → 𝐴 ∈ ℝ) |
47 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝑐)) → 1 ≤ 𝐴) |
48 | 42, 13, 43, 44, 45, 46, 47 | pntrlog2bndlem6 26488 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝑐)) → (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ ≤𝑂(1)) |
49 | 48 | rexlimdvaa 3212 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (∃𝑐 ∈ ℝ+
∀𝑦 ∈
ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝑐 → (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ ≤𝑂(1))) |
50 | 41, 49 | mpi 20 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ ≤𝑂(1)) |
51 | | simprl 771 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) → 𝑦 ∈
ℝ) |
52 | | chpcl 26030 |
. . . . 5
⊢ (𝑦 ∈ ℝ →
(ψ‘𝑦) ∈
ℝ) |
53 | 51, 52 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) →
(ψ‘𝑦) ∈
ℝ) |
54 | 53, 51 | readdcld 10887 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) →
((ψ‘𝑦) + 𝑦) ∈
ℝ) |
55 | 5 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) → 1 ∈
ℝ+) |
56 | | simprr 773 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) → 1 ≤ 𝑦) |
57 | 51, 55, 56 | rpgecld 12692 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) → 𝑦 ∈
ℝ+) |
58 | 57 | relogcld 25535 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) → (log‘𝑦) ∈
ℝ) |
59 | 54, 58 | remulcld 10888 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) →
(((ψ‘𝑦) + 𝑦) · (log‘𝑦)) ∈
ℝ) |
60 | 40 | adantr 484 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) ∈ ℝ) |
61 | 53 | ad2ant2r 747 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (ψ‘𝑦) ∈ ℝ) |
62 | | simprll 779 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ) |
63 | 61, 62 | readdcld 10887 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑦) + 𝑦) ∈ ℝ) |
64 | 57 | ad2ant2r 747 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ+) |
65 | 64 | relogcld 25535 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑦) ∈ ℝ) |
66 | 63, 65 | remulcld 10888 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (((ψ‘𝑦) + 𝑦) · (log‘𝑦)) ∈ ℝ) |
67 | 12 | adantr 484 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ+) |
68 | 66, 67 | rerpdivcld 12684 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((((ψ‘𝑦) + 𝑦) · (log‘𝑦)) / 𝑥) ∈ ℝ) |
69 | 16 | adantr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (𝑅‘𝑥) ∈ ℝ) |
70 | 69 | recnd 10886 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (𝑅‘𝑥) ∈ ℂ) |
71 | 70 | abscld 15025 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(𝑅‘𝑥)) ∈ ℝ) |
72 | 67 | relogcld 25535 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ∈ ℝ) |
73 | 71, 72 | remulcld 10888 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ) |
74 | 24 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (2 / (log‘𝑥)) ∈ ℝ) |
75 | 37 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ) |
76 | 74, 75 | remulcld 10888 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℝ) |
77 | 73, 76 | resubcld 11285 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ∈ ℝ) |
78 | 21 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℝ) |
79 | 4 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ) |
80 | 10 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 1 < 𝑥) |
81 | 79, 80 | rplogcld 25541 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ∈
ℝ+) |
82 | | 2rp 12616 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
83 | 82 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈
ℝ+) |
84 | 83 | rpge0d 12657 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ 2) |
85 | 78, 81, 84 | divge0d 12693 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (2 / (log‘𝑥))) |
86 | | fzfid 13571 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (1...(⌊‘(𝑥 / 𝐴))) ∈ Fin) |
87 | 36 | adantlr 715 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ) |
88 | 33 | adantlr 715 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
89 | 88 | abscld 15025 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
90 | 29 | adantlr 715 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → 𝑛 ∈ ℝ+) |
91 | 90 | relogcld 25535 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → (log‘𝑛) ∈ ℝ) |
92 | 88 | absge0d 15033 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → 0 ≤ (abs‘(𝑅‘(𝑥 / 𝑛)))) |
93 | 90 | rpred 12653 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → 𝑛 ∈ ℝ) |
94 | 27 | adantl 485 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → 𝑛 ∈ ℕ) |
95 | 94 | nnge1d 11903 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → 1 ≤ 𝑛) |
96 | 93, 95 | logge0d 25542 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → 0 ≤ (log‘𝑛)) |
97 | 89, 91, 92, 96 | mulge0d 11434 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 1 ≤ 𝐴)
∧ 𝑥 ∈
(1(,)+∞)) ∧ ((𝑦
∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))) → 0 ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) |
98 | 86, 87, 97 | fsumge0 15384 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) |
99 | 74, 75, 85, 98 | mulge0d 11434 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) |
100 | 73, 76 | subge02d 11449 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (0 ≤ ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) ↔ (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ≤ ((abs‘(𝑅‘𝑥)) · (log‘𝑥)))) |
101 | 99, 100 | mpbid 235 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ≤ ((abs‘(𝑅‘𝑥)) · (log‘𝑥))) |
102 | 70 | absge0d 15033 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (abs‘(𝑅‘𝑥))) |
103 | 81 | rpge0d 12657 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (log‘𝑥)) |
104 | | chpcl 26030 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
105 | 79, 104 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (ψ‘𝑥) ∈ ℝ) |
106 | 105, 79 | readdcld 10887 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑥) + 𝑥) ∈ ℝ) |
107 | 13 | pntrval 26467 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥)) |
108 | 67, 107 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥)) |
109 | 108 | fveq2d 6740 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(𝑅‘𝑥)) = (abs‘((ψ‘𝑥) − 𝑥))) |
110 | 105 | recnd 10886 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (ψ‘𝑥) ∈ ℂ) |
111 | 79 | recnd 10886 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℂ) |
112 | 110, 111 | abs2dif2d 15047 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((ψ‘𝑥) − 𝑥)) ≤ ((abs‘(ψ‘𝑥)) + (abs‘𝑥))) |
113 | | chpge0 26032 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 0 ≤
(ψ‘𝑥)) |
114 | 79, 113 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (ψ‘𝑥)) |
115 | 105, 114 | absidd 15011 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(ψ‘𝑥)) = (ψ‘𝑥)) |
116 | 67 | rpge0d 12657 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ 𝑥) |
117 | 79, 116 | absidd 15011 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (abs‘𝑥) = 𝑥) |
118 | 115, 117 | oveq12d 7250 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((abs‘(ψ‘𝑥)) + (abs‘𝑥)) = ((ψ‘𝑥) + 𝑥)) |
119 | 112, 118 | breqtrd 5094 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((ψ‘𝑥) − 𝑥)) ≤ ((ψ‘𝑥) + 𝑥)) |
120 | 109, 119 | eqbrtrd 5090 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(𝑅‘𝑥)) ≤ ((ψ‘𝑥) + 𝑥)) |
121 | | simprr 773 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦) |
122 | 79, 62, 121 | ltled 11005 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≤ 𝑦) |
123 | | chpwordi 26063 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (ψ‘𝑥) ≤ (ψ‘𝑦)) |
124 | 79, 62, 122, 123 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (ψ‘𝑥) ≤ (ψ‘𝑦)) |
125 | 105, 79, 61, 62, 124, 122 | le2addd 11476 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑥) + 𝑥) ≤ ((ψ‘𝑦) + 𝑦)) |
126 | 71, 106, 63, 120, 125 | letrd 11014 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(𝑅‘𝑥)) ≤ ((ψ‘𝑦) + 𝑦)) |
127 | 67, 64 | logled 25539 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 ≤ 𝑦 ↔ (log‘𝑥) ≤ (log‘𝑦))) |
128 | 122, 127 | mpbid 235 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ≤ (log‘𝑦)) |
129 | 71, 63, 72, 65, 102, 103, 126, 128 | lemul12ad 11799 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ≤ (((ψ‘𝑦) + 𝑦) · (log‘𝑦))) |
130 | 77, 73, 66, 101, 129 | letrd 11014 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ≤ (((ψ‘𝑦) + 𝑦) · (log‘𝑦))) |
131 | 77, 66, 67, 130 | lediv1dd 12711 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) ≤ ((((ψ‘𝑦) + 𝑦) · (log‘𝑦)) / 𝑥)) |
132 | 5 | a1i 11 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 1 ∈
ℝ+) |
133 | | chpge0 26032 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → 0 ≤
(ψ‘𝑦)) |
134 | 62, 133 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (ψ‘𝑦)) |
135 | 64 | rpge0d 12657 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ 𝑦) |
136 | 61, 62, 134, 135 | addge0d 11433 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ ((ψ‘𝑦) + 𝑦)) |
137 | | simprlr 780 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 1 ≤ 𝑦) |
138 | 62, 137 | logge0d 25542 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (log‘𝑦)) |
139 | 63, 65, 136, 138 | mulge0d 11434 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (((ψ‘𝑦) + 𝑦) · (log‘𝑦))) |
140 | 11 | adantr 484 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 1 ≤ 𝑥) |
141 | 132, 67, 66, 139, 140 | lediv2ad 12675 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((((ψ‘𝑦) + 𝑦) · (log‘𝑦)) / 𝑥) ≤ ((((ψ‘𝑦) + 𝑦) · (log‘𝑦)) / 1)) |
142 | 61 | recnd 10886 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (ψ‘𝑦) ∈ ℂ) |
143 | 62 | recnd 10886 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℂ) |
144 | 142, 143 | addcld 10877 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑦) + 𝑦) ∈ ℂ) |
145 | 65 | recnd 10886 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑦) ∈ ℂ) |
146 | 144, 145 | mulcld 10878 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → (((ψ‘𝑦) + 𝑦) · (log‘𝑦)) ∈ ℂ) |
147 | 146 | div1d 11625 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((((ψ‘𝑦) + 𝑦) · (log‘𝑦)) / 1) = (((ψ‘𝑦) + 𝑦) · (log‘𝑦))) |
148 | 141, 147 | breqtrd 5094 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((((ψ‘𝑦) + 𝑦) · (log‘𝑦)) / 𝑥) ≤ (((ψ‘𝑦) + 𝑦) · (log‘𝑦))) |
149 | 60, 68, 66, 131, 148 | letrd 11014 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑥 ∈ (1(,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤
𝑦) ∧ 𝑥 < 𝑦)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) ≤ (((ψ‘𝑦) + 𝑦) · (log‘𝑦))) |
150 | 2, 3, 40, 50, 59, 149 | lo1bddrp 15111 |
1
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → ∃𝑐 ∈ ℝ+
∀𝑥 ∈
(1(,)+∞)((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) ≤ 𝑐) |