Proof of Theorem harmonicbnd4
Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1...(⌊‘𝐴)) ∈ Fin) |
2 | | elfznn 12241 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘𝐴))
→ 𝑚 ∈
ℕ) |
3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ 𝑚 ∈
ℕ) |
4 | 3 | nnrecred 10943 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑚) ∈
ℝ) |
5 | 1, 4 | fsumrecl 14312 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) ∈
ℝ) |
6 | 5 | recnd 9947 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) ∈
ℂ) |
7 | | relogcl 24126 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
8 | 7 | recnd 9947 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℂ) |
9 | | emre 24532 |
. . . . . 6
⊢ γ
∈ ℝ |
10 | 9 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ γ ∈ ℝ) |
11 | 10 | recnd 9947 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ γ ∈ ℂ) |
12 | 6, 8, 11 | subsub4d 10302 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − γ) =
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ))) |
13 | 12 | fveq2d 6107 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) =
(abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ)))) |
14 | | rpreccl 11733 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℝ+) |
15 | 14 | rpred 11748 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℝ) |
16 | | resubcl 10224 |
. . . . 5
⊢ ((γ
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (γ − (1
/ 𝐴)) ∈
ℝ) |
17 | 9, 15, 16 | sylancr 694 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ∈ ℝ) |
18 | | rprege0 11723 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴)) |
19 | | flge0nn0 12483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
21 | | nn0p1nn 11209 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℕ0 → ((⌊‘𝐴) + 1) ∈ ℕ) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℕ) |
23 | 22 | nnrpd 11746 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℝ+) |
24 | | relogcl 24126 |
. . . . . 6
⊢
(((⌊‘𝐴)
+ 1) ∈ ℝ+ → (log‘((⌊‘𝐴) + 1)) ∈
ℝ) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ∈ ℝ) |
26 | 5, 25 | resubcld 10337 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ) |
27 | 5, 7 | resubcld 10337 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ∈
ℝ) |
28 | 22 | nnrecred 10943 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ∈ ℝ) |
29 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (1...((⌊‘𝐴) + 1)) ∈ Fin) |
30 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...((⌊‘𝐴) +
1)) → 𝑚 ∈
ℕ) |
31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → 𝑚 ∈
ℕ) |
32 | 31 | nnrecred 10943 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → (1 / 𝑚) ∈
ℝ) |
33 | 29, 32 | fsumrecl 14312 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) ∈
ℝ) |
34 | 33, 25 | resubcld 10337 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ) |
35 | | harmonicbnd 24530 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
+ 1) ∈ ℕ → (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈
(γ[,]1)) |
36 | 22, 35 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈
(γ[,]1)) |
37 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
38 | 9, 37 | elicc2i 12110 |
. . . . . . . 8
⊢
((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (γ[,]1) ↔
((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ ∧ γ ≤
(Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∧ (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤
1)) |
39 | 38 | simp2bi 1070 |
. . . . . . 7
⊢
((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (γ[,]1) → γ
≤ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
40 | 36, 39 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ γ ≤ (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1)))) |
41 | | rpre 11715 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
42 | | fllep1 12464 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
44 | | rpregt0 11722 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 < 𝐴)) |
45 | 22 | nnred 10912 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℝ) |
46 | 22 | nngt0d 10941 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 0 < ((⌊‘𝐴) + 1)) |
47 | | lerec 10785 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧
(((⌊‘𝐴) + 1)
∈ ℝ ∧ 0 < ((⌊‘𝐴) + 1))) → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴))) |
48 | 44, 45, 46, 47 | syl12anc 1316 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ≤
((⌊‘𝐴) + 1)
↔ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴))) |
49 | 43, 48 | mpbid 221 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴)) |
50 | 10, 28, 34, 15, 40, 49 | le2subd 10526 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) − (1 /
((⌊‘𝐴) +
1)))) |
51 | 33 | recnd 9947 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) ∈
ℂ) |
52 | 25 | recnd 9947 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ∈ ℂ) |
53 | 28 | recnd 9947 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ∈ ℂ) |
54 | 51, 52, 53 | sub32d 10303 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))) = ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1)))
− (log‘((⌊‘𝐴) + 1)))) |
55 | | nnuz 11599 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
56 | 22, 55 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ (ℤ≥‘1)) |
57 | 32 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → (1 / 𝑚) ∈
ℂ) |
58 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝐴) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝐴) + 1))) |
59 | 56, 57, 58 | fsumm1 14324 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) = (Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) + (1
/ ((⌊‘𝐴) +
1)))) |
60 | 20 | nn0cnd 11230 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℂ) |
61 | | ax-1cn 9873 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
62 | | pncan 10166 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝐴) + 1) − 1) =
(⌊‘𝐴)) |
63 | 60, 61, 62 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) − 1) = (⌊‘𝐴)) |
64 | 63 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (1...(((⌊‘𝐴) + 1) − 1)) =
(1...(⌊‘𝐴))) |
65 | 64 | sumeq1d 14279 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) =
Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) |
66 | 65 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) + (1
/ ((⌊‘𝐴) + 1)))
= (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) + (1 /
((⌊‘𝐴) +
1)))) |
67 | 59, 66 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) = (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) + (1 /
((⌊‘𝐴) +
1)))) |
68 | 67 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1))) =
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) + (1 /
((⌊‘𝐴) + 1)))
− (1 / ((⌊‘𝐴) + 1)))) |
69 | 6, 53 | pncand 10272 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) + (1 /
((⌊‘𝐴) + 1)))
− (1 / ((⌊‘𝐴) + 1))) = Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚)) |
70 | 68, 69 | eqtrd 2644 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1))) =
Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) |
71 | 70 | oveq1d 6564 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1)))
− (log‘((⌊‘𝐴) + 1))) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1)))) |
72 | 54, 71 | eqtrd 2644 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))) = (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
73 | 50, 72 | breqtrd 4609 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1)))) |
74 | | logleb 24153 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ ((⌊‘𝐴) +
1) ∈ ℝ+) → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (log‘𝐴) ≤ (log‘((⌊‘𝐴) + 1)))) |
75 | 23, 74 | mpdan 699 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ≤
((⌊‘𝐴) + 1)
↔ (log‘𝐴) ≤
(log‘((⌊‘𝐴) + 1)))) |
76 | 43, 75 | mpbid 221 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ≤
(log‘((⌊‘𝐴) + 1))) |
77 | 7, 25, 5, 76 | lesub2dd 10523 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴))) |
78 | 17, 26, 27, 73, 77 | letrd 10073 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴))) |
79 | 27, 15 | resubcld 10337 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ∈
ℝ) |
80 | 15 | recnd 9947 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℂ) |
81 | 6, 8, 80 | subsub4d 10302 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + (1 / 𝐴)))) |
82 | 7, 15 | readdcld 9948 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘𝐴) + (1
/ 𝐴)) ∈
ℝ) |
83 | | id 22 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ+) |
84 | 23, 83 | relogdivd 24176 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) = ((log‘((⌊‘𝐴) + 1)) − (log‘𝐴))) |
85 | | rerpdivcl 11737 |
. . . . . . . . . . . . 13
⊢
((((⌊‘𝐴)
+ 1) ∈ ℝ ∧ 𝐴
∈ ℝ+) → (((⌊‘𝐴) + 1) / 𝐴) ∈ ℝ) |
86 | 45, 85 | mpancom 700 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ∈
ℝ) |
87 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 1 ∈ ℝ) |
88 | 87, 15 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) ∈
ℝ) |
89 | 15 | reefcld 14657 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (exp‘(1 / 𝐴))
∈ ℝ) |
90 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ 1 ∈ ℂ) |
91 | | rpcnne0 11726 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℂ
∧ 𝐴 ≠
0)) |
92 | | divdir 10589 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → (((⌊‘𝐴) + 1) / 𝐴) = (((⌊‘𝐴) / 𝐴) + (1 / 𝐴))) |
93 | 60, 90, 91, 92 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) =
(((⌊‘𝐴) / 𝐴) + (1 / 𝐴))) |
94 | | reflcl 12459 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
95 | 41, 94 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
96 | | rerpdivcl 11737 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 𝐴
∈ ℝ+) → ((⌊‘𝐴) / 𝐴) ∈ ℝ) |
97 | 95, 96 | mpancom 700 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) /
𝐴) ∈
ℝ) |
98 | | flle 12462 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
99 | 41, 98 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ 𝐴) |
100 | | rpcn 11717 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
101 | 100 | mulid1d 9936 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ+
→ (𝐴 · 1) =
𝐴) |
102 | 99, 101 | breqtrrd 4611 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ (𝐴 ·
1)) |
103 | | ledivmul 10778 |
. . . . . . . . . . . . . . . 16
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (((⌊‘𝐴) / 𝐴) ≤ 1 ↔ (⌊‘𝐴) ≤ (𝐴 · 1))) |
104 | 95, 87, 44, 103 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
/ 𝐴) ≤ 1 ↔
(⌊‘𝐴) ≤
(𝐴 ·
1))) |
105 | 102, 104 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) /
𝐴) ≤ 1) |
106 | 97, 87, 15, 105 | leadd1dd 10520 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
/ 𝐴) + (1 / 𝐴)) ≤ (1 + (1 / 𝐴))) |
107 | 93, 106 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ≤ (1 + (1 /
𝐴))) |
108 | | efgt1p 14684 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝐴) ∈
ℝ+ → (1 + (1 / 𝐴)) < (exp‘(1 / 𝐴))) |
109 | 14, 108 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) <
(exp‘(1 / 𝐴))) |
110 | 88, 89, 109 | ltled 10064 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) ≤
(exp‘(1 / 𝐴))) |
111 | 86, 88, 89, 107, 110 | letrd 10073 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ≤
(exp‘(1 / 𝐴))) |
112 | | rpdivcl 11732 |
. . . . . . . . . . . . 13
⊢
((((⌊‘𝐴)
+ 1) ∈ ℝ+ ∧ 𝐴 ∈ ℝ+) →
(((⌊‘𝐴) + 1) /
𝐴) ∈
ℝ+) |
113 | 23, 112 | mpancom 700 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ∈
ℝ+) |
114 | 15 | rpefcld 14674 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (exp‘(1 / 𝐴))
∈ ℝ+) |
115 | 113, 114 | logled 24177 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ ((((⌊‘𝐴)
+ 1) / 𝐴) ≤
(exp‘(1 / 𝐴)) ↔
(log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (log‘(exp‘(1 / 𝐴))))) |
116 | 111, 115 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (log‘(exp‘(1 / 𝐴)))) |
117 | 15 | relogefd 24178 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(exp‘(1 / 𝐴))) = (1 / 𝐴)) |
118 | 116, 117 | breqtrd 4609 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (1 / 𝐴)) |
119 | 84, 118 | eqbrtrrd 4607 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)) ≤ (1 / 𝐴)) |
120 | 25, 7, 15 | lesubadd2d 10505 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)) ≤ (1 / 𝐴) ↔ (log‘((⌊‘𝐴) + 1)) ≤ ((log‘𝐴) + (1 / 𝐴)))) |
121 | 119, 120 | mpbid 221 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ≤ ((log‘𝐴) + (1 / 𝐴))) |
122 | 25, 82, 5, 121 | lesub2dd 10523 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) + (1 / 𝐴))) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
123 | 81, 122 | eqbrtrd 4605 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
124 | | harmonicbnd3 24534 |
. . . . . . 7
⊢
((⌊‘𝐴)
∈ ℕ0 → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈
(0[,]γ)) |
125 | 20, 124 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈
(0[,]γ)) |
126 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
127 | 126, 9 | elicc2i 12110 |
. . . . . . 7
⊢
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ) ↔
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ ∧ 0 ≤
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∧ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤
γ)) |
128 | 127 | simp3bi 1071 |
. . . . . 6
⊢
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ) →
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ γ) |
129 | 125, 128 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ γ) |
130 | 79, 26, 10, 123, 129 | letrd 10073 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤
γ) |
131 | 27, 15, 10 | lesubaddd 10503 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ γ ↔
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴)))) |
132 | 130, 131 | mpbid 221 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴))) |
133 | 27, 10, 15 | absdifled 14021 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) ≤ (1 / 𝐴) ↔ ((γ − (1 /
𝐴)) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ∧ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴))))) |
134 | 78, 132, 133 | mpbir2and 959 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) ≤ (1 / 𝐴)) |
135 | 13, 134 | eqbrtrrd 4607 |
1
⊢ (𝐴 ∈ ℝ+
→ (abs‘(Σ𝑚
∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴)) |