Step | Hyp | Ref
| Expression |
1 | | 2re 12054 |
. . . 4
⊢ 2 ∈
ℝ |
2 | | fzfid 13700 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(1...𝑁) ∈
Fin) |
3 | | elfzuz 13259 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈
(ℤ≥‘1)) |
4 | 3 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈
(ℤ≥‘1)) |
5 | | nnuz 12628 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
6 | 4, 5 | eleqtrrdi 2847 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ) |
7 | 6 | nnrpd 12777 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ+) |
8 | 7 | relogcld 25785 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (log‘𝑛) ∈ ℝ) |
9 | 8, 6 | nndivred 12034 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((log‘𝑛) / 𝑛) ∈ ℝ) |
10 | 2, 9 | fsumrecl 15453 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ∈ ℝ) |
11 | | remulcl 10963 |
. . . 4
⊢ ((2
∈ ℝ ∧ Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ∈ ℝ) → (2 ·
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛)) ∈ ℝ) |
12 | 1, 10, 11 | sylancr 587 |
. . 3
⊢ (𝑁 ∈ ℕ → (2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) ∈ ℝ) |
13 | | elfznn 13292 |
. . . . . . 7
⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ) |
14 | 13 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → 𝑖 ∈ ℕ) |
15 | 14 | nnrecred 12031 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑖) ∈ ℝ) |
16 | 2, 15 | fsumrecl 15453 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) ∈ ℝ) |
17 | 16 | resqcld 13972 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) ∈ ℝ) |
18 | | nnrp 12748 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
19 | 18 | relogcld 25785 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(log‘𝑁) ∈
ℝ) |
20 | | peano2re 11155 |
. . . . 5
⊢
((log‘𝑁)
∈ ℝ → ((log‘𝑁) + 1) ∈ ℝ) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ℕ →
((log‘𝑁) + 1) ∈
ℝ) |
22 | 21 | resqcld 13972 |
. . 3
⊢ (𝑁 ∈ ℕ →
(((log‘𝑁) +
1)↑2) ∈ ℝ) |
23 | 10 | recnd 11010 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ∈ ℂ) |
24 | 23 | 2timesd 12223 |
. . . 4
⊢ (𝑁 ∈ ℕ → (2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) + Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛))) |
25 | | fzfid 13700 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1...𝑛) ∈ Fin) |
26 | | elfznn 13292 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...𝑛) → 𝑖 ∈ ℕ) |
27 | 26 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℕ) |
28 | 27 | nnrecred 12031 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → (1 / 𝑖) ∈ ℝ) |
29 | 25, 28 | fsumrecl 15453 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ∈ ℝ) |
30 | 29, 6 | nndivred 12034 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) ∈ ℝ) |
31 | 2, 30 | fsumrecl 15453 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) ∈ ℝ) |
32 | | fzfid 13700 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1...(𝑛 − 1)) ∈ Fin) |
33 | | elfznn 13292 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...(𝑛 − 1)) → 𝑖 ∈ ℕ) |
34 | 33 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...(𝑛 − 1))) → 𝑖 ∈ ℕ) |
35 | 34 | nnrecred 12031 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...(𝑛 − 1))) → (1 / 𝑖) ∈ ℝ) |
36 | 32, 35 | fsumrecl 15453 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ∈ ℝ) |
37 | 36, 6 | nndivred 12034 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ∈ ℝ) |
38 | 2, 37 | fsumrecl 15453 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ∈ ℝ) |
39 | 6 | nncnd 11996 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ) |
40 | | ax-1cn 10936 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
41 | | npcan 11237 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
42 | 39, 40, 41 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 − 1) + 1) = 𝑛) |
43 | 42 | fveq2d 6785 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (log‘((𝑛 − 1) + 1)) = (log‘𝑛)) |
44 | 43 | oveq2d 7298 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘((𝑛 − 1) + 1))) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛))) |
45 | | nnm1nn0 12281 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
46 | | harmonicbnd3 26164 |
. . . . . . . . . . . . 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 2837 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛)) ∈ (0[,]γ)) |
49 | | 0re 10984 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
50 | | emre 26162 |
. . . . . . . . . . . . 13
⊢ γ
∈ ℝ |
51 | 49, 50 | elicc2i 13152 |
. . . . . . . . . . . 12
⊢
((Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) − (log‘𝑛)) ∈ (0[,]γ) ↔
((Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) − (log‘𝑛)) ∈ ℝ ∧ 0 ≤
(Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) − (log‘𝑛)) ∧ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛)) ≤ γ)) |
52 | 51 | simp2bi 1145 |
. . . . . . . . . . 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 11572 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (0 ≤ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) − (log‘𝑛)) ↔ (log‘𝑛) ≤ Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) |
55 | 53, 54 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (log‘𝑛) ≤ Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) |
56 | 8, 36, 7, 55 | lediv1dd 12837 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((log‘𝑛) / 𝑛) ≤ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
57 | 27 | nnrpd 12777 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℝ+) |
58 | 57 | rpreccld 12789 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → (1 / 𝑖) ∈
ℝ+) |
59 | 58 | rpge0d 12783 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → 0 ≤ (1 / 𝑖)) |
60 | | elfzelz 13263 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ) |
61 | 60 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℤ) |
62 | | peano2zm 12370 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (𝑛 − 1) ∈
ℤ) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ ℤ) |
64 | 6 | nnred 11995 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ) |
65 | 64 | lem1d 11915 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ≤ 𝑛) |
66 | | eluz2 12595 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘(𝑛 − 1)) ↔ ((𝑛 − 1) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ (𝑛 − 1) ≤ 𝑛)) |
67 | 63, 61, 65, 66 | syl3anbrc 1342 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (ℤ≥‘(𝑛 − 1))) |
68 | | fzss2 13303 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘(𝑛 − 1)) → (1...(𝑛 − 1)) ⊆ (1...𝑛)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1...(𝑛 − 1)) ⊆ (1...𝑛)) |
70 | 25, 28, 59, 69 | fsumless 15515 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ≤ Σ𝑖 ∈ (1...𝑛)(1 / 𝑖)) |
71 | 6 | nngt0d 12029 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 0 < 𝑛) |
72 | | lediv1 11847 |
. . . . . . . . . 10
⊢
((Σ𝑖 ∈
(1...(𝑛 − 1))(1 /
𝑖) ∈ ℝ ∧
Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ∈ ℝ ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ≤ Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ↔ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛))) |
73 | 36, 29, 64, 71, 72 | syl112anc 1373 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ≤ Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ↔ (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛))) |
74 | 70, 73 | mpbid 231 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
75 | 9, 37, 30, 56, 74 | letrd 11139 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((log‘𝑛) / 𝑛) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
76 | 2, 9, 30, 75 | fsumle 15518 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
77 | 2, 9, 37, 56 | fsumle 15518 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
78 | 10, 10, 31, 38, 76, 77 | le2addd 11601 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) + Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛)) ≤ (Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) + Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛))) |
79 | | oveq1 7289 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1)) |
80 | 79 | oveq2d 7298 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (1...(𝑚 − 1)) = (1...(𝑛 − 1))) |
81 | 80 | sumeq1d 15420 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) |
82 | 81, 81 | jca 512 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ∧ Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) |
83 | | oveq1 7289 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1)) |
84 | 83 | oveq2d 7298 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (1...(𝑚 − 1)) = (1...((𝑛 + 1) − 1))) |
85 | 84 | sumeq1d 15420 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)) |
86 | 85, 85 | jca 512 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) ∧ Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖))) |
87 | | oveq1 7289 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
88 | | 1m1e0 12052 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
89 | 87, 88 | eqtrdi 2791 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
90 | 89 | oveq2d 7298 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (1...(𝑚 − 1)) =
(1...0)) |
91 | | fz10 13284 |
. . . . . . . . . . . 12
⊢ (1...0) =
∅ |
92 | 90, 91 | eqtrdi 2791 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (1...(𝑚 − 1)) =
∅) |
93 | 92 | sumeq1d 15420 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ ∅ (1 / 𝑖)) |
94 | | sum0 15440 |
. . . . . . . . . 10
⊢
Σ𝑖 ∈
∅ (1 / 𝑖) =
0 |
95 | 93, 94 | eqtrdi 2791 |
. . . . . . . . 9
⊢ (𝑚 = 1 → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = 0) |
96 | 95, 95 | jca 512 |
. . . . . . . 8
⊢ (𝑚 = 1 → (Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = 0 ∧ Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = 0)) |
97 | | oveq1 7289 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑁 + 1) → (𝑚 − 1) = ((𝑁 + 1) − 1)) |
98 | 97 | oveq2d 7298 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑁 + 1) → (1...(𝑚 − 1)) = (1...((𝑁 + 1) − 1))) |
99 | 98 | sumeq1d 15420 |
. . . . . . . . 9
⊢ (𝑚 = (𝑁 + 1) → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) |
100 | 99, 99 | jca 512 |
. . . . . . . 8
⊢ (𝑚 = (𝑁 + 1) → (Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖) ∧ Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖))) |
101 | | peano2nn 11992 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
102 | 101, 5 | eleqtrdi 2846 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
(ℤ≥‘1)) |
103 | | fzfid 13700 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → (1...(𝑚 − 1)) ∈ Fin) |
104 | | elfznn 13292 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...(𝑚 − 1)) → 𝑖 ∈ ℕ) |
105 | 104 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) ∧ 𝑖 ∈ (1...(𝑚 − 1))) → 𝑖 ∈ ℕ) |
106 | 105 | nnrecred 12031 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) ∧ 𝑖 ∈ (1...(𝑚 − 1))) → (1 / 𝑖) ∈ ℝ) |
107 | 103, 106 | fsumrecl 15453 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) ∈ ℝ) |
108 | 107 | recnd 11010 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → Σ𝑖 ∈ (1...(𝑚 − 1))(1 / 𝑖) ∈ ℂ) |
109 | 82, 86, 96, 100, 102, 108, 108 | fsumparts 15525 |
. . . . . . 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 12349 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
111 | | fzval3 13463 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(1...𝑁) = (1..^(𝑁 + 1))) |
112 | 110, 111 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(1...𝑁) = (1..^(𝑁 + 1))) |
113 | 112 | eqcomd 2741 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(1..^(𝑁 + 1)) = (1...𝑁)) |
114 | 36 | recnd 11010 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) ∈ ℂ) |
115 | 6 | nnrecred 12031 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1 / 𝑛) ∈ ℝ) |
116 | 115 | recnd 11010 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1 / 𝑛) ∈ ℂ) |
117 | | pncan 11234 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
118 | 39, 40, 117 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 + 1) − 1) = 𝑛) |
119 | 118 | oveq2d 7298 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (1...((𝑛 + 1) − 1)) = (1...𝑛)) |
120 | 119 | sumeq1d 15420 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) = Σ𝑖 ∈ (1...𝑛)(1 / 𝑖)) |
121 | 28 | recnd 11010 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑖 ∈ (1...𝑛)) → (1 / 𝑖) ∈ ℂ) |
122 | | oveq2 7290 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → (1 / 𝑖) = (1 / 𝑛)) |
123 | 4, 121, 122 | fsumm1 15470 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) + (1 / 𝑛))) |
124 | 120, 123 | eqtrd 2775 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) + (1 / 𝑛))) |
125 | 114, 116,
124 | mvrladdd 11395 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) = (1 / 𝑛)) |
126 | 125 | oveq2d 7298 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (1 / 𝑛))) |
127 | 6 | nnne0d 12030 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ≠ 0) |
128 | 114, 39, 127 | divrecd 11761 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (1 / 𝑛))) |
129 | 126, 128 | eqtr4d 2778 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) = (Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
130 | 113, 129 | sumeq12rdv 15426 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1..^(𝑁 + 1))(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) · (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖))) = Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
131 | | nncn 11988 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
132 | | pncan 11234 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
133 | 131, 40, 132 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
134 | 133 | oveq2d 7298 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(1...((𝑁 + 1) − 1)) =
(1...𝑁)) |
135 | 134 | sumeq1d 15420 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) = Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)) |
136 | 135, 135 | oveq12d 7300 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) · Σ𝑖 ∈ (1...𝑁)(1 / 𝑖))) |
137 | 16 | recnd 11010 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) ∈ ℂ) |
138 | 137 | sqvald 13868 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) · Σ𝑖 ∈ (1...𝑁)(1 / 𝑖))) |
139 | 136, 138 | eqtr4d 2778 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
140 | | 0cn 10974 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
141 | 140 | mul01i 11172 |
. . . . . . . . . . 11
⊢ (0
· 0) = 0 |
142 | 141 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (0
· 0) = 0) |
143 | 139, 142 | oveq12d 7300 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) − (0 · 0)) = ((Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) − 0)) |
144 | 137 | sqcld 13869 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) ∈ ℂ) |
145 | 144 | subid1d 11328 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((Σ𝑖 ∈
(1...𝑁)(1 / 𝑖)↑2) − 0) =
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
146 | 143, 145 | eqtrd 2775 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((Σ𝑖 ∈
(1...((𝑁 + 1) − 1))(1
/ 𝑖) · Σ𝑖 ∈ (1...((𝑁 + 1) − 1))(1 / 𝑖)) − (0 · 0)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
147 | 125, 120 | oveq12d 7300 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) · Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)) = ((1 / 𝑛) · Σ𝑖 ∈ (1...𝑛)(1 / 𝑖))) |
148 | 29 | recnd 11010 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) ∈ ℂ) |
149 | 148, 39, 127 | divrec2d 11762 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) = ((1 / 𝑛) · Σ𝑖 ∈ (1...𝑛)(1 / 𝑖))) |
150 | 147, 149 | eqtr4d 2778 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → ((Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) · Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)) = (Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
151 | 113, 150 | sumeq12rdv 15426 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1..^(𝑁 + 1))((Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖) − Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖)) · Σ𝑖 ∈ (1...((𝑛 + 1) − 1))(1 / 𝑖)) = Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) |
152 | 146, 151 | oveq12d 7300 |
. . . . . . 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 / 𝑖) / 𝑛))) |
153 | 109, 130,
152 | 3eqtr3rd 2784 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((Σ𝑖 ∈
(1...𝑁)(1 / 𝑖)↑2) − Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) = Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) |
154 | 31 | recnd 11010 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) ∈ ℂ) |
155 | 38 | recnd 11010 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ∈ ℂ) |
156 | 144, 154,
155 | subaddd 11357 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(((Σ𝑖 ∈
(1...𝑁)(1 / 𝑖)↑2) − Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛)) = Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛) ↔ (Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) + Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2))) |
157 | 153, 156 | mpbid 231 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...𝑛)(1 / 𝑖) / 𝑛) + Σ𝑛 ∈ (1...𝑁)(Σ𝑖 ∈ (1...(𝑛 − 1))(1 / 𝑖) / 𝑛)) = (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
158 | 78, 157 | breqtrd 5099 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) + Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛)) ≤ (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
159 | 24, 158 | eqbrtrd 5095 |
. . 3
⊢ (𝑁 ∈ ℕ → (2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) ≤ (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2)) |
160 | | flid 13535 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(⌊‘𝑁) = 𝑁) |
161 | 110, 160 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(⌊‘𝑁) = 𝑁) |
162 | 161 | oveq2d 7298 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(1...(⌊‘𝑁)) =
(1...𝑁)) |
163 | 162 | sumeq1d 15420 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈
(1...(⌊‘𝑁))(1 /
𝑖) = Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)) |
164 | | nnre 11987 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
165 | | nnge1 12008 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) |
166 | | harmonicubnd 26166 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 1 ≤
𝑁) → Σ𝑖 ∈
(1...(⌊‘𝑁))(1 /
𝑖) ≤ ((log‘𝑁) + 1)) |
167 | 164, 165,
166 | syl2anc 584 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈
(1...(⌊‘𝑁))(1 /
𝑖) ≤ ((log‘𝑁) + 1)) |
168 | 163, 167 | eqbrtrrd 5097 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) ≤ ((log‘𝑁) + 1)) |
169 | 14 | nnrpd 12777 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → 𝑖 ∈ ℝ+) |
170 | 169 | rpreccld 12789 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑖) ∈
ℝ+) |
171 | 170 | rpge0d 12783 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ (1 / 𝑖)) |
172 | 2, 15, 171 | fsumge0 15514 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 ≤
Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)) |
173 | 49 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
174 | | log1 25748 |
. . . . . . 7
⊢
(log‘1) = 0 |
175 | | 1rp 12741 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
176 | | logleb 25765 |
. . . . . . . . 9
⊢ ((1
∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (1 ≤
𝑁 ↔ (log‘1) ≤
(log‘𝑁))) |
177 | 175, 18, 176 | sylancr 587 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1 ≤
𝑁 ↔ (log‘1) ≤
(log‘𝑁))) |
178 | 165, 177 | mpbid 231 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(log‘1) ≤ (log‘𝑁)) |
179 | 174, 178 | eqbrtrrid 5109 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
(log‘𝑁)) |
180 | 19 | lep1d 11913 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘𝑁) ≤
((log‘𝑁) +
1)) |
181 | 173, 19, 21, 179, 180 | letrd 11139 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 ≤
((log‘𝑁) +
1)) |
182 | 16, 21, 172, 181 | le2sqd 13981 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖) ≤ ((log‘𝑁) + 1) ↔ (Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) ≤ (((log‘𝑁) + 1)↑2))) |
183 | 168, 182 | mpbid 231 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑖 ∈ (1...𝑁)(1 / 𝑖)↑2) ≤ (((log‘𝑁) + 1)↑2)) |
184 | 12, 17, 22, 159, 183 | letrd 11139 |
. 2
⊢ (𝑁 ∈ ℕ → (2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) ≤ (((log‘𝑁) + 1)↑2)) |
185 | 1 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
186 | | 2pos 12083 |
. . . 4
⊢ 0 <
2 |
187 | 186 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ → 0 <
2) |
188 | | lemuldiv2 11863 |
. . 3
⊢
((Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛) ∈ ℝ ∧ (((log‘𝑁) + 1)↑2) ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛)) ≤ (((log‘𝑁) + 1)↑2) ↔ Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ ((((log‘𝑁) + 1)↑2) / 2))) |
189 | 10, 22, 185, 187, 188 | syl112anc 1373 |
. 2
⊢ (𝑁 ∈ ℕ → ((2
· Σ𝑛 ∈
(1...𝑁)((log‘𝑛) / 𝑛)) ≤ (((log‘𝑁) + 1)↑2) ↔ Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ ((((log‘𝑁) + 1)↑2) / 2))) |
190 | 184, 189 | mpbid 231 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ ((((log‘𝑁) + 1)↑2) / 2)) |