Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ+) |
2 | 1 | rprege0d 11879 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
3 | | flge0nn0 12621 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
5 | | faccl 13070 |
. . . . . . . . . 10
⊢
((⌊‘𝐴)
∈ ℕ0 → (!‘(⌊‘𝐴)) ∈ ℕ) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(!‘(⌊‘𝐴))
∈ ℕ) |
7 | 6 | nnrpd 11870 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(!‘(⌊‘𝐴))
∈ ℝ+) |
8 | | relogcl 24322 |
. . . . . . . 8
⊢
((!‘(⌊‘𝐴)) ∈ ℝ+ →
(log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
10 | | rpre 11839 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
11 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ) |
12 | | relogcl 24322 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
13 | 12 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘𝐴) ∈
ℝ) |
14 | | peano2rem 10348 |
. . . . . . . . 9
⊢
((log‘𝐴)
∈ ℝ → ((log‘𝐴) − 1) ∈
ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘𝐴) − 1)
∈ ℝ) |
16 | 11, 15 | remulcld 10070 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(𝐴 ·
((log‘𝐴) − 1))
∈ ℝ) |
17 | 9, 16 | resubcld 10458 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈
ℝ) |
18 | 17 | recnd 10068 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈
ℂ) |
19 | 18 | abscld 14175 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈
ℝ) |
20 | | peano2rem 10348 |
. . . 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 9994 |
. . . . 5
⊢ 1 ∈
ℂ |
23 | | subcl 10280 |
. . . . 5
⊢
((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈
ℂ) → (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈
ℂ) |
24 | 18, 22, 23 | sylancl 694 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈
ℂ) |
25 | 24 | abscld 14175 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ∈
ℝ) |
26 | | abs1 14037 |
. . . . 5
⊢
(abs‘1) = 1 |
27 | 26 | oveq2i 6661 |
. . . 4
⊢
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) =
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) |
28 | | abs2dif 14072 |
. . . . 5
⊢
((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈
ℂ) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
29 | 18, 22, 28 | sylancl 694 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
30 | 27, 29 | syl5eqbrr 4689 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
31 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (⌊‘𝑥) = (⌊‘𝐴)) |
32 | 31 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (1...(⌊‘𝑥)) = (1...(⌊‘𝐴))) |
33 | 32 | sumeq1d 14431 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
34 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
35 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴)) |
36 | 35 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((log‘𝑥) − 1) = ((log‘𝐴) − 1)) |
37 | 34, 36 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 · ((log‘𝑥) − 1)) = (𝐴 · ((log‘𝐴) − 1))) |
38 | 33, 37 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
39 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) |
40 | | ovex 6678 |
. . . . . . . . 9
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) ∈ V |
41 | 38, 39, 40 | fvmpt3i 6287 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
42 | 41 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
43 | | logfac 24347 |
. . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
44 | 4, 43 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
45 | 44 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) |
46 | 42, 45 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) =
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) |
47 | | 1rp 11836 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
48 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (⌊‘𝑥) =
(⌊‘1)) |
49 | | 1z 11407 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
50 | | flid 12609 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → (⌊‘1) = 1) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(⌊‘1) = 1 |
52 | 48, 51 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (⌊‘𝑥) = 1) |
53 | 52 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 →
(1...(⌊‘𝑥)) =
(1...1)) |
54 | 53 | sumeq1d 14431 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...1)(log‘𝑛)) |
55 | | 0cn 10032 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
56 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (log‘𝑛) =
(log‘1)) |
57 | | log1 24332 |
. . . . . . . . . . . . . 14
⊢
(log‘1) = 0 |
58 | 56, 57 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (log‘𝑛) = 0) |
59 | 58 | fsum1 14476 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ 0 ∈ ℂ) → Σ𝑛 ∈ (1...1)(log‘𝑛) = 0) |
60 | 49, 55, 59 | mp2an 708 |
. . . . . . . . . . 11
⊢
Σ𝑛 ∈
(1...1)(log‘𝑛) =
0 |
61 | 54, 60 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) = 0) |
62 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → 𝑥 = 1) |
63 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (log‘𝑥) =
(log‘1)) |
64 | 63, 57 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (log‘𝑥) = 0) |
65 | 64 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((log‘𝑥) − 1) = (0 −
1)) |
66 | 62, 65 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (1 · (0 −
1))) |
67 | 55, 22 | subcli 10357 |
. . . . . . . . . . . 12
⊢ (0
− 1) ∈ ℂ |
68 | 67 | mulid2i 10043 |
. . . . . . . . . . 11
⊢ (1
· (0 − 1)) = (0 − 1) |
69 | 66, 68 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (0 −
1)) |
70 | 61, 69 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (0 − (0 −
1))) |
71 | | nncan 10310 |
. . . . . . . . . 10
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → (0 − (0 − 1)) =
1) |
72 | 55, 22, 71 | mp2an 708 |
. . . . . . . . 9
⊢ (0
− (0 − 1)) = 1 |
73 | 70, 72 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑥 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = 1) |
74 | 73, 39, 40 | fvmpt3i 6287 |
. . . . . . 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 6668 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1)) =
(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) |
77 | 76 | fveq2d 6195 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) =
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) |
78 | | ioorp 12251 |
. . . . . 6
⊢
(0(,)+∞) = ℝ+ |
79 | 78 | eqcomi 2631 |
. . . . 5
⊢
ℝ+ = (0(,)+∞) |
80 | | nnuz 11723 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
81 | 49 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℤ) |
82 | | 1re 10039 |
. . . . . 6
⊢ 1 ∈
ℝ |
83 | 82 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℝ) |
84 | | pnfxr 10092 |
. . . . . 6
⊢ +∞
∈ ℝ* |
85 | 84 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
+∞ ∈ ℝ*) |
86 | | 1nn0 11308 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
87 | 82, 86 | nn0addge1i 11341 |
. . . . . 6
⊢ 1 ≤ (1
+ 1) |
88 | 87 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ (1 + 1)) |
89 | | 0red 10041 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 0
∈ ℝ) |
90 | | rpre 11839 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
91 | 90 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ 𝑥 ∈
ℝ) |
92 | | relogcl 24322 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
93 | 92 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
94 | | peano2rem 10348 |
. . . . . . 7
⊢
((log‘𝑥)
∈ ℝ → ((log‘𝑥) − 1) ∈ ℝ) |
95 | 93, 94 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ ((log‘𝑥)
− 1) ∈ ℝ) |
96 | 91, 95 | remulcld 10070 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ (𝑥 ·
((log‘𝑥) − 1))
∈ ℝ) |
97 | | nnrp 11842 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) |
98 | 97, 93 | sylan2 491 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℕ) →
(log‘𝑥) ∈
ℝ) |
99 | | advlog 24400 |
. . . . . 6
⊢ (ℝ
D (𝑥 ∈
ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
100 | 99 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(ℝ D (𝑥 ∈
ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) |
101 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = 𝑛 → (log‘𝑥) = (log‘𝑛)) |
102 | | simp32 1098 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → 𝑥 ≤ 𝑛) |
103 | | logleb 24349 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛))) |
104 | 103 | 3ad2ant2 1083 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛))) |
105 | 102, 104 | mpbid 222 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (log‘𝑥) ≤ (log‘𝑛)) |
106 | | simprr 796 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
107 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
108 | | logleb 24349 |
. . . . . . . 8
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
109 | 47, 107, 108 | sylancr 695 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥))) |
110 | 106, 109 | mpbid 222 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥)) |
111 | 57, 110 | syl5eqbrr 4689 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥)) |
112 | 47 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℝ+) |
113 | | 1le1 10655 |
. . . . . 6
⊢ 1 ≤
1 |
114 | 113 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ 1) |
115 | | simpr 477 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ 𝐴) |
116 | 11 | rexrd 10089 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ*) |
117 | | pnfge 11964 |
. . . . . 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 23797 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) ≤
(log‘𝐴)) |
120 | 77, 119 | eqbrtrrd 4677 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ≤
(log‘𝐴)) |
121 | 21, 25, 13, 30, 120 | letrd 10194 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(log‘𝐴)) |
122 | 19, 83, 13 | lesubaddd 10624 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(log‘𝐴) ↔
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))) |
123 | 121, 122 | mpbid 222 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1)) |