Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ+) |
2 | 1 | rprege0d 12779 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
3 | | flge0nn0 13540 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
5 | 4 | faccld 13998 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(!‘(⌊‘𝐴))
∈ ℕ) |
6 | 5 | nnrpd 12770 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(!‘(⌊‘𝐴))
∈ ℝ+) |
7 | | relogcl 25731 |
. . . . . . . 8
⊢
((!‘(⌊‘𝐴)) ∈ ℝ+ →
(log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
9 | | rpre 12738 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
10 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ) |
11 | | relogcl 25731 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
12 | 11 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘𝐴) ∈
ℝ) |
13 | | peano2rem 11288 |
. . . . . . . . 9
⊢
((log‘𝐴)
∈ ℝ → ((log‘𝐴) − 1) ∈
ℝ) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘𝐴) − 1)
∈ ℝ) |
15 | 10, 14 | remulcld 11005 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(𝐴 ·
((log‘𝐴) − 1))
∈ ℝ) |
16 | 8, 15 | resubcld 11403 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈
ℝ) |
17 | 16 | recnd 11003 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈
ℂ) |
18 | 17 | abscld 15148 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈
ℝ) |
19 | | peano2rem 11288 |
. . . 4
⊢
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈ ℝ →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ∈
ℝ) |
20 | 18, 19 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ∈
ℝ) |
21 | | ax-1cn 10929 |
. . . . 5
⊢ 1 ∈
ℂ |
22 | | subcl 11220 |
. . . . 5
⊢
((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈
ℂ) → (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈
ℂ) |
23 | 17, 21, 22 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈
ℂ) |
24 | 23 | abscld 15148 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ∈
ℝ) |
25 | | abs1 15009 |
. . . . 5
⊢
(abs‘1) = 1 |
26 | 25 | oveq2i 7286 |
. . . 4
⊢
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) =
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) |
27 | | abs2dif 15044 |
. . . . 5
⊢
((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈
ℂ) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
28 | 17, 21, 27 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
29 | 26, 28 | eqbrtrrid 5110 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
30 | | fveq2 6774 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (⌊‘𝑥) = (⌊‘𝐴)) |
31 | 30 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (1...(⌊‘𝑥)) = (1...(⌊‘𝐴))) |
32 | 31 | sumeq1d 15413 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
33 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
34 | | fveq2 6774 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴)) |
35 | 34 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((log‘𝑥) − 1) = ((log‘𝐴) − 1)) |
36 | 33, 35 | oveq12d 7293 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 · ((log‘𝑥) − 1)) = (𝐴 · ((log‘𝐴) − 1))) |
37 | 32, 36 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
38 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) |
39 | | ovex 7308 |
. . . . . . . . 9
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) ∈ V |
40 | 37, 38, 39 | fvmpt3i 6880 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
41 | 40 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
42 | | logfac 25756 |
. . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
43 | 4, 42 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
44 | 43 | oveq1d 7290 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
45 | 41, 44 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) =
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) |
46 | | 1rp 12734 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
47 | | fveq2 6774 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (⌊‘𝑥) =
(⌊‘1)) |
48 | | 1z 12350 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
49 | | flid 13528 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → (⌊‘1) = 1) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(⌊‘1) = 1 |
51 | 47, 50 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (⌊‘𝑥) = 1) |
52 | 51 | oveq2d 7291 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 →
(1...(⌊‘𝑥)) =
(1...1)) |
53 | 52 | sumeq1d 15413 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...1)(log‘𝑛)) |
54 | | 0cn 10967 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
55 | | fveq2 6774 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (log‘𝑛) =
(log‘1)) |
56 | | log1 25741 |
. . . . . . . . . . . . . 14
⊢
(log‘1) = 0 |
57 | 55, 56 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (log‘𝑛) = 0) |
58 | 57 | fsum1 15459 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ 0 ∈ ℂ) → Σ𝑛 ∈ (1...1)(log‘𝑛) = 0) |
59 | 48, 54, 58 | mp2an 689 |
. . . . . . . . . . 11
⊢
Σ𝑛 ∈
(1...1)(log‘𝑛) =
0 |
60 | 53, 59 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) = 0) |
61 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → 𝑥 = 1) |
62 | | fveq2 6774 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (log‘𝑥) =
(log‘1)) |
63 | 62, 56 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (log‘𝑥) = 0) |
64 | 63 | oveq1d 7290 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((log‘𝑥) − 1) = (0 −
1)) |
65 | 61, 64 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (1 · (0 −
1))) |
66 | 54, 21 | subcli 11297 |
. . . . . . . . . . . 12
⊢ (0
− 1) ∈ ℂ |
67 | 66 | mulid2i 10980 |
. . . . . . . . . . 11
⊢ (1
· (0 − 1)) = (0 − 1) |
68 | 65, 67 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (0 −
1)) |
69 | 60, 68 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (0 − (0 −
1))) |
70 | | nncan 11250 |
. . . . . . . . . 10
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → (0 − (0 − 1)) =
1) |
71 | 54, 21, 70 | mp2an 689 |
. . . . . . . . 9
⊢ (0
− (0 − 1)) = 1 |
72 | 69, 71 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑥 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = 1) |
73 | 72, 38, 39 | fvmpt3i 6880 |
. . . . . . 7
⊢ (1 ∈
ℝ+ → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1) =
1) |
74 | 46, 73 | mp1i 13 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1) =
1) |
75 | 45, 74 | oveq12d 7293 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1)) =
(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) |
76 | 75 | fveq2d 6778 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) =
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
77 | | ioorp 13157 |
. . . . . 6
⊢
(0(,)+∞) = ℝ+ |
78 | 77 | eqcomi 2747 |
. . . . 5
⊢
ℝ+ = (0(,)+∞) |
79 | | nnuz 12621 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
80 | 48 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℤ) |
81 | | 1re 10975 |
. . . . . 6
⊢ 1 ∈
ℝ |
82 | 81 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℝ) |
83 | | pnfxr 11029 |
. . . . . 6
⊢ +∞
∈ ℝ* |
84 | 83 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
+∞ ∈ ℝ*) |
85 | | 1nn0 12249 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
86 | 81, 85 | nn0addge1i 12281 |
. . . . . 6
⊢ 1 ≤ (1
+ 1) |
87 | 86 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ (1 + 1)) |
88 | | 0red 10978 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 0
∈ ℝ) |
89 | | rpre 12738 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
90 | 89 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ 𝑥 ∈
ℝ) |
91 | | relogcl 25731 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
92 | 91 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
93 | | peano2rem 11288 |
. . . . . . 7
⊢
((log‘𝑥)
∈ ℝ → ((log‘𝑥) − 1) ∈ ℝ) |
94 | 92, 93 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ ((log‘𝑥)
− 1) ∈ ℝ) |
95 | 90, 94 | remulcld 11005 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ (𝑥 ·
((log‘𝑥) − 1))
∈ ℝ) |
96 | | nnrp 12741 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) |
97 | 96, 92 | sylan2 593 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℕ) →
(log‘𝑥) ∈
ℝ) |
98 | | advlog 25809 |
. . . . . 6
⊢ (ℝ
D (𝑥 ∈
ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
99 | 98 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(ℝ D (𝑥 ∈
ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) |
100 | | fveq2 6774 |
. . . . 5
⊢ (𝑥 = 𝑛 → (log‘𝑥) = (log‘𝑛)) |
101 | | simp32 1209 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → 𝑥 ≤ 𝑛) |
102 | | logleb 25758 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛))) |
103 | 102 | 3ad2ant2 1133 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛))) |
104 | 101, 103 | mpbid 231 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (log‘𝑥) ≤ (log‘𝑛)) |
105 | | simprr 770 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
106 | | simprl 768 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
107 | | logleb 25758 |
. . . . . . . 8
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
108 | 46, 106, 107 | sylancr 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥))) |
109 | 105, 108 | mpbid 231 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥)) |
110 | 56, 109 | eqbrtrrid 5110 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥)) |
111 | 46 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℝ+) |
112 | | 1le1 11603 |
. . . . . 6
⊢ 1 ≤
1 |
113 | 112 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ 1) |
114 | | simpr 485 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ 𝐴) |
115 | 10 | rexrd 11025 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ*) |
116 | | pnfge 12866 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ 𝐴 ≤
+∞) |
117 | 115, 116 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ≤
+∞) |
118 | 78, 79, 80, 82, 84, 87, 88, 95, 92, 97, 99, 100, 104, 38, 110, 111, 1, 113, 114, 117, 34 | dvfsum2 25198 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) ≤
(log‘𝐴)) |
119 | 76, 118 | eqbrtrrd 5098 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ≤
(log‘𝐴)) |
120 | 20, 24, 12, 29, 119 | letrd 11132 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(log‘𝐴)) |
121 | 18, 82, 12 | lesubaddd 11572 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(log‘𝐴) ↔
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))) |
122 | 120, 121 | mpbid 231 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1)) |