| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzfid 14015 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) | 
| 2 |  | elfznn 13594 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℕ) | 
| 3 | 2 | adantl 481 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ) | 
| 4 | 3 | nnrpd 13076 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℝ+) | 
| 5 | 4 | relogcld 26666 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (log‘𝑘) ∈
ℝ) | 
| 6 | 5, 3 | nndivred 12321 | . . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘𝑘) / 𝑘) ∈ ℝ) | 
| 7 | 1, 6 | fsumrecl 15771 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) ∈ ℝ) | 
| 8 | 7 | recnd 11290 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) ∈ ℂ) | 
| 9 |  | elioore 13418 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) | 
| 10 | 9 | adantl 481 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) | 
| 11 |  | 1rp 13039 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ | 
| 12 | 11 | a1i 11 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) | 
| 13 |  | 1red 11263 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) | 
| 14 |  | eliooord 13447 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) | 
| 15 | 14 | adantl 481 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) | 
| 16 | 15 | simpld 494 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) | 
| 17 | 13, 10, 16 | ltled 11410 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) | 
| 18 | 10, 12, 17 | rpgecld 13117 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) | 
| 19 | 18 | relogcld 26666 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) | 
| 20 | 19 | resqcld 14166 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥)↑2) ∈ ℝ) | 
| 21 | 20 | rehalfcld 12515 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥)↑2) / 2) ∈
ℝ) | 
| 22 | 21 | recnd 11290 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥)↑2) / 2) ∈
ℂ) | 
| 23 | 19 | recnd 11290 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) | 
| 24 | 10, 16 | rplogcld 26672 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) | 
| 25 | 24 | rpne0d 13083 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) | 
| 26 | 8, 22, 23, 25 | divsubdird 12083 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((((log‘𝑥)↑2) / 2) / (log‘𝑥)))) | 
| 27 | 7, 21 | resubcld 11692 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) ∈
ℝ) | 
| 28 | 27 | recnd 11290 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) ∈
ℂ) | 
| 29 | 28, 23, 25 | divrecd 12047 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 /
(log‘𝑥)))) | 
| 30 | 20 | recnd 11290 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥)↑2) ∈ ℂ) | 
| 31 |  | 2cnd 12345 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℂ) | 
| 32 |  | 2ne0 12371 | . . . . . . . . . 10
⊢ 2 ≠
0 | 
| 33 | 32 | a1i 11 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ≠ 0) | 
| 34 | 30, 31, 23, 33, 25 | divdiv32d 12069 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / 2) / (log‘𝑥)) = ((((log‘𝑥)↑2) / (log‘𝑥)) / 2)) | 
| 35 | 23 | sqvald 14184 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥)↑2) = ((log‘𝑥) · (log‘𝑥))) | 
| 36 | 35 | oveq1d 7447 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥)↑2) / (log‘𝑥)) = (((log‘𝑥) · (log‘𝑥)) / (log‘𝑥))) | 
| 37 | 23, 23, 25 | divcan3d 12049 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥) · (log‘𝑥)) / (log‘𝑥)) = (log‘𝑥)) | 
| 38 | 36, 37 | eqtrd 2776 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥)↑2) / (log‘𝑥)) = (log‘𝑥)) | 
| 39 | 38 | oveq1d 7447 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / (log‘𝑥)) / 2) = ((log‘𝑥) / 2)) | 
| 40 | 34, 39 | eqtrd 2776 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / 2) / (log‘𝑥)) = ((log‘𝑥) / 2)) | 
| 41 | 40 | oveq2d 7448 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((((log‘𝑥)↑2) / 2) / (log‘𝑥))) = ((Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) | 
| 42 | 26, 29, 41 | 3eqtr3rd 2785 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 /
(log‘𝑥)))) | 
| 43 | 42 | mpteq2dva 5241 | . . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 /
(log‘𝑥))))) | 
| 44 | 24 | rprecred 13089 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ) | 
| 45 | 18 | ex 412 | . . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) → 𝑥
∈ ℝ+)) | 
| 46 | 45 | ssrdv 3988 | . . . . . 6
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ+) | 
| 47 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) | 
| 48 | 47 | logdivsum 27578 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) /
2))):ℝ+⟶ℝ ∧ (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom
⇝𝑟 ∧ (((𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ⇝𝑟
1 ∧ 1 ∈ ℝ+ ∧ e ≤ 1) → (abs‘(((𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)))‘1) − 1)) ≤
((log‘1) / 1))) | 
| 49 | 48 | simp2i 1140 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom
⇝𝑟 | 
| 50 |  | rlimdmo1 15655 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom
⇝𝑟 → (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈
𝑂(1)) | 
| 51 | 49, 50 | mp1i 13 | . . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈
𝑂(1)) | 
| 52 | 46, 51 | o1res2 15600 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈
𝑂(1)) | 
| 53 |  | divlogrlim 26678 | . . . . . 6
⊢ (𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 | 
| 54 |  | rlimo1 15654 | . . . . . 6
⊢ ((𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) | 
| 55 | 53, 54 | mp1i 13 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1)) | 
| 56 | 27, 44, 52, 55 | o1mul2 15662 | . . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 /
(log‘𝑥)))) ∈
𝑂(1)) | 
| 57 | 43, 56 | eqeltrd 2840 | . . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1)) | 
| 58 | 8, 23, 25 | divcld 12044 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) ∈ ℂ) | 
| 59 | 23 | halfcld 12513 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ) | 
| 60 | 58, 59 | subcld 11621 | . . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ) | 
| 61 |  | elfznn 13594 | . . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) | 
| 62 | 61 | adantl 481 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) | 
| 63 |  | vmacl 27162 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) | 
| 64 | 62, 63 | syl 17 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) | 
| 65 | 64, 62 | nndivred 12321 | . . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) | 
| 66 | 18 | adantr 480 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) | 
| 67 | 62 | nnrpd 13076 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) | 
| 68 | 66, 67 | rpdivcld 13095 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) | 
| 69 | 68 | relogcld 26666 | . . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) | 
| 70 | 65, 69 | remulcld 11292 | . . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) | 
| 71 | 1, 70 | fsumrecl 15771 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ) | 
| 72 | 71 | recnd 11290 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ) | 
| 73 | 24 | rpcnd 13080 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) | 
| 74 | 72, 73, 25 | divcld 12044 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ) | 
| 75 | 73 | halfcld 12513 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ) | 
| 76 | 74, 75 | subcld 11621 | . . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ) | 
| 77 | 58, 74, 59 | nnncan2d 11656 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))) | 
| 78 | 8, 72, 23, 25 | divsubdird 12083 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))) | 
| 79 |  | fzfid 14015 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑥 /
𝑛))) ∈
Fin) | 
| 80 | 64 | adantr 480 | . . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑛) ∈
ℝ) | 
| 81 | 62 | adantr 480 | . . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℕ) | 
| 82 |  | elfznn 13594 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) | 
| 83 | 82 | adantl 481 | . . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ) | 
| 84 | 81, 83 | nnmulcld 12320 | . . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑛 · 𝑚) ∈ ℕ) | 
| 85 | 80, 84 | nndivred 12321 | . . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℝ) | 
| 86 | 79, 85 | fsumrecl 15771 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℝ) | 
| 87 | 86 | recnd 11290 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℂ) | 
| 88 | 70 | recnd 11290 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℂ) | 
| 89 | 1, 87, 88 | fsumsub 15825 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) | 
| 90 | 64 | recnd 11290 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℂ) | 
| 91 | 62 | nncnd 12283 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) | 
| 92 | 62 | nnne0d 12317 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0) | 
| 93 | 90, 91, 92 | divcld 12044 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) | 
| 94 | 83 | nnrecred 12318 | . . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 / 𝑚) ∈ ℝ) | 
| 95 | 79, 94 | fsumrecl 15771 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) ∈ ℝ) | 
| 96 | 95 | recnd 11290 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) ∈ ℂ) | 
| 97 | 69 | recnd 11290 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ) | 
| 98 | 93, 96, 97 | subdid 11720 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) | 
| 99 | 90 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑛) ∈
ℂ) | 
| 100 | 91 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℂ) | 
| 101 | 83 | nncnd 12283 | . . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ) | 
| 102 | 92 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ≠ 0) | 
| 103 | 83 | nnne0d 12317 | . . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≠ 0) | 
| 104 | 99, 100, 101, 102, 103 | divdiv1d 12075 | . . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑛) / 𝑛) / 𝑚) = ((Λ‘𝑛) / (𝑛 · 𝑚))) | 
| 105 | 99, 100, 102 | divcld 12044 | . . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ) | 
| 106 | 105, 101,
103 | divrecd 12047 | . . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑛) / 𝑛) / 𝑚) = (((Λ‘𝑛) / 𝑛) · (1 / 𝑚))) | 
| 107 | 104, 106 | eqtr3d 2778 | . . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / (𝑛 · 𝑚)) = (((Λ‘𝑛) / 𝑛) · (1 / 𝑚))) | 
| 108 | 107 | sumeq2dv 15739 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑛) / 𝑛) · (1 / 𝑚))) | 
| 109 | 101, 103 | reccld 12037 | . . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 / 𝑚) ∈ ℂ) | 
| 110 | 79, 93, 109 | fsummulc2 15821 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑛) / 𝑛) · (1 / 𝑚))) | 
| 111 | 108, 110 | eqtr4d 2779 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) = (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚))) | 
| 112 | 111 | oveq1d 7447 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) | 
| 113 | 98, 112 | eqtr4d 2779 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) | 
| 114 | 113 | sumeq2dv 15739 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) | 
| 115 |  | vmasum 27261 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ →
Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) = (log‘𝑘)) | 
| 116 | 3, 115 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) = (log‘𝑘)) | 
| 117 | 116 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) / 𝑘) = ((log‘𝑘) / 𝑘)) | 
| 118 |  | fzfid 14015 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (1...𝑘) ∈ Fin) | 
| 119 |  | dvdsssfz1 16356 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) | 
| 120 | 3, 119 | syl 17 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) | 
| 121 | 118, 120 | ssfid 9302 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ∈ Fin) | 
| 122 | 3 | nncnd 12283 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℂ) | 
| 123 |  | ssrab2 4079 | . . . . . . . . . . . . . . . . . 18
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ | 
| 124 |  | simprr 772 | . . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) | 
| 125 | 123, 124 | sselid 3980 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ) | 
| 126 | 125, 63 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (Λ‘𝑛) ∈ ℝ) | 
| 127 | 126 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (Λ‘𝑛) ∈ ℂ) | 
| 128 | 127 | anassrs 467 | . . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘𝑛) ∈ ℂ) | 
| 129 | 3 | nnne0d 12317 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ≠ 0) | 
| 130 | 121, 122,
128, 129 | fsumdivc 15823 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) / 𝑘) = Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘)) | 
| 131 | 117, 130 | eqtr3d 2778 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘𝑘) / 𝑘) = Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘)) | 
| 132 | 131 | sumeq2dv 15739 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘)) | 
| 133 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 · 𝑚) → ((Λ‘𝑛) / 𝑘) = ((Λ‘𝑛) / (𝑛 · 𝑚))) | 
| 134 | 2 | ad2antrl 728 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℕ) | 
| 135 | 134 | nncnd 12283 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℂ) | 
| 136 | 134 | nnne0d 12317 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ≠ 0) | 
| 137 | 127, 135,
136 | divcld 12044 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((Λ‘𝑛) / 𝑘) ∈ ℂ) | 
| 138 | 133, 10, 137 | dvdsflsumcom 27232 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚))) | 
| 139 | 132, 138 | eqtrd 2776 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚))) | 
| 140 | 139 | oveq1d 7447 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) | 
| 141 | 89, 114, 140 | 3eqtr4rd 2787 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) | 
| 142 | 141 | oveq1d 7447 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) | 
| 143 | 77, 78, 142 | 3eqtr2d 2782 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) | 
| 144 | 143 | mpteq2dva 5241 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) = (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)))) | 
| 145 |  | 1red 11263 | . . . . . . 7
⊢ (⊤
→ 1 ∈ ℝ) | 
| 146 | 1, 65 | fsumrecl 15771 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ) | 
| 147 | 146, 24 | rerpdivcld 13109 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℝ) | 
| 148 |  | ioossre 13449 | . . . . . . . . . . 11
⊢
(1(,)+∞) ⊆ ℝ | 
| 149 |  | ax-1cn 11214 | . . . . . . . . . . 11
⊢ 1 ∈
ℂ | 
| 150 |  | o1const 15657 | . . . . . . . . . . 11
⊢
(((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1)) | 
| 151 | 148, 149,
150 | mp2an 692 | . . . . . . . . . 10
⊢ (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1) | 
| 152 | 151 | a1i 11 | . . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ 1) ∈ 𝑂(1)) | 
| 153 | 147 | recnd 11290 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℂ) | 
| 154 | 12 | rpcnd 13080 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℂ) | 
| 155 | 146 | recnd 11290 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) | 
| 156 | 155, 23, 23, 25 | divsubdird 12083 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥)))) | 
| 157 | 155, 23 | subcld 11621 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) | 
| 158 | 157, 23, 25 | divrecd 12047 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) | 
| 159 | 23, 25 | dividd 12042 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥) / (log‘𝑥)) = 1) | 
| 160 | 159 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) | 
| 161 | 156, 158,
160 | 3eqtr3rd 2785 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) | 
| 162 | 161 | mpteq2dva 5241 | . . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))))) | 
| 163 | 146, 19 | resubcld 11692 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ) | 
| 164 |  | vmadivsum 27527 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) | 
| 165 | 164 | a1i 11 | . . . . . . . . . . . . 13
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) | 
| 166 | 46, 165 | o1res2 15600 | . . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) | 
| 167 | 163, 44, 166, 55 | o1mul2 15662 | . . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) ∈
𝑂(1)) | 
| 168 | 162, 167 | eqeltrd 2840 | . . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) ∈
𝑂(1)) | 
| 169 | 153, 154,
168 | o1dif 15667 | . . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1))) | 
| 170 | 152, 169 | mpbird 257 | . . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1)) | 
| 171 | 147, 170 | o1lo1d 15576 | . . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ ≤𝑂(1)) | 
| 172 | 95, 69 | resubcld 11692 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℝ) | 
| 173 | 65, 172 | remulcld 11292 | . . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ) | 
| 174 | 1, 173 | fsumrecl 15771 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ) | 
| 175 | 174, 24 | rerpdivcld 13109 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ∈ ℝ) | 
| 176 |  | 1red 11263 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) | 
| 177 |  | vmage0 27165 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) | 
| 178 | 62, 177 | syl 17 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(Λ‘𝑛)) | 
| 179 | 64, 67, 178 | divge0d 13118 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
((Λ‘𝑛) / 𝑛)) | 
| 180 | 68 | rpred 13078 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ) | 
| 181 | 91 | mullidd 11280 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛) | 
| 182 |  | fznnfl 13903 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) | 
| 183 | 10, 182 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥))) | 
| 184 | 183 | simplbda 499 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥) | 
| 185 | 181, 184 | eqbrtrd 5164 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥) | 
| 186 | 10 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ) | 
| 187 | 176, 186,
67 | lemuldivd 13127 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) | 
| 188 | 185, 187 | mpbid 232 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛)) | 
| 189 |  | harmonicubnd 27054 | . . . . . . . . . . . . . 14
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1)) | 
| 190 | 180, 188,
189 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1)) | 
| 191 | 95, 69, 176 | lesubadd2d 11863 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ≤ 1 ↔ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1))) | 
| 192 | 190, 191 | mpbird 257 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ≤ 1) | 
| 193 | 172, 176,
65, 179, 192 | lemul2ad 12209 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ (((Λ‘𝑛) / 𝑛) · 1)) | 
| 194 | 93 | mulridd 11279 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · 1) =
((Λ‘𝑛) / 𝑛)) | 
| 195 | 193, 194 | breqtrd 5168 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ ((Λ‘𝑛) / 𝑛)) | 
| 196 | 1, 173, 65, 195 | fsumle 15836 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) | 
| 197 | 174, 146,
24, 196 | lediv1dd 13136 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) | 
| 198 | 197 | adantrr 717 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) | 
| 199 | 145, 171,
147, 175, 198 | lo1le 15689 | . . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ ≤𝑂(1)) | 
| 200 |  | 0red 11265 | . . . . . . 7
⊢ (⊤
→ 0 ∈ ℝ) | 
| 201 |  | harmoniclbnd 27053 | . . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ+ →
(log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚)) | 
| 202 | 68, 201 | syl 17 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) | 
| 203 | 95, 69 | subge0d 11854 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 ≤ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ↔ (log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚))) | 
| 204 | 202, 203 | mpbird 257 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) | 
| 205 | 65, 172, 179, 204 | mulge0d 11841 | . . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) | 
| 206 | 1, 173, 205 | fsumge0 15832 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) | 
| 207 | 174, 24, 206 | divge0d 13118 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) | 
| 208 | 175, 200,
207 | o1lo12 15575 | . . . . . 6
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈
≤𝑂(1))) | 
| 209 | 199, 208 | mpbird 257 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1)) | 
| 210 | 144, 209 | eqeltrd 2840 | . . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈
𝑂(1)) | 
| 211 | 60, 76, 210 | o1dif 15667 | . . 3
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1))) | 
| 212 | 57, 211 | mpbid 232 | . 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1)) | 
| 213 | 212 | mptru 1546 | 1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) |