Proof of Theorem logfacrlim
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1red 11262 | . . 3
⊢ (⊤
→ 1 ∈ ℝ) | 
| 2 |  | 1cnd 11256 | . . 3
⊢ (⊤
→ 1 ∈ ℂ) | 
| 3 |  | relogcl 26617 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) | 
| 4 | 3 | adantl 481 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℝ) | 
| 5 | 4 | recnd 11289 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℂ) | 
| 6 |  | 1cnd 11256 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 1 ∈ ℂ) | 
| 7 |  | rpcnne0 13053 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) | 
| 8 | 7 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) | 
| 9 |  | divdir 11947 | . . . . . . 7
⊢
(((log‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘𝑥) + 1) / 𝑥) = (((log‘𝑥) / 𝑥) + (1 / 𝑥))) | 
| 10 | 5, 6, 8, 9 | syl3anc 1373 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((log‘𝑥) + 1) / 𝑥) = (((log‘𝑥) / 𝑥) + (1 / 𝑥))) | 
| 11 | 10 | mpteq2dva 5242 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(((log‘𝑥) / 𝑥) + (1 / 𝑥)))) | 
| 12 |  | simpr 484 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ+) | 
| 13 | 4, 12 | rerpdivcld 13108 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘𝑥) / 𝑥) ∈ ℝ) | 
| 14 |  | rpreccl 13061 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) | 
| 15 | 14 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈
ℝ+) | 
| 16 | 15 | rpred 13077 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈ ℝ) | 
| 17 | 8 | simpld 494 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℂ) | 
| 18 | 17 | cxp1d 26748 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥↑𝑐1) = 𝑥) | 
| 19 | 18 | oveq2d 7447 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘𝑥) / (𝑥↑𝑐1)) =
((log‘𝑥) / 𝑥)) | 
| 20 | 19 | mpteq2dva 5242 | . . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘𝑥) / (𝑥↑𝑐1))) = (𝑥 ∈ ℝ+
↦ ((log‘𝑥) /
𝑥))) | 
| 21 |  | 1rp 13038 | . . . . . . . 8
⊢ 1 ∈
ℝ+ | 
| 22 |  | cxploglim 27021 | . . . . . . . 8
⊢ (1 ∈
ℝ+ → (𝑥 ∈ ℝ+ ↦
((log‘𝑥) / (𝑥↑𝑐1)))
⇝𝑟 0) | 
| 23 | 21, 22 | mp1i 13 | . . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘𝑥) / (𝑥↑𝑐1)))
⇝𝑟 0) | 
| 24 | 20, 23 | eqbrtrrd 5167 | . . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘𝑥) / 𝑥)) ⇝𝑟
0) | 
| 25 |  | ax-1cn 11213 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 26 |  | divrcnv 15888 | . . . . . . 7
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) | 
| 27 | 25, 26 | mp1i 13 | . . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) | 
| 28 | 13, 16, 24, 27 | rlimadd 15679 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥) / 𝑥) + (1 / 𝑥))) ⇝𝑟 (0 +
0)) | 
| 29 | 11, 28 | eqbrtrd 5165 | . . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥) + 1) / 𝑥)) ⇝𝑟 (0 +
0)) | 
| 30 |  | 00id 11436 | . . . 4
⊢ (0 + 0) =
0 | 
| 31 | 29, 30 | breqtrdi 5184 | . . 3
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥) + 1) / 𝑥)) ⇝𝑟
0) | 
| 32 |  | peano2re 11434 | . . . . . 6
⊢
((log‘𝑥)
∈ ℝ → ((log‘𝑥) + 1) ∈ ℝ) | 
| 33 | 4, 32 | syl 17 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘𝑥) + 1) ∈ ℝ) | 
| 34 | 33, 12 | rerpdivcld 13108 | . . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((log‘𝑥) + 1) / 𝑥) ∈ ℝ) | 
| 35 | 34 | recnd 11289 | . . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((log‘𝑥) + 1) / 𝑥) ∈ ℂ) | 
| 36 |  | rprege0 13050 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) | 
| 37 | 36 | adantl 481 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) | 
| 38 |  | flge0nn0 13860 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) | 
| 39 |  | faccl 14322 | . . . . . . . . 9
⊢
((⌊‘𝑥)
∈ ℕ0 → (!‘(⌊‘𝑥)) ∈ ℕ) | 
| 40 | 37, 38, 39 | 3syl 18 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (!‘(⌊‘𝑥)) ∈ ℕ) | 
| 41 | 40 | nnrpd 13075 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (!‘(⌊‘𝑥)) ∈
ℝ+) | 
| 42 |  | relogcl 26617 | . . . . . . 7
⊢
((!‘(⌊‘𝑥)) ∈ ℝ+ →
(log‘(!‘(⌊‘𝑥))) ∈ ℝ) | 
| 43 | 41, 42 | syl 17 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘(!‘(⌊‘𝑥))) ∈
ℝ) | 
| 44 | 43, 12 | rerpdivcld 13108 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℝ) | 
| 45 | 44 | recnd 11289 | . . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℂ) | 
| 46 | 5, 45 | subcld 11620 | . . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ ℂ) | 
| 47 |  | logfacbnd3 27267 | . . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) ≤ ((log‘𝑥) + 1)) | 
| 48 | 47 | adantl 481 | . . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) →
(abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) ≤ ((log‘𝑥) + 1)) | 
| 49 | 43 | recnd 11289 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘(!‘(⌊‘𝑥))) ∈
ℂ) | 
| 50 | 49 | adantrr 717 | . . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) →
(log‘(!‘(⌊‘𝑥))) ∈ ℂ) | 
| 51 | 7 | ad2antrl 728 | . . . . . . . . . 10
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) | 
| 52 | 51 | simpld 494 | . . . . . . . . 9
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ) | 
| 53 | 5 | adantrr 717 | . . . . . . . . . 10
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ) | 
| 54 |  | subcl 11507 | . . . . . . . . . 10
⊢
(((log‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ) → ((log‘𝑥) − 1) ∈ ℂ) | 
| 55 | 53, 25, 54 | sylancl 586 | . . . . . . . . 9
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) − 1) ∈ ℂ) | 
| 56 | 52, 55 | mulcld 11281 | . . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · ((log‘𝑥) − 1)) ∈
ℂ) | 
| 57 | 50, 56 | subcld 11620 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) →
((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1))) ∈
ℂ) | 
| 58 | 57 | abscld 15475 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) →
(abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) ∈
ℝ) | 
| 59 | 4 | adantrr 717 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ) | 
| 60 | 59, 32 | syl 17 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) + 1) ∈ ℝ) | 
| 61 |  | rpregt0 13049 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) | 
| 62 | 61 | ad2antrl 728 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 < 𝑥)) | 
| 63 |  | lediv1 12133 | . . . . . 6
⊢
(((abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) ∈ ℝ ∧
((log‘𝑥) + 1) ∈
ℝ ∧ (𝑥 ∈
ℝ ∧ 0 < 𝑥))
→ ((abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) ≤ ((log‘𝑥) + 1) ↔
((abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) / 𝑥) ≤ (((log‘𝑥) + 1) / 𝑥))) | 
| 64 | 58, 60, 62, 63 | syl3anc 1373 | . . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) →
((abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) ≤ ((log‘𝑥) + 1) ↔
((abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) / 𝑥) ≤ (((log‘𝑥) + 1) / 𝑥))) | 
| 65 | 48, 64 | mpbid 232 | . . . 4
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) →
((abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) / 𝑥) ≤ (((log‘𝑥) + 1) / 𝑥)) | 
| 66 | 51 | simprd 495 | . . . . . . . . 9
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0) | 
| 67 | 55, 52, 66 | divcan3d 12048 | . . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑥 · ((log‘𝑥) − 1)) / 𝑥) = ((log‘𝑥) − 1)) | 
| 68 | 67 | oveq1d 7446 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑥 · ((log‘𝑥) − 1)) / 𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) = (((log‘𝑥) − 1) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) | 
| 69 |  | divsubdir 11961 | . . . . . . . 8
⊢ (((𝑥 · ((log‘𝑥) − 1)) ∈ ℂ
∧ (log‘(!‘(⌊‘𝑥))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) = (((𝑥 · ((log‘𝑥) − 1)) / 𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) | 
| 70 | 56, 50, 51, 69 | syl3anc 1373 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) = (((𝑥 · ((log‘𝑥) − 1)) / 𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) | 
| 71 | 45 | adantrr 717 | . . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) →
((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℂ) | 
| 72 |  | 1cnd 11256 | . . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ) | 
| 73 | 53, 71, 72 | sub32d 11652 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − 1) = (((log‘𝑥) − 1) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) | 
| 74 | 68, 70, 73 | 3eqtr4rd 2788 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − 1) = (((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥)) | 
| 75 | 74 | fveq2d 6910 | . . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − 1)) = (abs‘(((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥))) | 
| 76 | 56, 50 | subcld 11620 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥)))) ∈ ℂ) | 
| 77 | 76, 52, 66 | absdivd 15494 | . . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥)) = ((abs‘((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥))))) / (abs‘𝑥))) | 
| 78 | 56, 50 | abssubd 15492 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥))))) =
(abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1))))) | 
| 79 | 36 | ad2antrl 728 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) | 
| 80 |  | absid 15335 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) | 
| 81 | 79, 80 | syl 17 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥) | 
| 82 | 78, 81 | oveq12d 7449 | . . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘((𝑥 · ((log‘𝑥) − 1)) −
(log‘(!‘(⌊‘𝑥))))) / (abs‘𝑥)) =
((abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) / 𝑥)) | 
| 83 | 75, 77, 82 | 3eqtrd 2781 | . . . 4
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − 1)) =
((abs‘((log‘(!‘(⌊‘𝑥))) − (𝑥 · ((log‘𝑥) − 1)))) / 𝑥)) | 
| 84 | 35 | adantrr 717 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥) + 1) / 𝑥) ∈ ℂ) | 
| 85 | 84 | subid1d 11609 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥) + 1) / 𝑥) − 0) = (((log‘𝑥) + 1) / 𝑥)) | 
| 86 | 85 | fveq2d 6910 | . . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥) + 1) / 𝑥) − 0)) = (abs‘(((log‘𝑥) + 1) / 𝑥))) | 
| 87 |  | log1 26627 | . . . . . . . . 9
⊢
(log‘1) = 0 | 
| 88 |  | simprr 773 | . . . . . . . . . 10
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) | 
| 89 | 12 | adantrr 717 | . . . . . . . . . . 11
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) | 
| 90 |  | logleb 26645 | . . . . . . . . . . 11
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) | 
| 91 | 21, 89, 90 | sylancr 587 | . . . . . . . . . 10
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥))) | 
| 92 | 88, 91 | mpbid 232 | . . . . . . . . 9
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥)) | 
| 93 | 87, 92 | eqbrtrrid 5179 | . . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥)) | 
| 94 | 59, 93 | ge0p1rpd 13107 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥) + 1) ∈
ℝ+) | 
| 95 | 94, 89 | rpdivcld 13094 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥) + 1) / 𝑥) ∈
ℝ+) | 
| 96 |  | rprege0 13050 | . . . . . 6
⊢
((((log‘𝑥) +
1) / 𝑥) ∈
ℝ+ → ((((log‘𝑥) + 1) / 𝑥) ∈ ℝ ∧ 0 ≤
(((log‘𝑥) + 1) /
𝑥))) | 
| 97 |  | absid 15335 | . . . . . 6
⊢
(((((log‘𝑥) +
1) / 𝑥) ∈ ℝ
∧ 0 ≤ (((log‘𝑥) + 1) / 𝑥)) → (abs‘(((log‘𝑥) + 1) / 𝑥)) = (((log‘𝑥) + 1) / 𝑥)) | 
| 98 | 95, 96, 97 | 3syl 18 | . . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥) + 1) / 𝑥)) = (((log‘𝑥) + 1) / 𝑥)) | 
| 99 | 86, 98 | eqtrd 2777 | . . . 4
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥) + 1) / 𝑥) − 0)) = (((log‘𝑥) + 1) / 𝑥)) | 
| 100 | 65, 83, 99 | 3brtr4d 5175 | . . 3
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − 1)) ≤
(abs‘((((log‘𝑥)
+ 1) / 𝑥) −
0))) | 
| 101 | 1, 2, 31, 35, 46, 100 | rlimsqzlem 15685 | . 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ⇝𝑟
1) | 
| 102 | 101 | mptru 1547 | 1
⊢ (𝑥 ∈ ℝ+
↦ ((log‘𝑥)
− ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ⇝𝑟
1 |