| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ+) | 
| 2 | 1 | rprege0d 13084 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) | 
| 3 |  | flge0nn0 13860 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) | 
| 4 | 2, 3 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(⌊‘𝐴) ∈
ℕ0) | 
| 5 | 4 | faccld 14323 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(!‘(⌊‘𝐴))
∈ ℕ) | 
| 6 | 5 | nnrpd 13075 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(!‘(⌊‘𝐴))
∈ ℝ+) | 
| 7 |  | relogcl 26617 | . . . . . . . 8
⊢
((!‘(⌊‘𝐴)) ∈ ℝ+ →
(log‘(!‘(⌊‘𝐴))) ∈ ℝ) | 
| 8 | 6, 7 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘(!‘(⌊‘𝐴))) ∈ ℝ) | 
| 9 |  | rpre 13043 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) | 
| 10 | 9 | adantr 480 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ) | 
| 11 |  | relogcl 26617 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) | 
| 12 | 11 | adantr 480 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘𝐴) ∈
ℝ) | 
| 13 |  | peano2rem 11576 | . . . . . . . . 9
⊢
((log‘𝐴)
∈ ℝ → ((log‘𝐴) − 1) ∈
ℝ) | 
| 14 | 12, 13 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘𝐴) − 1)
∈ ℝ) | 
| 15 | 10, 14 | remulcld 11291 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(𝐴 ·
((log‘𝐴) − 1))
∈ ℝ) | 
| 16 | 8, 15 | resubcld 11691 | . . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈
ℝ) | 
| 17 | 16 | recnd 11289 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈
ℂ) | 
| 18 | 17 | abscld 15475 | . . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈
ℝ) | 
| 19 |  | peano2rem 11576 | . . . 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 11213 | . . . . 5
⊢ 1 ∈
ℂ | 
| 22 |  | subcl 11507 | . . . . 5
⊢
((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈
ℂ) → (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈
ℂ) | 
| 23 | 17, 21, 22 | sylancl 586 | . . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈
ℂ) | 
| 24 | 23 | abscld 15475 | . . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ∈
ℝ) | 
| 25 |  | abs1 15336 | . . . . 5
⊢
(abs‘1) = 1 | 
| 26 | 25 | oveq2i 7442 | . . . 4
⊢
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) =
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) | 
| 27 |  | abs2dif 15371 | . . . . 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 5179 | . . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) | 
| 30 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (⌊‘𝑥) = (⌊‘𝐴)) | 
| 31 | 30 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (1...(⌊‘𝑥)) = (1...(⌊‘𝐴))) | 
| 32 | 31 | sumeq1d 15736 | . . . . . . . . . 10
⊢ (𝑥 = 𝐴 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) | 
| 33 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | 
| 34 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴)) | 
| 35 | 34 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((log‘𝑥) − 1) = ((log‘𝐴) − 1)) | 
| 36 | 33, 35 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 · ((log‘𝑥) − 1)) = (𝐴 · ((log‘𝐴) − 1))) | 
| 37 | 32, 36 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑥 = 𝐴 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) | 
| 38 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) | 
| 39 |  | ovex 7464 | . . . . . . . . 9
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) ∈ V | 
| 40 | 37, 38, 39 | fvmpt3i 7021 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) | 
| 41 | 40 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) | 
| 42 |  | logfac 26643 | . . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) | 
| 43 | 4, 42 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) | 
| 44 | 43 | oveq1d 7446 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1)))) | 
| 45 | 41, 44 | eqtr4d 2780 | . . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) =
((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) | 
| 46 |  | 1rp 13038 | . . . . . . 7
⊢ 1 ∈
ℝ+ | 
| 47 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (⌊‘𝑥) =
(⌊‘1)) | 
| 48 |  | 1z 12647 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ | 
| 49 |  | flid 13848 | . . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → (⌊‘1) = 1) | 
| 50 | 48, 49 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
(⌊‘1) = 1 | 
| 51 | 47, 50 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (⌊‘𝑥) = 1) | 
| 52 | 51 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 →
(1...(⌊‘𝑥)) =
(1...1)) | 
| 53 | 52 | sumeq1d 15736 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...1)(log‘𝑛)) | 
| 54 |  | 0cn 11253 | . . . . . . . . . . . 12
⊢ 0 ∈
ℂ | 
| 55 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (log‘𝑛) =
(log‘1)) | 
| 56 |  | log1 26627 | . . . . . . . . . . . . . 14
⊢
(log‘1) = 0 | 
| 57 | 55, 56 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (log‘𝑛) = 0) | 
| 58 | 57 | fsum1 15783 | . . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ 0 ∈ ℂ) → Σ𝑛 ∈ (1...1)(log‘𝑛) = 0) | 
| 59 | 48, 54, 58 | mp2an 692 | . . . . . . . . . . 11
⊢
Σ𝑛 ∈
(1...1)(log‘𝑛) =
0 | 
| 60 | 53, 59 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝑥 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) = 0) | 
| 61 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → 𝑥 = 1) | 
| 62 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (log‘𝑥) =
(log‘1)) | 
| 63 | 62, 56 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (log‘𝑥) = 0) | 
| 64 | 63 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((log‘𝑥) − 1) = (0 −
1)) | 
| 65 | 61, 64 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (1 · (0 −
1))) | 
| 66 | 54, 21 | subcli 11585 | . . . . . . . . . . . 12
⊢ (0
− 1) ∈ ℂ | 
| 67 | 66 | mullidi 11266 | . . . . . . . . . . 11
⊢ (1
· (0 − 1)) = (0 − 1) | 
| 68 | 65, 67 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (0 −
1)) | 
| 69 | 60, 68 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑥 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (0 − (0 −
1))) | 
| 70 |  | nncan 11538 | . . . . . . . . . 10
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → (0 − (0 − 1)) =
1) | 
| 71 | 54, 21, 70 | mp2an 692 | . . . . . . . . 9
⊢ (0
− (0 − 1)) = 1 | 
| 72 | 69, 71 | eqtrdi 2793 | . . . . . . . 8
⊢ (𝑥 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = 1) | 
| 73 | 72, 38, 39 | fvmpt3i 7021 | . . . . . . 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 7449 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1)) =
(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) | 
| 76 | 75 | fveq2d 6910 | . . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) =
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))) | 
| 77 |  | ioorp 13465 | . . . . . 6
⊢
(0(,)+∞) = ℝ+ | 
| 78 | 77 | eqcomi 2746 | . . . . 5
⊢
ℝ+ = (0(,)+∞) | 
| 79 |  | nnuz 12921 | . . . . 5
⊢ ℕ =
(ℤ≥‘1) | 
| 80 | 48 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℤ) | 
| 81 |  | 1re 11261 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 82 | 81 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℝ) | 
| 83 |  | pnfxr 11315 | . . . . . 6
⊢ +∞
∈ ℝ* | 
| 84 | 83 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
+∞ ∈ ℝ*) | 
| 85 |  | 1nn0 12542 | . . . . . . 7
⊢ 1 ∈
ℕ0 | 
| 86 | 81, 85 | nn0addge1i 12574 | . . . . . 6
⊢ 1 ≤ (1
+ 1) | 
| 87 | 86 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ (1 + 1)) | 
| 88 |  | 0red 11264 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 0
∈ ℝ) | 
| 89 |  | rpre 13043 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) | 
| 90 | 89 | adantl 481 | . . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ 𝑥 ∈
ℝ) | 
| 91 |  | relogcl 26617 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) | 
| 92 | 91 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) | 
| 93 |  | peano2rem 11576 | . . . . . . 7
⊢
((log‘𝑥)
∈ ℝ → ((log‘𝑥) − 1) ∈ ℝ) | 
| 94 | 92, 93 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ ((log‘𝑥)
− 1) ∈ ℝ) | 
| 95 | 90, 94 | remulcld 11291 | . . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+)
→ (𝑥 ·
((log‘𝑥) − 1))
∈ ℝ) | 
| 96 |  | nnrp 13046 | . . . . . 6
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) | 
| 97 | 96, 92 | sylan2 593 | . . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℕ) →
(log‘𝑥) ∈
ℝ) | 
| 98 |  | advlog 26696 | . . . . . 6
⊢ (ℝ
D (𝑥 ∈
ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) | 
| 99 | 98 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(ℝ D (𝑥 ∈
ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) | 
| 100 |  | fveq2 6906 | . . . . 5
⊢ (𝑥 = 𝑛 → (log‘𝑥) = (log‘𝑛)) | 
| 101 |  | simp32 1211 | . . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → 𝑥 ≤ 𝑛) | 
| 102 |  | logleb 26645 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛))) | 
| 103 | 102 | 3ad2ant2 1135 | . . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛))) | 
| 104 | 101, 103 | mpbid 232 | . . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 𝑛
∈ ℝ+) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (log‘𝑥) ≤ (log‘𝑛)) | 
| 105 |  | simprr 773 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) | 
| 106 |  | simprl 771 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) | 
| 107 |  | logleb 26645 | . . . . . . . 8
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) | 
| 108 | 46, 106, 107 | sylancr 587 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥))) | 
| 109 | 105, 108 | mpbid 232 | . . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥)) | 
| 110 | 56, 109 | eqbrtrrid 5179 | . . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) ∧
(𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥)) | 
| 111 | 46 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
∈ ℝ+) | 
| 112 |  | 1le1 11891 | . . . . . 6
⊢ 1 ≤
1 | 
| 113 | 112 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ 1) | 
| 114 |  | simpr 484 | . . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) → 1
≤ 𝐴) | 
| 115 | 10 | rexrd 11311 | . . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
𝐴 ∈
ℝ*) | 
| 116 |  | pnfge 13172 | . . . . . 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 26075 | . . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) ≤
(log‘𝐴)) | 
| 119 | 76, 118 | eqbrtrrd 5167 | . . 3
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ≤
(log‘𝐴)) | 
| 120 | 20, 24, 12, 29, 119 | letrd 11418 | . 2
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(log‘𝐴)) | 
| 121 | 18, 82, 12 | lesubaddd 11860 | . 2
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤
(log‘𝐴) ↔
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))) | 
| 122 | 120, 121 | mpbid 232 | 1
⊢ ((𝐴 ∈ ℝ+
∧ 1 ≤ 𝐴) →
(abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1)) |