Step | Hyp | Ref
| Expression |
1 | | simpl 476 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ+) |
2 | 1 | rprege0d 12188 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
3 | | flge0nn0 12940 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
5 | | faccl 13388 |
. . . . . . . . . 10
⊢
((⌊‘𝐴)
∈ ℕ0 → (!‘(⌊‘𝐴)) ∈ ℕ) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(!‘(⌊‘𝐴))
∈ ℕ) |
7 | 6 | nnrpd 12179 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(!‘(⌊‘𝐴))
∈ ℝ+) |
8 | | relogcl 24759 |
. . . . . . . 8
⊢
((!‘(⌊‘𝐴)) ∈ ℝ+ →
(log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
10 | | rpre 12145 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
11 | 10 | adantr 474 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ) |
12 | | relogcl 24759 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
13 | 12 | adantr 474 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘𝐴) ∈
ℝ) |
14 | | peano2rem 10690 |
. . . . . . . . 9
⊢
((log‘𝐴)
∈ ℝ → ((log‘𝐴) − 1) ∈
ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘𝐴) − 1)
∈ ℝ) |
16 | 11, 15 | remulcld 10407 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(𝐴 ·
((log‘𝐴) − 1))
∈ ℝ) |
17 | 9, 16 | resubcld 10803 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈
ℝ) |
18 | 17 | recnd 10405 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈
ℂ) |
19 | 18 | abscld 14583 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈
ℝ) |
20 | | peano2rem 10690 |
. . . 4
⊢
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈ ℝ →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ∈
ℝ) |
21 | 19, 20 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ∈
ℝ) |
22 | | ax-1cn 10330 |
. . . . 5
⊢ 1 ∈
ℂ |
23 | | subcl 10621 |
. . . . 5
⊢
((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈
ℂ) → (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈
ℂ) |
24 | 18, 22, 23 | sylancl 580 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈
ℂ) |
25 | 24 | abscld 14583 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ∈
ℝ) |
26 | | abs1 14444 |
. . . . 5
⊢
(abs‘1) = 1 |
27 | 26 | oveq2i 6933 |
. . . 4
⊢
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) =
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) |
28 | | abs2dif 14479 |
. . . . 5
⊢
((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈
ℂ) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
29 | 18, 22, 28 | sylancl 580 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
30 | 27, 29 | syl5eqbrr 4922 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
31 | | fveq2 6446 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (⌊‘𝑥) = (⌊‘𝐴)) |
32 | 31 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (1...(⌊‘𝑥)) = (1...(⌊‘𝐴))) |
33 | 32 | sumeq1d 14839 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
34 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
35 | | fveq2 6446 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴)) |
36 | 35 | oveq1d 6937 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((log‘𝑥) − 1) = ((log‘𝐴) − 1)) |
37 | 34, 36 | oveq12d 6940 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 · ((log‘𝑥) − 1)) = (𝐴 · ((log‘𝐴) − 1))) |
38 | 33, 37 | oveq12d 6940 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
39 | | eqid 2778 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) |
40 | | ovex 6954 |
. . . . . . . . 9
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) ∈ V |
41 | 38, 39, 40 | fvmpt3i 6547 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
42 | 41 | adantr 474 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
43 | | logfac 24784 |
. . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
44 | 4, 43 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
45 | 44 | oveq1d 6937 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
46 | 42, 45 | eqtr4d 2817 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) =
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) |
47 | | 1rp 12141 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
48 | | fveq2 6446 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (⌊‘𝑥) =
(⌊‘1)) |
49 | | 1z 11759 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
50 | | flid 12928 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → (⌊‘1) = 1) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(⌊‘1) = 1 |
52 | 48, 51 | syl6eq 2830 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (⌊‘𝑥) = 1) |
53 | 52 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 →
(1...(⌊‘𝑥)) =
(1...1)) |
54 | 53 | sumeq1d 14839 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...1)(log‘𝑛)) |
55 | | 0cn 10368 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
56 | | fveq2 6446 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (log‘𝑛) =
(log‘1)) |
57 | | log1 24769 |
. . . . . . . . . . . . . 14
⊢
(log‘1) = 0 |
58 | 56, 57 | syl6eq 2830 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (log‘𝑛) = 0) |
59 | 58 | fsum1 14883 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ 0 ∈ ℂ) → Σ𝑛 ∈ (1...1)(log‘𝑛) = 0) |
60 | 49, 55, 59 | mp2an 682 |
. . . . . . . . . . 11
⊢
Σ𝑛 ∈
(1...1)(log‘𝑛) =
0 |
61 | 54, 60 | syl6eq 2830 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) = 0) |
62 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → 𝑥 = 1) |
63 | | fveq2 6446 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (log‘𝑥) =
(log‘1)) |
64 | 63, 57 | syl6eq 2830 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (log‘𝑥) = 0) |
65 | 64 | oveq1d 6937 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((log‘𝑥) − 1) = (0 −
1)) |
66 | 62, 65 | oveq12d 6940 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (1 · (0 −
1))) |
67 | 55, 22 | subcli 10699 |
. . . . . . . . . . . 12
⊢ (0
− 1) ∈ ℂ |
68 | 67 | mulid2i 10382 |
. . . . . . . . . . 11
⊢ (1
· (0 − 1)) = (0 − 1) |
69 | 66, 68 | syl6eq 2830 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (0 −
1)) |
70 | 61, 69 | oveq12d 6940 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (0 − (0 −
1))) |
71 | | nncan 10652 |
. . . . . . . . . 10
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → (0 − (0 − 1)) =
1) |
72 | 55, 22, 71 | mp2an 682 |
. . . . . . . . 9
⊢ (0
− (0 − 1)) = 1 |
73 | 70, 72 | syl6eq 2830 |
. . . . . . . 8
⊢ (𝑥 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = 1) |
74 | 73, 39, 40 | fvmpt3i 6547 |
. . . . . . 7
⊢ (1 ∈
ℝ+ → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1) =
1) |
75 | 47, 74 | mp1i 13 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1) =
1) |
76 | 46, 75 | oveq12d 6940 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1)) =
(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) |
77 | 76 | fveq2d 6450 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) =
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
78 | | ioorp 12563 |
. . . . . 6
⊢
(0(,)+∞) = ℝ+ |
79 | 78 | eqcomi 2787 |
. . . . 5
⊢
ℝ+ = (0(,)+∞) |
80 | | nnuz 12029 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
81 | 49 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℤ) |
82 | | 1re 10376 |
. . . . . 6
⊢ 1 ∈
ℝ |
83 | 82 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℝ) |
84 | | pnfxr 10430 |
. . . . . 6
⊢ +∞
∈ ℝ* |
85 | 84 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
+∞ ∈ ℝ*) |
86 | | 1nn0 11660 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
87 | 82, 86 | nn0addge1i 11692 |
. . . . . 6
⊢ 1 ≤ (1
+ 1) |
88 | 87 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ (1 + 1)) |
89 | | 0red 10380 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 0
∈ ℝ) |
90 | | rpre 12145 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
91 | 90 | adantl 475 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ 𝑥 ∈
ℝ) |
92 | | relogcl 24759 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
93 | 92 | adantl 475 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
94 | | peano2rem 10690 |
. . . . . . 7
⊢
((log‘𝑥)
∈ ℝ → ((log‘𝑥) − 1) ∈ ℝ) |
95 | 93, 94 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ ((log‘𝑥)
− 1) ∈ ℝ) |
96 | 91, 95 | remulcld 10407 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ (𝑥 ·
((log‘𝑥) − 1))
∈ ℝ) |
97 | | nnrp 12150 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) |
98 | 97, 93 | sylan2 586 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℕ) →
(log‘𝑥) ∈
ℝ) |
99 | | advlog 24837 |
. . . . . 6
⊢ (ℝ
D (𝑥 ∈
ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
100 | 99 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(ℝ D (𝑥 ∈
ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) |
101 | | fveq2 6446 |
. . . . 5
⊢ (𝑥 = 𝑛 → (log‘𝑥) = (log‘𝑛)) |
102 | | simp32 1224 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → 𝑥 ≤ 𝑛) |
103 | | logleb 24786 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛))) |
104 | 103 | 3ad2ant2 1125 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛))) |
105 | 102, 104 | mpbid 224 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (log‘𝑥) ≤ (log‘𝑛)) |
106 | | simprr 763 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
107 | | simprl 761 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
108 | | logleb 24786 |
. . . . . . . 8
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
109 | 47, 107, 108 | sylancr 581 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥))) |
110 | 106, 109 | mpbid 224 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥)) |
111 | 57, 110 | syl5eqbrr 4922 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥)) |
112 | 47 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℝ+) |
113 | | 1le1 11003 |
. . . . . 6
⊢ 1 ≤
1 |
114 | 113 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ 1) |
115 | | simpr 479 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ 𝐴) |
116 | 11 | rexrd 10426 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ*) |
117 | | pnfge 12275 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ 𝐴 ≤
+∞) |
118 | 116, 117 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ≤
+∞) |
119 | 79, 80, 81, 83, 85, 88, 89, 96, 93, 98, 100, 101, 105, 39, 111, 112, 1, 114, 115, 118, 35 | dvfsum2 24234 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) ≤
(log‘𝐴)) |
120 | 77, 119 | eqbrtrrd 4910 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ≤
(log‘𝐴)) |
121 | 21, 25, 13, 30, 120 | letrd 10533 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(log‘𝐴)) |
122 | 19, 83, 13 | lesubaddd 10972 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(log‘𝐴) ↔
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))) |
123 | 121, 122 | mpbid 224 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1)) |