Proof of Theorem harmonicbnd4
Step | Hyp | Ref
| Expression |
1 | | fzfid 13156 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1...(⌊‘𝐴)) ∈ Fin) |
2 | | elfznn 12752 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘𝐴))
→ 𝑚 ∈
ℕ) |
3 | 2 | adantl 474 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ 𝑚 ∈
ℕ) |
4 | 3 | nnrecred 11491 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑚) ∈
ℝ) |
5 | 1, 4 | fsumrecl 14951 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) ∈
ℝ) |
6 | 5 | recnd 10468 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) ∈
ℂ) |
7 | | relogcl 24860 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
8 | 7 | recnd 10468 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℂ) |
9 | | emre 25285 |
. . . . . 6
⊢ γ
∈ ℝ |
10 | 9 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ γ ∈ ℝ) |
11 | 10 | recnd 10468 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ γ ∈ ℂ) |
12 | 6, 8, 11 | subsub4d 10829 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − γ) =
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ))) |
13 | 12 | fveq2d 6503 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) =
(abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ)))) |
14 | | rpreccl 12232 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℝ+) |
15 | 14 | rpred 12248 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℝ) |
16 | | resubcl 10751 |
. . . . 5
⊢ ((γ
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (γ − (1
/ 𝐴)) ∈
ℝ) |
17 | 9, 15, 16 | sylancr 578 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ∈ ℝ) |
18 | | rprege0 12221 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴)) |
19 | | flge0nn0 13005 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
21 | | nn0p1nn 11748 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℕ0 → ((⌊‘𝐴) + 1) ∈ ℕ) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℕ) |
23 | 22 | nnrpd 12246 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℝ+) |
24 | | relogcl 24860 |
. . . . . 6
⊢
(((⌊‘𝐴)
+ 1) ∈ ℝ+ → (log‘((⌊‘𝐴) + 1)) ∈
ℝ) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ∈ ℝ) |
26 | 5, 25 | resubcld 10869 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ) |
27 | 5, 7 | resubcld 10869 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ∈
ℝ) |
28 | 22 | nnrecred 11491 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ∈ ℝ) |
29 | | fzfid 13156 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (1...((⌊‘𝐴) + 1)) ∈ Fin) |
30 | | elfznn 12752 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...((⌊‘𝐴) +
1)) → 𝑚 ∈
ℕ) |
31 | 30 | adantl 474 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → 𝑚 ∈
ℕ) |
32 | 31 | nnrecred 11491 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → (1 / 𝑚) ∈
ℝ) |
33 | 29, 32 | fsumrecl 14951 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) ∈
ℝ) |
34 | 33, 25 | resubcld 10869 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ) |
35 | | harmonicbnd 25283 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
+ 1) ∈ ℕ → (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈
(γ[,]1)) |
36 | 22, 35 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈
(γ[,]1)) |
37 | | 1re 10439 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
38 | 9, 37 | elicc2i 12618 |
. . . . . . . 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 1126 |
. . . . . . 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 12212 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
42 | | fllep1 12986 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
44 | | rpregt0 12220 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 < 𝐴)) |
45 | 22 | nnred 11456 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℝ) |
46 | 22 | nngt0d 11489 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 0 < ((⌊‘𝐴) + 1)) |
47 | | lerec 11324 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧
(((⌊‘𝐴) + 1)
∈ ℝ ∧ 0 < ((⌊‘𝐴) + 1))) → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴))) |
48 | 44, 45, 46, 47 | syl12anc 824 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ≤
((⌊‘𝐴) + 1)
↔ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴))) |
49 | 43, 48 | mpbid 224 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴)) |
50 | 10, 28, 34, 15, 40, 49 | le2subd 11061 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) − (1 /
((⌊‘𝐴) +
1)))) |
51 | 33 | recnd 10468 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) ∈
ℂ) |
52 | 25 | recnd 10468 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ∈ ℂ) |
53 | 28 | recnd 10468 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ∈ ℂ) |
54 | 51, 52, 53 | sub32d 10830 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))) = ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1)))
− (log‘((⌊‘𝐴) + 1)))) |
55 | | nnuz 12095 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
56 | 22, 55 | syl6eleq 2876 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ (ℤ≥‘1)) |
57 | 32 | recnd 10468 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → (1 / 𝑚) ∈
ℂ) |
58 | | oveq2 6984 |
. . . . . . . . . 10
⊢ (𝑚 = ((⌊‘𝐴) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝐴) + 1))) |
59 | 56, 57, 58 | fsumm1 14966 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) = (Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) + (1
/ ((⌊‘𝐴) +
1)))) |
60 | 20 | nn0cnd 11769 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℂ) |
61 | | ax-1cn 10393 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
62 | | pncan 10692 |
. . . . . . . . . . . . 13
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝐴) + 1) − 1) =
(⌊‘𝐴)) |
63 | 60, 61, 62 | sylancl 577 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) − 1) = (⌊‘𝐴)) |
64 | 63 | oveq2d 6992 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1...(((⌊‘𝐴) + 1) − 1)) =
(1...(⌊‘𝐴))) |
65 | 64 | sumeq1d 14918 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) =
Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) |
66 | 65 | oveq1d 6991 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) + (1
/ ((⌊‘𝐴) + 1)))
= (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) + (1 /
((⌊‘𝐴) +
1)))) |
67 | 59, 66 | eqtrd 2814 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) = (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) + (1 /
((⌊‘𝐴) +
1)))) |
68 | 6, 53, 67 | mvrraddd 10853 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1))) =
Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) |
69 | 68 | oveq1d 6991 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1)))
− (log‘((⌊‘𝐴) + 1))) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1)))) |
70 | 54, 69 | eqtrd 2814 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))) = (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
71 | 50, 70 | breqtrd 4955 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1)))) |
72 | | logleb 24887 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ ((⌊‘𝐴) +
1) ∈ ℝ+) → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (log‘𝐴) ≤ (log‘((⌊‘𝐴) + 1)))) |
73 | 23, 72 | mpdan 674 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ≤
((⌊‘𝐴) + 1)
↔ (log‘𝐴) ≤
(log‘((⌊‘𝐴) + 1)))) |
74 | 43, 73 | mpbid 224 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ≤
(log‘((⌊‘𝐴) + 1))) |
75 | 7, 25, 5, 74 | lesub2dd 11058 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴))) |
76 | 17, 26, 27, 71, 75 | letrd 10597 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴))) |
77 | 27, 15 | resubcld 10869 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ∈
ℝ) |
78 | 15 | recnd 10468 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℂ) |
79 | 6, 8, 78 | subsub4d 10829 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + (1 / 𝐴)))) |
80 | 7, 15 | readdcld 10469 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘𝐴) + (1
/ 𝐴)) ∈
ℝ) |
81 | | id 22 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ+) |
82 | 23, 81 | relogdivd 24910 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) = ((log‘((⌊‘𝐴) + 1)) − (log‘𝐴))) |
83 | | rerpdivcl 12236 |
. . . . . . . . . . . . 13
⊢
((((⌊‘𝐴)
+ 1) ∈ ℝ ∧ 𝐴
∈ ℝ+) → (((⌊‘𝐴) + 1) / 𝐴) ∈ ℝ) |
84 | 45, 83 | mpancom 675 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ∈
ℝ) |
85 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 1 ∈ ℝ) |
86 | 85, 15 | readdcld 10469 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) ∈
ℝ) |
87 | 15 | reefcld 15301 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (exp‘(1 / 𝐴))
∈ ℝ) |
88 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ 1 ∈ ℂ) |
89 | | rpcnne0 12224 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℂ
∧ 𝐴 ≠
0)) |
90 | | divdir 11124 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → (((⌊‘𝐴) + 1) / 𝐴) = (((⌊‘𝐴) / 𝐴) + (1 / 𝐴))) |
91 | 60, 88, 89, 90 | syl3anc 1351 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) =
(((⌊‘𝐴) / 𝐴) + (1 / 𝐴))) |
92 | | reflcl 12981 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
93 | 41, 92 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
94 | | rerpdivcl 12236 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 𝐴
∈ ℝ+) → ((⌊‘𝐴) / 𝐴) ∈ ℝ) |
95 | 93, 94 | mpancom 675 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) /
𝐴) ∈
ℝ) |
96 | | flle 12984 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
97 | 41, 96 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ 𝐴) |
98 | | rpcn 12216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
99 | 98 | mulid1d 10457 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ+
→ (𝐴 · 1) =
𝐴) |
100 | 97, 99 | breqtrrd 4957 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ (𝐴 ·
1)) |
101 | | ledivmul 11317 |
. . . . . . . . . . . . . . . 16
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (((⌊‘𝐴) / 𝐴) ≤ 1 ↔ (⌊‘𝐴) ≤ (𝐴 · 1))) |
102 | 93, 85, 44, 101 | syl3anc 1351 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
/ 𝐴) ≤ 1 ↔
(⌊‘𝐴) ≤
(𝐴 ·
1))) |
103 | 100, 102 | mpbird 249 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) /
𝐴) ≤ 1) |
104 | 95, 85, 15, 103 | leadd1dd 11055 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
/ 𝐴) + (1 / 𝐴)) ≤ (1 + (1 / 𝐴))) |
105 | 91, 104 | eqbrtrd 4951 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ≤ (1 + (1 /
𝐴))) |
106 | | efgt1p 15328 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝐴) ∈
ℝ+ → (1 + (1 / 𝐴)) < (exp‘(1 / 𝐴))) |
107 | 14, 106 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) <
(exp‘(1 / 𝐴))) |
108 | 86, 87, 107 | ltled 10588 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) ≤
(exp‘(1 / 𝐴))) |
109 | 84, 86, 87, 105, 108 | letrd 10597 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ≤
(exp‘(1 / 𝐴))) |
110 | | rpdivcl 12231 |
. . . . . . . . . . . . 13
⊢
((((⌊‘𝐴)
+ 1) ∈ ℝ+ ∧ 𝐴 ∈ ℝ+) →
(((⌊‘𝐴) + 1) /
𝐴) ∈
ℝ+) |
111 | 23, 110 | mpancom 675 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ∈
ℝ+) |
112 | 15 | rpefcld 15318 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (exp‘(1 / 𝐴))
∈ ℝ+) |
113 | 111, 112 | logled 24911 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ ((((⌊‘𝐴)
+ 1) / 𝐴) ≤
(exp‘(1 / 𝐴)) ↔
(log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (log‘(exp‘(1 / 𝐴))))) |
114 | 109, 113 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (log‘(exp‘(1 / 𝐴)))) |
115 | 15 | relogefd 24912 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(exp‘(1 / 𝐴))) = (1 / 𝐴)) |
116 | 114, 115 | breqtrd 4955 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (1 / 𝐴)) |
117 | 82, 116 | eqbrtrrd 4953 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)) ≤ (1 / 𝐴)) |
118 | 25, 7, 15 | lesubadd2d 11040 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)) ≤ (1 / 𝐴) ↔ (log‘((⌊‘𝐴) + 1)) ≤ ((log‘𝐴) + (1 / 𝐴)))) |
119 | 117, 118 | mpbid 224 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ≤ ((log‘𝐴) + (1 / 𝐴))) |
120 | 25, 80, 5, 119 | lesub2dd 11058 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) + (1 / 𝐴))) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
121 | 79, 120 | eqbrtrd 4951 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
122 | | harmonicbnd3 25287 |
. . . . . . 7
⊢
((⌊‘𝐴)
∈ ℕ0 → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈
(0[,]γ)) |
123 | 20, 122 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈
(0[,]γ)) |
124 | | 0re 10441 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
125 | 124, 9 | elicc2i 12618 |
. . . . . . 7
⊢
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ) ↔
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ ∧ 0 ≤
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∧ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤
γ)) |
126 | 125 | simp3bi 1127 |
. . . . . 6
⊢
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ) →
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ γ) |
127 | 123, 126 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ γ) |
128 | 77, 26, 10, 121, 127 | letrd 10597 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤
γ) |
129 | 27, 15, 10 | lesubaddd 11038 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ γ ↔
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴)))) |
130 | 128, 129 | mpbid 224 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴))) |
131 | 27, 10, 15 | absdifled 14655 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) ≤ (1 / 𝐴) ↔ ((γ − (1 /
𝐴)) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ∧ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴))))) |
132 | 76, 130, 131 | mpbir2and 700 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) ≤ (1 / 𝐴)) |
133 | 13, 132 | eqbrtrrd 4953 |
1
⊢ (𝐴 ∈ ℝ+
→ (abs‘(Σ𝑚
∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴)) |