Step | Hyp | Ref
| Expression |
1 | | 2re 11090 |
. . . 4
⊢ 2 ∈
ℝ |
2 | | fzfid 12772 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(1...𝑁) ∈
Fin) |
3 | | elfzuz 12338 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈
(ℤ≥‘1)) |
4 | 3 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈
(ℤ≥‘1)) |
5 | | nnuz 11723 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
6 | 4, 5 | syl6eleqr 2712 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ) |
7 | 6 | nnrpd 11870 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ+) |
8 | 7 | relogcld 24369 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (log‘𝑛) ∈ ℝ) |
9 | 8, 6 | nndivred 11069 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((log‘𝑛) / 𝑛) ∈ ℝ) |
10 | 2, 9 | fsumrecl 14465 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ∈ ℝ) |
11 | | remulcl 10021 |
. . . 4
⊢ ((2
∈ ℝ ∧ Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ∈ ℝ) → (2 ·
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛)) ∈ ℝ) |
12 | 1, 10, 11 | sylancr 695 |
. . 3
⊢ (𝑁 ∈ ℕ → (2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) ∈ ℝ) |
13 | | elfznn 12370 |
. . . . . . 7
⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ) |
14 | 13 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → 𝑖 ∈ ℕ) |
15 | 14 | nnrecred 11066 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑖) ∈ ℝ) |
16 | 2, 15 | fsumrecl 14465 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) ∈ ℝ) |
17 | 16 | resqcld 13035 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) ∈ ℝ) |
18 | | nnrp 11842 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
19 | 18 | relogcld 24369 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(log‘𝑁) ∈
ℝ) |
20 | | peano2re 10209 |
. . . . 5
⊢
((log‘𝑁)
∈ ℝ → ((log‘𝑁) + 1) ∈ ℝ) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ℕ →
((log‘𝑁) + 1) ∈
ℝ) |
22 | 21 | resqcld 13035 |
. . 3
⊢ (𝑁 ∈ ℕ →
(((log‘𝑁) +
1)↑2) ∈ ℝ) |
23 | 10 | recnd 10068 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ∈ ℂ) |
24 | 23 | 2timesd 11275 |
. . . 4
⊢ (𝑁 ∈ ℕ → (2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) + Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛))) |
25 | | fzfid 12772 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1...𝑛) ∈ Fin) |
26 | | elfznn 12370 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...𝑛) → 𝑖 ∈ ℕ) |
27 | 26 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℕ) |
28 | 27 | nnrecred 11066 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → (1 / 𝑖) ∈ ℝ) |
29 | 25, 28 | fsumrecl 14465 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ∈ ℝ) |
30 | 29, 6 | nndivred 11069 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) ∈ ℝ) |
31 | 2, 30 | fsumrecl 14465 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) ∈ ℝ) |
32 | | fzfid 12772 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1...(𝑛 − 1)) ∈ Fin) |
33 | | elfznn 12370 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑛 − 1)) → 𝑖 ∈ ℕ) |
34 | 33 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...(𝑛 − 1))) → 𝑖 ∈ ℕ) |
35 | 34 | nnrecred 11066 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...(𝑛 − 1))) → (1 / 𝑖) ∈ ℝ) |
36 | 32, 35 | fsumrecl 14465 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ∈ ℝ) |
37 | 36, 6 | nndivred 11069 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ∈ ℝ) |
38 | 2, 37 | fsumrecl 14465 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ∈ ℝ) |
39 | 6 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ) |
40 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
41 | | npcan 10290 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
42 | 39, 40, 41 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 − 1) + 1) = 𝑛) |
43 | 42 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (log‘((𝑛 − 1) + 1)) = (log‘𝑛)) |
44 | 43 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘((𝑛 − 1) + 1))) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛))) |
45 | | nnm1nn0 11334 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
46 | | harmonicbnd3 24734 |
. . . . . . . . . . . . 13
⊢ ((𝑛 − 1) ∈
ℕ0 → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘((𝑛 − 1) + 1))) ∈
(0[,]γ)) |
47 | 6, 45, 46 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘((𝑛 − 1) + 1))) ∈
(0[,]γ)) |
48 | 44, 47 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛)) ∈ (0[,]γ)) |
49 | | 0re 10040 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
50 | | emre 24732 |
. . . . . . . . . . . . 13
⊢ γ
∈ ℝ |
51 | 49, 50 | elicc2i 12239 |
. . . . . . . . . . . 12
⊢
((Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) − (log‘𝑛)) ∈ (0[,]γ) ↔
((Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) − (log‘𝑛)) ∈ ℝ ∧ 0 ≤
(Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) − (log‘𝑛)) ∧ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛)) ≤ γ)) |
52 | 51 | simp2bi 1077 |
. . . . . . . . . . 11
⊢
((Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) − (log‘𝑛)) ∈ (0[,]γ) → 0
≤ (Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) − (log‘𝑛))) |
53 | 48, 52 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 0 ≤ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛))) |
54 | 36, 8 | subge0d 10617 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛)) ↔ (log‘𝑛) ≤ Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) |
55 | 53, 54 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (log‘𝑛) ≤ Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) |
56 | 8, 36, 7, 55 | lediv1dd 11930 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((log‘𝑛) / 𝑛) ≤ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
57 | 27 | nnrpd 11870 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℝ+) |
58 | 57 | rpreccld 11882 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → (1 / 𝑖) ∈
ℝ+) |
59 | 58 | rpge0d 11876 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → 0 ≤ (1 / 𝑖)) |
60 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ) |
61 | 60 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℤ) |
62 | | peano2zm 11420 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (𝑛 − 1) ∈
ℤ) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ ℤ) |
64 | 6 | nnred 11035 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ) |
65 | 64 | lem1d 10957 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ≤ 𝑛) |
66 | | eluz2 11693 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘(𝑛 − 1)) ↔ ((𝑛 − 1) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ (𝑛 − 1) ≤ 𝑛)) |
67 | 63, 61, 65, 66 | syl3anbrc 1246 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (ℤ≥‘(𝑛 − 1))) |
68 | | fzss2 12381 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘(𝑛 − 1)) → (1...(𝑛 − 1)) ⊆ (1...𝑛)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1...(𝑛 − 1)) ⊆ (1...𝑛)) |
70 | 25, 28, 59, 69 | fsumless 14528 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ≤ Σ𝑖 ∈ (1...𝑛)(1 / 𝑖)) |
71 | 6 | nngt0d 11064 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 0 < 𝑛) |
72 | | lediv1 10888 |
. . . . . . . . . 10
⊢
((Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) ∈ ℝ ∧
Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ∈ ℝ ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ≤ Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ↔ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛))) |
73 | 36, 29, 64, 71, 72 | syl112anc 1330 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ≤ Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ↔ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛))) |
74 | 70, 73 | mpbid 222 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
75 | 9, 37, 30, 56, 74 | letrd 10194 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((log‘𝑛) / 𝑛) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
76 | 2, 9, 30, 75 | fsumle 14531 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
77 | 2, 9, 37, 56 | fsumle 14531 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
78 | 10, 10, 31, 38, 76, 77 | le2addd 10646 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) + Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛)) ≤ (Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) + Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛))) |
79 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1)) |
80 | 79 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (1...(𝑚 − 1)) = (1...(𝑛 − 1))) |
81 | 80 | sumeq1d 14431 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) |
82 | 81, 81 | jca 554 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ∧ Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) |
83 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1)) |
84 | 83 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (1...(𝑚 − 1)) = (1...((𝑛 + 1) − 1))) |
85 | 84 | sumeq1d 14431 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)) |
86 | 85, 85 | jca 554 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) ∧ Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖))) |
87 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
88 | | 1m1e0 11089 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
89 | 87, 88 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
90 | 89 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (1...(𝑚 − 1)) =
(1...0)) |
91 | | fz10 12362 |
. . . . . . . . . . . 12
⊢ (1...0) =
∅ |
92 | 90, 91 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (1...(𝑚 − 1)) =
∅) |
93 | 92 | sumeq1d 14431 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ ∅ (1 / 𝑖)) |
94 | | sum0 14452 |
. . . . . . . . . 10
⊢
Σ𝑖 ∈
∅ (1 / 𝑖) =
0 |
95 | 93, 94 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑚 = 1 → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = 0) |
96 | 95, 95 | jca 554 |
. . . . . . . 8
⊢ (𝑚 = 1 → (Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = 0 ∧ Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = 0)) |
97 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑁 + 1) → (𝑚 − 1) = ((𝑁 + 1) − 1)) |
98 | 97 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑁 + 1) → (1...(𝑚 − 1)) = (1...((𝑁 + 1) − 1))) |
99 | 98 | sumeq1d 14431 |
. . . . . . . . 9
⊢ (𝑚 = (𝑁 + 1) → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) |
100 | 99, 99 | jca 554 |
. . . . . . . 8
⊢ (𝑚 = (𝑁 + 1) → (Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖) ∧ Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖))) |
101 | | peano2nn 11032 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
102 | 101, 5 | syl6eleq 2711 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
(ℤ≥‘1)) |
103 | | fzfid 12772 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → (1...(𝑚 − 1)) ∈ Fin) |
104 | | elfznn 12370 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...(𝑚 − 1)) → 𝑖 ∈ ℕ) |
105 | 104 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) ∧ 𝑖 ∈ (1...(𝑚 − 1))) → 𝑖 ∈ ℕ) |
106 | 105 | nnrecred 11066 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) ∧ 𝑖 ∈ (1...(𝑚 − 1))) → (1 / 𝑖) ∈ ℝ) |
107 | 103, 106 | fsumrecl 14465 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) ∈ ℝ) |
108 | 107 | recnd 10068 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) ∈ ℂ) |
109 | 82, 86, 96, 100, 102, 108, 108 | fsumparts 14538 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1..^(𝑁 + 1))(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) = (((Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) − (0 · 0)) −
Σ𝑛 ∈ (1..^(𝑁 + 1))((Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) · Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)))) |
110 | | nnz 11399 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
111 | | fzval3 12536 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(1...𝑁) = (1..^(𝑁 + 1))) |
112 | 110, 111 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(1...𝑁) = (1..^(𝑁 + 1))) |
113 | 112 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(1..^(𝑁 + 1)) = (1...𝑁)) |
114 | | pncan 10287 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
115 | 39, 40, 114 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 + 1) − 1) = 𝑛) |
116 | 115 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1...((𝑛 + 1) − 1)) = (1...𝑛)) |
117 | 116 | sumeq1d 14431 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...𝑛)(1 / 𝑖)) |
118 | 28 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → (1 / 𝑖) ∈ ℂ) |
119 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (1 / 𝑖) = (1 / 𝑛)) |
120 | 4, 118, 119 | fsumm1 14480 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) + (1 / 𝑛))) |
121 | 117, 120 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) + (1 / 𝑛))) |
122 | 121 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) = ((Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) + (1 / 𝑛)) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) |
123 | 36 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ∈ ℂ) |
124 | 6 | nnrecred 11066 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1 / 𝑛) ∈ ℝ) |
125 | 124 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1 / 𝑛) ∈ ℂ) |
126 | 123, 125 | pncan2d 10394 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) + (1 / 𝑛)) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) = (1 / 𝑛)) |
127 | 122, 126 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) = (1 / 𝑛)) |
128 | 127 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (1 / 𝑛))) |
129 | 6 | nnne0d 11065 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ≠ 0) |
130 | 123, 39, 129 | divrecd 10804 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (1 / 𝑛))) |
131 | 128, 130 | eqtr4d 2659 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
132 | 113, 131 | sumeq12rdv 14438 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1..^(𝑁 + 1))(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) = Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
133 | | nncn 11028 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
134 | | pncan 10287 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
135 | 133, 40, 134 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
136 | 135 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(1...((𝑁 + 1) − 1)) =
(1...𝑁)) |
137 | 136 | sumeq1d 14431 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) = Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)) |
138 | 137, 137 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) · Σ𝑖 ∈ (1...𝑁)(1 / 𝑖))) |
139 | 16 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) ∈ ℂ) |
140 | 139 | sqvald 13005 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) · Σ𝑖 ∈ (1...𝑁)(1 / 𝑖))) |
141 | 138, 140 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
142 | | 0cn 10032 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
143 | 142 | mul01i 10226 |
. . . . . . . . . . 11
⊢ (0
· 0) = 0 |
144 | 143 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (0
· 0) = 0) |
145 | 141, 144 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) − (0 · 0)) = ((Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) − 0)) |
146 | 139 | sqcld 13006 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) ∈ ℂ) |
147 | 146 | subid1d 10381 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((Σ𝑖 ∈
(1...𝑁)(1 / 𝑖)↑2) − 0) =
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
148 | 145, 147 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) − (0 · 0)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
149 | 127, 117 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) · Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)) = ((1 / 𝑛) · Σ𝑖 ∈ (1...𝑛)(1 / 𝑖))) |
150 | 29 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ∈ ℂ) |
151 | 150, 39, 129 | divrec2d 10805 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) = ((1 / 𝑛) · Σ𝑖 ∈ (1...𝑛)(1 / 𝑖))) |
152 | 149, 151 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) · Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)) = (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
153 | 113, 152 | sumeq12rdv 14438 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1..^(𝑁 + 1))((Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) · Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)) = Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
154 | 148, 153 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(((Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) − (0 · 0)) −
Σ𝑛 ∈ (1..^(𝑁 + 1))((Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) · Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖))) = ((Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) − Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛))) |
155 | 109, 132,
154 | 3eqtr3rd 2665 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((Σ𝑖 ∈
(1...𝑁)(1 / 𝑖)↑2) − Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) = Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
156 | 31 | recnd 10068 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) ∈ ℂ) |
157 | 38 | recnd 10068 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ∈ ℂ) |
158 | 146, 156,
157 | subaddd 10410 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(((Σ𝑖 ∈
(1...𝑁)(1 / 𝑖)↑2) − Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) = Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ↔ (Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) + Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2))) |
159 | 155, 158 | mpbid 222 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) + Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
160 | 78, 159 | breqtrd 4679 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) + Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛)) ≤ (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
161 | 24, 160 | eqbrtrd 4675 |
. . 3
⊢ (𝑁 ∈ ℕ → (2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) ≤ (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
162 | | flid 12609 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(⌊‘𝑁) = 𝑁) |
163 | 110, 162 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(⌊‘𝑁) = 𝑁) |
164 | 163 | oveq2d 6666 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(1...(⌊‘𝑁)) =
(1...𝑁)) |
165 | 164 | sumeq1d 14431 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈
(1...(⌊‘𝑁))(1 /
𝑖) = Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)) |
166 | | nnre 11027 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
167 | | nnge1 11046 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) |
168 | | harmonicubnd 24736 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 1 ≤
𝑁) → Σ𝑖 ∈
(1...(⌊‘𝑁))(1 /
𝑖) ≤ ((log‘𝑁) + 1)) |
169 | 166, 167,
168 | syl2anc 693 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈
(1...(⌊‘𝑁))(1 /
𝑖) ≤ ((log‘𝑁) + 1)) |
170 | 165, 169 | eqbrtrrd 4677 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) ≤ ((log‘𝑁) + 1)) |
171 | 14 | nnrpd 11870 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → 𝑖 ∈ ℝ+) |
172 | 171 | rpreccld 11882 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑖) ∈
ℝ+) |
173 | 172 | rpge0d 11876 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ (1 / 𝑖)) |
174 | 2, 15, 173 | fsumge0 14527 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 ≤
Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)) |
175 | 49 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
176 | | log1 24332 |
. . . . . . 7
⊢
(log‘1) = 0 |
177 | | 1rp 11836 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
178 | | logleb 24349 |
. . . . . . . . 9
⊢ ((1
∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (1 ≤
𝑁 ↔ (log‘1) ≤
(log‘𝑁))) |
179 | 177, 18, 178 | sylancr 695 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1 ≤
𝑁 ↔ (log‘1) ≤
(log‘𝑁))) |
180 | 167, 179 | mpbid 222 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(log‘1) ≤ (log‘𝑁)) |
181 | 176, 180 | syl5eqbrr 4689 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
(log‘𝑁)) |
182 | 19 | lep1d 10955 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘𝑁) ≤
((log‘𝑁) +
1)) |
183 | 175, 19, 21, 181, 182 | letrd 10194 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 ≤
((log‘𝑁) +
1)) |
184 | 16, 21, 174, 183 | le2sqd 13044 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) ≤ ((log‘𝑁) + 1) ↔ (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) ≤ (((log‘𝑁) + 1)↑2))) |
185 | 170, 184 | mpbid 222 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) ≤ (((log‘𝑁) + 1)↑2)) |
186 | 12, 17, 22, 161, 185 | letrd 10194 |
. 2
⊢ (𝑁 ∈ ℕ → (2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) ≤ (((log‘𝑁) + 1)↑2)) |
187 | 1 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
188 | | 2pos 11112 |
. . . 4
⊢ 0 <
2 |
189 | 188 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ → 0 <
2) |
190 | | lemuldiv2 10904 |
. . 3
⊢
((Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛) ∈ ℝ ∧ (((log‘𝑁) + 1)↑2) ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛)) ≤ (((log‘𝑁) + 1)↑2) ↔ Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ ((((log‘𝑁) + 1)↑2) / 2))) |
191 | 10, 22, 187, 189, 190 | syl112anc 1330 |
. 2
⊢ (𝑁 ∈ ℕ → ((2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) ≤ (((log‘𝑁) + 1)↑2) ↔ Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ ((((log‘𝑁) + 1)↑2) / 2))) |
192 | 186, 191 | mpbid 222 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ ((((log‘𝑁) + 1)↑2) / 2)) |