| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzfid 14014 | . . . . . 6
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) | 
| 2 |  | mulog2sumlem1.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 3 |  | elfznn 13593 | . . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘𝐴))
→ 𝑚 ∈
ℕ) | 
| 4 | 3 | nnrpd 13075 | . . . . . . . . 9
⊢ (𝑚 ∈
(1...(⌊‘𝐴))
→ 𝑚 ∈
ℝ+) | 
| 5 |  | rpdivcl 13060 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → (𝐴 / 𝑚) ∈
ℝ+) | 
| 6 | 2, 4, 5 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑚) ∈
ℝ+) | 
| 7 | 6 | relogcld 26665 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (log‘(𝐴 / 𝑚)) ∈ ℝ) | 
| 8 | 3 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → 𝑚 ∈ ℕ) | 
| 9 | 7, 8 | nndivred 12320 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → ((log‘(𝐴 / 𝑚)) / 𝑚) ∈ ℝ) | 
| 10 | 1, 9 | fsumrecl 15770 | . . . . 5
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) ∈ ℝ) | 
| 11 | 2 | relogcld 26665 | . . . . . . . 8
⊢ (𝜑 → (log‘𝐴) ∈
ℝ) | 
| 12 | 11 | resqcld 14165 | . . . . . . 7
⊢ (𝜑 → ((log‘𝐴)↑2) ∈
ℝ) | 
| 13 | 12 | rehalfcld 12513 | . . . . . 6
⊢ (𝜑 → (((log‘𝐴)↑2) / 2) ∈
ℝ) | 
| 14 |  | emre 27049 | . . . . . . . 8
⊢ γ
∈ ℝ | 
| 15 |  | remulcl 11240 | . . . . . . . 8
⊢ ((γ
∈ ℝ ∧ (log‘𝐴) ∈ ℝ) → (γ ·
(log‘𝐴)) ∈
ℝ) | 
| 16 | 14, 11, 15 | sylancr 587 | . . . . . . 7
⊢ (𝜑 → (γ ·
(log‘𝐴)) ∈
ℝ) | 
| 17 |  | rpsup 13906 | . . . . . . . . 9
⊢
sup(ℝ+, ℝ*, < ) =
+∞ | 
| 18 | 17 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → sup(ℝ+,
ℝ*, < ) = +∞) | 
| 19 |  | logdivsum.1 | . . . . . . . . . . . . 13
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦
(Σ𝑖 ∈
(1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2))) | 
| 20 | 19 | logdivsum 27577 | . . . . . . . . . . . 12
⊢ (𝐹:ℝ+⟶ℝ ∧
𝐹 ∈ dom
⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤
𝐴) →
(abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴))) | 
| 21 | 20 | simp1i 1140 | . . . . . . . . . . 11
⊢ 𝐹:ℝ+⟶ℝ | 
| 22 | 21 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℝ+⟶ℝ) | 
| 23 | 22 | feqmptd 6977 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ+ ↦ (𝐹‘𝑥))) | 
| 24 |  | mulog2sumlem.1 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) | 
| 25 | 23, 24 | eqbrtrrd 5167 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝐹‘𝑥)) ⇝𝑟 𝐿) | 
| 26 | 21 | ffvelcdmi 7103 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝐹‘𝑥) ∈
ℝ) | 
| 27 | 26 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐹‘𝑥) ∈ ℝ) | 
| 28 | 18, 25, 27 | rlimrecl 15616 | . . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℝ) | 
| 29 | 16, 28 | resubcld 11691 | . . . . . 6
⊢ (𝜑 → ((γ ·
(log‘𝐴)) −
𝐿) ∈
ℝ) | 
| 30 | 13, 29 | readdcld 11290 | . . . . 5
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) + ((γ
· (log‘𝐴))
− 𝐿)) ∈
ℝ) | 
| 31 | 10, 30 | resubcld 11691 | . . . 4
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ ·
(log‘𝐴)) −
𝐿))) ∈
ℝ) | 
| 32 | 31 | recnd 11289 | . . 3
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ ·
(log‘𝐴)) −
𝐿))) ∈
ℂ) | 
| 33 | 32 | abscld 15475 | . 2
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ ·
(log‘𝐴)) −
𝐿)))) ∈
ℝ) | 
| 34 |  | rerpdivcl 13065 | . . . . . . . 8
⊢
(((log‘𝐴)
∈ ℝ ∧ 𝑚
∈ ℝ+) → ((log‘𝐴) / 𝑚) ∈ ℝ) | 
| 35 | 11, 4, 34 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → ((log‘𝐴) / 𝑚) ∈ ℝ) | 
| 36 | 35 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → ((log‘𝐴) / 𝑚) ∈ ℂ) | 
| 37 | 1, 36 | fsumcl 15769 | . . . . 5
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) ∈ ℂ) | 
| 38 | 11 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) | 
| 39 |  | readdcl 11238 | . . . . . . . 8
⊢
(((log‘𝐴)
∈ ℝ ∧ γ ∈ ℝ) → ((log‘𝐴) + γ) ∈
ℝ) | 
| 40 | 11, 14, 39 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → ((log‘𝐴) + γ) ∈
ℝ) | 
| 41 | 40 | recnd 11289 | . . . . . 6
⊢ (𝜑 → ((log‘𝐴) + γ) ∈
ℂ) | 
| 42 | 38, 41 | mulcld 11281 | . . . . 5
⊢ (𝜑 → ((log‘𝐴) · ((log‘𝐴) + γ)) ∈
ℂ) | 
| 43 | 37, 42 | subcld 11620 | . . . 4
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ))) ∈
ℂ) | 
| 44 | 43 | abscld 15475 | . . 3
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) ∈
ℝ) | 
| 45 | 8 | nnrpd 13075 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → 𝑚 ∈ ℝ+) | 
| 46 | 45 | relogcld 26665 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (log‘𝑚) ∈ ℝ) | 
| 47 | 46, 8 | nndivred 12320 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → ((log‘𝑚) / 𝑚) ∈ ℝ) | 
| 48 | 47 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → ((log‘𝑚) / 𝑚) ∈ ℂ) | 
| 49 | 1, 48 | fsumcl 15769 | . . . . 5
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) ∈ ℂ) | 
| 50 | 13 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (((log‘𝐴)↑2) / 2) ∈
ℂ) | 
| 51 | 28 | recnd 11289 | . . . . . 6
⊢ (𝜑 → 𝐿 ∈ ℂ) | 
| 52 | 50, 51 | addcld 11280 | . . . . 5
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) + 𝐿) ∈
ℂ) | 
| 53 | 49, 52 | subcld 11620 | . . . 4
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿)) ∈ ℂ) | 
| 54 | 53 | abscld 15475 | . . 3
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿))) ∈ ℝ) | 
| 55 | 44, 54 | readdcld 11290 | . 2
⊢ (𝜑 → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) + (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿)))) ∈ ℝ) | 
| 56 |  | 2re 12340 | . . 3
⊢ 2 ∈
ℝ | 
| 57 | 11, 2 | rerpdivcld 13108 | . . 3
⊢ (𝜑 → ((log‘𝐴) / 𝐴) ∈ ℝ) | 
| 58 |  | remulcl 11240 | . . 3
⊢ ((2
∈ ℝ ∧ ((log‘𝐴) / 𝐴) ∈ ℝ) → (2 ·
((log‘𝐴) / 𝐴)) ∈
ℝ) | 
| 59 | 56, 57, 58 | sylancr 587 | . 2
⊢ (𝜑 → (2 ·
((log‘𝐴) / 𝐴)) ∈
ℝ) | 
| 60 |  | relogdiv 26635 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → (log‘(𝐴 / 𝑚)) = ((log‘𝐴) − (log‘𝑚))) | 
| 61 | 2, 4, 60 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (log‘(𝐴 / 𝑚)) = ((log‘𝐴) − (log‘𝑚))) | 
| 62 | 61 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → ((log‘(𝐴 / 𝑚)) / 𝑚) = (((log‘𝐴) − (log‘𝑚)) / 𝑚)) | 
| 63 | 38 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (log‘𝐴) ∈ ℂ) | 
| 64 | 46 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (log‘𝑚) ∈ ℂ) | 
| 65 | 45 | rpcnne0d 13086 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) | 
| 66 |  | divsubdir 11961 | . . . . . . . . . 10
⊢
(((log‘𝐴)
∈ ℂ ∧ (log‘𝑚) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → (((log‘𝐴) − (log‘𝑚)) / 𝑚) = (((log‘𝐴) / 𝑚) − ((log‘𝑚) / 𝑚))) | 
| 67 | 63, 64, 65, 66 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (((log‘𝐴) − (log‘𝑚)) / 𝑚) = (((log‘𝐴) / 𝑚) − ((log‘𝑚) / 𝑚))) | 
| 68 | 62, 67 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → ((log‘(𝐴 / 𝑚)) / 𝑚) = (((log‘𝐴) / 𝑚) − ((log‘𝑚) / 𝑚))) | 
| 69 | 68 | sumeq2dv 15738 | . . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) = Σ𝑚 ∈ (1...(⌊‘𝐴))(((log‘𝐴) / 𝑚) − ((log‘𝑚) / 𝑚))) | 
| 70 | 1, 36, 48 | fsumsub 15824 | . . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))(((log‘𝐴) / 𝑚) − ((log‘𝑚) / 𝑚)) = (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚))) | 
| 71 | 69, 70 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) = (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚))) | 
| 72 |  | remulcl 11240 | . . . . . . . . . . . . 13
⊢
(((log‘𝐴)
∈ ℝ ∧ γ ∈ ℝ) → ((log‘𝐴) · γ) ∈
ℝ) | 
| 73 | 11, 14, 72 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝐴) · γ) ∈
ℝ) | 
| 74 | 13, 73 | readdcld 11290 | . . . . . . . . . . 11
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) +
((log‘𝐴) ·
γ)) ∈ ℝ) | 
| 75 | 74 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) +
((log‘𝐴) ·
γ)) ∈ ℂ) | 
| 76 | 75, 50 | pncand 11621 | . . . . . . . . 9
⊢ (𝜑 → ((((((log‘𝐴)↑2) / 2) +
((log‘𝐴) ·
γ)) + (((log‘𝐴)↑2) / 2)) − (((log‘𝐴)↑2) / 2)) =
((((log‘𝐴)↑2) /
2) + ((log‘𝐴)
· γ))) | 
| 77 | 14 | recni 11275 | . . . . . . . . . . . . 13
⊢ γ
∈ ℂ | 
| 78 | 77 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → γ ∈
ℂ) | 
| 79 | 38, 38, 78 | adddid 11285 | . . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝐴) · ((log‘𝐴) + γ)) =
(((log‘𝐴) ·
(log‘𝐴)) +
((log‘𝐴) ·
γ))) | 
| 80 | 12 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((log‘𝐴)↑2) ∈
ℂ) | 
| 81 | 80 | 2halvesd 12512 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) +
(((log‘𝐴)↑2) /
2)) = ((log‘𝐴)↑2)) | 
| 82 | 38 | sqvald 14183 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((log‘𝐴)↑2) = ((log‘𝐴) · (log‘𝐴))) | 
| 83 | 81, 82 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) +
(((log‘𝐴)↑2) /
2)) = ((log‘𝐴)
· (log‘𝐴))) | 
| 84 | 83 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝜑 → (((((log‘𝐴)↑2) / 2) +
(((log‘𝐴)↑2) /
2)) + ((log‘𝐴)
· γ)) = (((log‘𝐴) · (log‘𝐴)) + ((log‘𝐴) · γ))) | 
| 85 | 73 | recnd 11289 | . . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝐴) · γ) ∈
ℂ) | 
| 86 | 50, 50, 85 | add32d 11489 | . . . . . . . . . . 11
⊢ (𝜑 → (((((log‘𝐴)↑2) / 2) +
(((log‘𝐴)↑2) /
2)) + ((log‘𝐴)
· γ)) = (((((log‘𝐴)↑2) / 2) + ((log‘𝐴) · γ)) +
(((log‘𝐴)↑2) /
2))) | 
| 87 | 79, 84, 86 | 3eqtr2d 2783 | . . . . . . . . . 10
⊢ (𝜑 → ((log‘𝐴) · ((log‘𝐴) + γ)) =
(((((log‘𝐴)↑2) /
2) + ((log‘𝐴)
· γ)) + (((log‘𝐴)↑2) / 2))) | 
| 88 | 87 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝜑 → (((log‘𝐴) · ((log‘𝐴) + γ)) −
(((log‘𝐴)↑2) /
2)) = ((((((log‘𝐴)↑2) / 2) + ((log‘𝐴) · γ)) +
(((log‘𝐴)↑2) /
2)) − (((log‘𝐴)↑2) / 2))) | 
| 89 |  | mulcom 11241 | . . . . . . . . . . 11
⊢ ((γ
∈ ℂ ∧ (log‘𝐴) ∈ ℂ) → (γ ·
(log‘𝐴)) =
((log‘𝐴) ·
γ)) | 
| 90 | 77, 38, 89 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (γ ·
(log‘𝐴)) =
((log‘𝐴) ·
γ)) | 
| 91 | 90 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) + (γ
· (log‘𝐴))) =
((((log‘𝐴)↑2) /
2) + ((log‘𝐴)
· γ))) | 
| 92 | 76, 88, 91 | 3eqtr4rd 2788 | . . . . . . . 8
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) + (γ
· (log‘𝐴))) =
(((log‘𝐴) ·
((log‘𝐴) + γ))
− (((log‘𝐴)↑2) / 2))) | 
| 93 | 92 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → (((((log‘𝐴)↑2) / 2) + (γ
· (log‘𝐴)))
− 𝐿) =
((((log‘𝐴) ·
((log‘𝐴) + γ))
− (((log‘𝐴)↑2) / 2)) − 𝐿)) | 
| 94 | 90, 85 | eqeltrd 2841 | . . . . . . . 8
⊢ (𝜑 → (γ ·
(log‘𝐴)) ∈
ℂ) | 
| 95 | 50, 94, 51 | addsubassd 11640 | . . . . . . 7
⊢ (𝜑 → (((((log‘𝐴)↑2) / 2) + (γ
· (log‘𝐴)))
− 𝐿) =
((((log‘𝐴)↑2) /
2) + ((γ · (log‘𝐴)) − 𝐿))) | 
| 96 | 42, 50, 51 | subsub4d 11651 | . . . . . . 7
⊢ (𝜑 → ((((log‘𝐴) · ((log‘𝐴) + γ)) −
(((log‘𝐴)↑2) /
2)) − 𝐿) =
(((log‘𝐴) ·
((log‘𝐴) + γ))
− ((((log‘𝐴)↑2) / 2) + 𝐿))) | 
| 97 | 93, 95, 96 | 3eqtr3d 2785 | . . . . . 6
⊢ (𝜑 → ((((log‘𝐴)↑2) / 2) + ((γ
· (log‘𝐴))
− 𝐿)) =
(((log‘𝐴) ·
((log‘𝐴) + γ))
− ((((log‘𝐴)↑2) / 2) + 𝐿))) | 
| 98 | 71, 97 | oveq12d 7449 | . . . . 5
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ ·
(log‘𝐴)) −
𝐿))) = ((Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚)) − (((log‘𝐴) · ((log‘𝐴) + γ)) − ((((log‘𝐴)↑2) / 2) + 𝐿)))) | 
| 99 | 37, 49, 42, 52 | sub4d 11669 | . . . . 5
⊢ (𝜑 → ((Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚)) − (((log‘𝐴) · ((log‘𝐴) + γ)) − ((((log‘𝐴)↑2) / 2) + 𝐿))) = ((Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ))) − (Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿)))) | 
| 100 | 98, 99 | eqtrd 2777 | . . . 4
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ ·
(log‘𝐴)) −
𝐿))) = ((Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ))) − (Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿)))) | 
| 101 | 100 | fveq2d 6910 | . . 3
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ ·
(log‘𝐴)) −
𝐿)))) =
(abs‘((Σ𝑚
∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ))) − (Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿))))) | 
| 102 | 43, 53 | abs2dif2d 15497 | . . 3
⊢ (𝜑 → (abs‘((Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ))) − (Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿)))) ≤ ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) + (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿))))) | 
| 103 | 101, 102 | eqbrtrd 5165 | . 2
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ ·
(log‘𝐴)) −
𝐿)))) ≤
((abs‘(Σ𝑚
∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) + (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿))))) | 
| 104 |  | harmonicbnd4 27054 | . . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (abs‘(Σ𝑚
∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴)) | 
| 105 | 2, 104 | syl 17 | . . . . . 6
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) + γ)))
≤ (1 / 𝐴)) | 
| 106 | 8 | nnrecred 12317 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (1 / 𝑚) ∈ ℝ) | 
| 107 | 1, 106 | fsumrecl 15770 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) ∈ ℝ) | 
| 108 | 107, 40 | resubcld 11691 | . . . . . . . . 9
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ)) ∈
ℝ) | 
| 109 | 108 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ)) ∈
ℂ) | 
| 110 | 109 | abscld 15475 | . . . . . . 7
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) + γ)))
∈ ℝ) | 
| 111 | 2 | rprecred 13088 | . . . . . . 7
⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | 
| 112 |  | 0red 11264 | . . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) | 
| 113 |  | 1red 11262 | . . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) | 
| 114 |  | 0lt1 11785 | . . . . . . . . 9
⊢ 0 <
1 | 
| 115 | 114 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 0 < 1) | 
| 116 |  | loge 26628 | . . . . . . . . 9
⊢
(log‘e) = 1 | 
| 117 |  | mulog2sumlem1.3 | . . . . . . . . . 10
⊢ (𝜑 → e ≤ 𝐴) | 
| 118 |  | epr 16244 | . . . . . . . . . . 11
⊢ e ∈
ℝ+ | 
| 119 |  | logleb 26645 | . . . . . . . . . . 11
⊢ ((e
∈ ℝ+ ∧ 𝐴 ∈ ℝ+) → (e ≤
𝐴 ↔ (log‘e) ≤
(log‘𝐴))) | 
| 120 | 118, 2, 119 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (e ≤ 𝐴 ↔ (log‘e) ≤ (log‘𝐴))) | 
| 121 | 117, 120 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (log‘e) ≤
(log‘𝐴)) | 
| 122 | 116, 121 | eqbrtrrid 5179 | . . . . . . . 8
⊢ (𝜑 → 1 ≤ (log‘𝐴)) | 
| 123 | 112, 113,
11, 115, 122 | ltletrd 11421 | . . . . . . 7
⊢ (𝜑 → 0 < (log‘𝐴)) | 
| 124 |  | lemul2 12120 | . . . . . . 7
⊢
(((abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ∈ ℝ ∧ (1 /
𝐴) ∈ ℝ ∧
((log‘𝐴) ∈
ℝ ∧ 0 < (log‘𝐴))) → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) + γ)))
≤ (1 / 𝐴) ↔
((log‘𝐴) ·
(abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ)))) ≤ ((log‘𝐴) · (1 / 𝐴)))) | 
| 125 | 110, 111,
11, 123, 124 | syl112anc 1376 | . . . . . 6
⊢ (𝜑 → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) + γ)))
≤ (1 / 𝐴) ↔
((log‘𝐴) ·
(abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ)))) ≤ ((log‘𝐴) · (1 / 𝐴)))) | 
| 126 | 105, 125 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((log‘𝐴) ·
(abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ)))) ≤ ((log‘𝐴) · (1 / 𝐴))) | 
| 127 | 45 | rpcnd 13079 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → 𝑚 ∈ ℂ) | 
| 128 | 45 | rpne0d 13082 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → 𝑚 ≠ 0) | 
| 129 | 63, 127, 128 | divrecd 12046 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → ((log‘𝐴) / 𝑚) = ((log‘𝐴) · (1 / 𝑚))) | 
| 130 | 129 | sumeq2dv 15738 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) = Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) · (1 / 𝑚))) | 
| 131 | 106 | recnd 11289 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → (1 / 𝑚) ∈ ℂ) | 
| 132 | 1, 38, 131 | fsummulc2 15820 | . . . . . . . . . 10
⊢ (𝜑 → ((log‘𝐴) · Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) = Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) · (1 / 𝑚))) | 
| 133 | 130, 132 | eqtr4d 2780 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) = ((log‘𝐴) · Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚))) | 
| 134 | 133 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ))) = (((log‘𝐴) · Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) −
((log‘𝐴) ·
((log‘𝐴) +
γ)))) | 
| 135 | 1, 131 | fsumcl 15769 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) ∈ ℂ) | 
| 136 | 38, 135, 41 | subdid 11719 | . . . . . . . 8
⊢ (𝜑 → ((log‘𝐴) · (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) + γ)))
= (((log‘𝐴) ·
Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) −
((log‘𝐴) ·
((log‘𝐴) +
γ)))) | 
| 137 | 134, 136 | eqtr4d 2780 | . . . . . . 7
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ))) = ((log‘𝐴) · (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ)))) | 
| 138 | 137 | fveq2d 6910 | . . . . . 6
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) =
(abs‘((log‘𝐴)
· (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ))))) | 
| 139 | 135, 41 | subcld 11620 | . . . . . . 7
⊢ (𝜑 → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ)) ∈
ℂ) | 
| 140 | 38, 139 | absmuld 15493 | . . . . . 6
⊢ (𝜑 →
(abs‘((log‘𝐴)
· (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ)))) = ((abs‘(log‘𝐴)) · (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ))))) | 
| 141 | 112, 11, 123 | ltled 11409 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ (log‘𝐴)) | 
| 142 | 11, 141 | absidd 15461 | . . . . . . 7
⊢ (𝜑 →
(abs‘(log‘𝐴)) =
(log‘𝐴)) | 
| 143 | 142 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 →
((abs‘(log‘𝐴))
· (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ)))) = ((log‘𝐴) ·
(abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ))))) | 
| 144 | 138, 140,
143 | 3eqtrd 2781 | . . . . 5
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) = ((log‘𝐴) ·
(abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ))))) | 
| 145 | 2 | rpcnd 13079 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 146 | 2 | rpne0d 13082 | . . . . . 6
⊢ (𝜑 → 𝐴 ≠ 0) | 
| 147 | 38, 145, 146 | divrecd 12046 | . . . . 5
⊢ (𝜑 → ((log‘𝐴) / 𝐴) = ((log‘𝐴) · (1 / 𝐴))) | 
| 148 | 126, 144,
147 | 3brtr4d 5175 | . . . 4
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) ≤ ((log‘𝐴) / 𝐴)) | 
| 149 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑚 → (log‘𝑖) = (log‘𝑚)) | 
| 150 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑚 → 𝑖 = 𝑚) | 
| 151 | 149, 150 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑚 → ((log‘𝑖) / 𝑖) = ((log‘𝑚) / 𝑚)) | 
| 152 | 151 | cbvsumv 15732 | . . . . . . . . . . . 12
⊢
Σ𝑖 ∈
(1...(⌊‘𝑦))((log‘𝑖) / 𝑖) = Σ𝑚 ∈ (1...(⌊‘𝑦))((log‘𝑚) / 𝑚) | 
| 153 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐴 → (⌊‘𝑦) = (⌊‘𝐴)) | 
| 154 | 153 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (1...(⌊‘𝑦)) = (1...(⌊‘𝐴))) | 
| 155 | 154 | sumeq1d 15736 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → Σ𝑚 ∈ (1...(⌊‘𝑦))((log‘𝑚) / 𝑚) = Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚)) | 
| 156 | 152, 155 | eqtrid 2789 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) = Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚)) | 
| 157 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (log‘𝑦) = (log‘𝐴)) | 
| 158 | 157 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → ((log‘𝑦)↑2) = ((log‘𝐴)↑2)) | 
| 159 | 158 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (((log‘𝑦)↑2) / 2) = (((log‘𝐴)↑2) / 2)) | 
| 160 | 156, 159 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)) = (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − (((log‘𝐴)↑2) / 2))) | 
| 161 |  | ovex 7464 | . . . . . . . . . 10
⊢
(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − (((log‘𝐴)↑2) / 2)) ∈ V | 
| 162 | 160, 19, 161 | fvmpt 7016 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐹‘𝐴) = (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − (((log‘𝐴)↑2) / 2))) | 
| 163 | 2, 162 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐴) = (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − (((log‘𝐴)↑2) / 2))) | 
| 164 | 163 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐴) − 𝐿) = ((Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − (((log‘𝐴)↑2) / 2)) − 𝐿)) | 
| 165 | 49, 50, 51 | subsub4d 11651 | . . . . . . 7
⊢ (𝜑 → ((Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − (((log‘𝐴)↑2) / 2)) − 𝐿) = (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿))) | 
| 166 | 164, 165 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → ((𝐹‘𝐴) − 𝐿) = (Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿))) | 
| 167 | 166 | fveq2d 6910 | . . . . 5
⊢ (𝜑 → (abs‘((𝐹‘𝐴) − 𝐿)) = (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿)))) | 
| 168 | 20 | simp3i 1142 | . . . . . 6
⊢ ((𝐹 ⇝𝑟
𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤
𝐴) →
(abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴)) | 
| 169 | 24, 2, 117, 168 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴)) | 
| 170 | 167, 169 | eqbrtrrd 5167 | . . . 4
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿))) ≤ ((log‘𝐴) / 𝐴)) | 
| 171 | 44, 54, 57, 57, 148, 170 | le2addd 11882 | . . 3
⊢ (𝜑 → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) + (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿)))) ≤ (((log‘𝐴) / 𝐴) + ((log‘𝐴) / 𝐴))) | 
| 172 | 57 | recnd 11289 | . . . 4
⊢ (𝜑 → ((log‘𝐴) / 𝐴) ∈ ℂ) | 
| 173 | 172 | 2timesd 12509 | . . 3
⊢ (𝜑 → (2 ·
((log‘𝐴) / 𝐴)) = (((log‘𝐴) / 𝐴) + ((log‘𝐴) / 𝐴))) | 
| 174 | 171, 173 | breqtrrd 5171 | . 2
⊢ (𝜑 → ((abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝐴) / 𝑚) − ((log‘𝐴) · ((log‘𝐴) + γ)))) + (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘𝑚) / 𝑚) − ((((log‘𝐴)↑2) / 2) + 𝐿)))) ≤ (2 · ((log‘𝐴) / 𝐴))) | 
| 175 | 33, 55, 59, 103, 174 | letrd 11418 | 1
⊢ (𝜑 → (abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ ·
(log‘𝐴)) −
𝐿)))) ≤ (2 ·
((log‘𝐴) / 𝐴))) |