Metamath Proof Explorer

Theorem logdivbnd

Description: A bound on a sum of logs, used in pntlemk . This is not as precise as logdivsum in its asymptotic behavior, but it is valid for all N and does not require a limit value. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Assertion logdivbnd ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( ( ( ( log ‘ 𝑁 ) + 1 ) ↑ 2 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
3 elfzuz ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
4 3 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 4 5 eleqtrrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ℕ )
7 6 nnrpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ℝ+ )
8 7 relogcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
9 8 6 nndivred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
10 2 9 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
11 remulcl ⊢ ( ( 2 ∈ ℝ ∧ Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) → ( 2 · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
12 1 10 11 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 2 · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
13 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → 𝑖 ∈ ℕ )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ℕ )
15 14 nnrecred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑖 ) ∈ ℝ )
16 2 15 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ∈ ℝ )
17 16 resqcld ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) ∈ ℝ )
18 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
19 18 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ 𝑁 ) ∈ ℝ )
20 peano2re ⊢ ( ( log ‘ 𝑁 ) ∈ ℝ → ( ( log ‘ 𝑁 ) + 1 ) ∈ ℝ )
21 19 20 syl ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ 𝑁 ) + 1 ) ∈ ℝ )
22 21 resqcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( log ‘ 𝑁 ) + 1 ) ↑ 2 ) ∈ ℝ )
23 10 recnd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
24 23 2timesd ⊢ ( 𝑁 ∈ ℕ → ( 2 · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
25 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 1 ... 𝑛 ) ∈ Fin )
26 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑛 ) → 𝑖 ∈ ℕ )
27 26 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → 𝑖 ∈ ℕ )
28 27 nnrecred ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( 1 / 𝑖 ) ∈ ℝ )
29 25 28 fsumrecl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) ∈ ℝ )
30 29 6 nndivred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) ∈ ℝ )
31 2 30 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) ∈ ℝ )
32 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 1 ... ( 𝑛 − 1 ) ) ∈ Fin )
33 elfznn ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) → 𝑖 ∈ ℕ )
34 33 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ) → 𝑖 ∈ ℕ )
35 34 nnrecred ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ) → ( 1 / 𝑖 ) ∈ ℝ )
36 32 35 fsumrecl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ∈ ℝ )
37 36 6 nndivred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ∈ ℝ )
38 2 37 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ∈ ℝ )
39 6 nncnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ℂ )
40 ax-1cn ⊢ 1 ∈ ℂ
41 npcan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
42 39 40 41 sylancl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
43 42 fveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( log ‘ 𝑛 ) )
44 43 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) = ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) )
45 nnm1nn0 ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
46 harmonicbnd3 ⊢ ( ( 𝑛 − 1 ) ∈ ℕ0 → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) ∈ ( 0 [,] γ ) )
47 6 45 46 3syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) ∈ ( 0 [,] γ ) )
48 44 47 eqeltrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) ∈ ( 0 [,] γ ) )
49 0re ⊢ 0 ∈ ℝ
50 emre ⊢ γ ∈ ℝ
51 49 50 elicc2i ⊢ ( ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) ∈ ( 0 [,] γ ) ↔ ( ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) ∈ ℝ ∧ 0 ≤ ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) ∧ ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) ≤ γ ) )
52 51 simp2bi ⊢ ( ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) ∈ ( 0 [,] γ ) → 0 ≤ ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) )
53 48 52 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) )
54 36 8 subge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 0 ≤ ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) − ( log ‘ 𝑛 ) ) ↔ ( log ‘ 𝑛 ) ≤ Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) )
55 53 54 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ 𝑛 ) ≤ Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) )
56 8 36 7 55 lediv1dd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) )
57 27 nnrpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → 𝑖 ∈ ℝ+ )
58 57 rpreccld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( 1 / 𝑖 ) ∈ ℝ+ )
59 58 rpge0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → 0 ≤ ( 1 / 𝑖 ) )
60 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℤ )
61 60 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ℤ )
62 peano2zm ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 − 1 ) ∈ ℤ )
63 61 62 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 − 1 ) ∈ ℤ )
64 6 nnred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ℝ )
65 64 lem1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 − 1 ) ≤ 𝑛 )
66 eluz2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) ↔ ( ( 𝑛 − 1 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ ( 𝑛 − 1 ) ≤ 𝑛 ) )
67 63 61 65 66 syl3anbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) )
68 fzss2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) → ( 1 ... ( 𝑛 − 1 ) ) ⊆ ( 1 ... 𝑛 ) )
69 67 68 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 1 ... ( 𝑛 − 1 ) ) ⊆ ( 1 ... 𝑛 ) )
70 25 28 59 69 fsumless ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ≤ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) )
71 6 nngt0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 0 < 𝑛 )
72 lediv1 ⊢ ( ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ∈ ℝ ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) ∈ ℝ ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ≤ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) ↔ ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) ) )
73 36 29 64 71 72 syl112anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ≤ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) ↔ ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) ) )
74 70 73 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) )
75 9 37 30 56 74 letrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) )
76 2 9 30 75 fsumle ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) )
77 2 9 37 56 fsumle ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) )
78 10 10 31 38 76 77 le2addd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ) )
79 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 − 1 ) = ( 𝑛 − 1 ) )
80 79 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 1 ... ( 𝑚 − 1 ) ) = ( 1 ... ( 𝑛 − 1 ) ) )
81 80 sumeq1d ⊢ ( 𝑚 = 𝑛 → Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) )
82 81 81 jca ⊢ ( 𝑚 = 𝑛 → ( Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ∧ Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) )
83 oveq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 − 1 ) = ( ( 𝑛 + 1 ) − 1 ) )
84 83 oveq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 1 ... ( 𝑚 − 1 ) ) = ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) )
85 84 sumeq1d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) )
86 85 85 jca ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ∧ Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) )
87 oveq1 ⊢ ( 𝑚 = 1 → ( 𝑚 − 1 ) = ( 1 − 1 ) )
88 1m1e0 ⊢ ( 1 − 1 ) = 0
89 87 88 eqtrdi ⊢ ( 𝑚 = 1 → ( 𝑚 − 1 ) = 0 )
90 89 oveq2d ⊢ ( 𝑚 = 1 → ( 1 ... ( 𝑚 − 1 ) ) = ( 1 ... 0 ) )
91 fz10 ⊢ ( 1 ... 0 ) = ∅
92 90 91 eqtrdi ⊢ ( 𝑚 = 1 → ( 1 ... ( 𝑚 − 1 ) ) = ∅ )
93 92 sumeq1d ⊢ ( 𝑚 = 1 → Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ∅ ( 1 / 𝑖 ) )
94 sum0 ⊢ Σ 𝑖 ∈ ∅ ( 1 / 𝑖 ) = 0
95 93 94 eqtrdi ⊢ ( 𝑚 = 1 → Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = 0 )
96 95 95 jca ⊢ ( 𝑚 = 1 → ( Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = 0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = 0 ) )
97 oveq1 ⊢ ( 𝑚 = ( 𝑁 + 1 ) → ( 𝑚 − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
98 97 oveq2d ⊢ ( 𝑚 = ( 𝑁 + 1 ) → ( 1 ... ( 𝑚 − 1 ) ) = ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) )
99 98 sumeq1d ⊢ ( 𝑚 = ( 𝑁 + 1 ) → Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) )
100 99 99 jca ⊢ ( 𝑚 = ( 𝑁 + 1 ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ∧ Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) )
101 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
102 101 5 eleqtrdi ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
103 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 1 ... ( 𝑚 − 1 ) ) ∈ Fin )
104 elfznn ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) → 𝑖 ∈ ℕ )
105 104 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → 𝑖 ∈ ℕ )
106 105 nnrecred ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( 1 / 𝑖 ) ∈ ℝ )
107 103 106 fsumrecl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) ∈ ℝ )
108 107 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → Σ 𝑖 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( 1 / 𝑖 ) ∈ ℂ )
109 82 86 96 100 102 108 108 fsumparts ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 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 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
111 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 1 ... 𝑁 ) = ( 1 ..^ ( 𝑁 + 1 ) ) )
112 110 111 syl ⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) = ( 1 ..^ ( 𝑁 + 1 ) ) )
113 112 eqcomd ⊢ ( 𝑁 ∈ ℕ → ( 1 ..^ ( 𝑁 + 1 ) ) = ( 1 ... 𝑁 ) )
114 36 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ∈ ℂ )
115 6 nnrecred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑛 ) ∈ ℝ )
116 115 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑛 ) ∈ ℂ )
117 pncan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
118 39 40 117 sylancl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
119 118 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) = ( 1 ... 𝑛 ) )
120 119 sumeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) )
121 28 recnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑛 ) ) → ( 1 / 𝑖 ) ∈ ℂ )
122 oveq2 ⊢ ( 𝑖 = 𝑛 → ( 1 / 𝑖 ) = ( 1 / 𝑛 ) )
123 4 121 122 fsumm1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) = ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) + ( 1 / 𝑛 ) ) )
124 120 123 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) = ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) + ( 1 / 𝑛 ) ) )
125 114 116 124 mvrladdd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) − Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) = ( 1 / 𝑛 ) )
126 125 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) · ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) − Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) ) = ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) · ( 1 / 𝑛 ) ) )
127 6 nnne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ≠ 0 )
128 114 39 127 divrecd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) = ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) · ( 1 / 𝑛 ) ) )
129 126 128 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) · ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) − Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) ) = ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) )
130 113 129 sumeq12rdv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ..^ ( 𝑁 + 1 ) ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) · ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) − Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) )
131 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
132 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
133 131 40 132 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
134 133 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 1 ... 𝑁 ) )
135 134 sumeq1d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) )
136 135 135 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) · Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ) )
137 16 recnd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ∈ ℂ )
138 137 sqvald ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ) )
139 136 138 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) · Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) )
140 0cn ⊢ 0 ∈ ℂ
141 140 mul01i ⊢ ( 0 · 0 ) = 0
142 141 a1i ⊢ ( 𝑁 ∈ ℕ → ( 0 · 0 ) = 0 )
143 139 142 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) · Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) − ( 0 · 0 ) ) = ( ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) − 0 ) )
144 137 sqcld ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) ∈ ℂ )
145 144 subid1d ⊢ ( 𝑁 ∈ ℕ → ( ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) − 0 ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) )
146 143 145 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) · Σ 𝑖 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) − ( 0 · 0 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) )
147 125 120 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) − Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) · Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) = ( ( 1 / 𝑛 ) · Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) ) )
148 29 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) ∈ ℂ )
149 148 39 127 divrec2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) = ( ( 1 / 𝑛 ) · Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) ) )
150 147 149 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) − Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) · Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) )
151 113 150 sumeq12rdv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ..^ ( 𝑁 + 1 ) ) ( ( Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) − Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) ) · Σ 𝑖 ∈ ( 1 ... ( ( 𝑛 + 1 ) − 1 ) ) ( 1 / 𝑖 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) )
152 146 151 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( ( Σ 𝑖 ∈ ( 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 ⊢ ( 𝑁 ∈ ℕ → ( ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) − Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) )
154 31 recnd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) ∈ ℂ )
155 38 recnd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ∈ ℂ )
156 144 154 155 subaddd ⊢ ( 𝑁 ∈ ℕ → ( ( ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) − Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ↔ ( Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) ) )
157 153 156 mpbid ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑖 ) / 𝑛 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( Σ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 1 / 𝑖 ) / 𝑛 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) )
158 78 157 breqtrd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) )
159 24 158 eqbrtrd ⊢ ( 𝑁 ∈ ℕ → ( 2 · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) )
160 flid ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
161 110 160 syl ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
162 161 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( ⌊ ‘ 𝑁 ) ) = ( 1 ... 𝑁 ) )
163 162 sumeq1d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ( 1 / 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) )
164 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
165 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
166 harmonicubnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ≤ 𝑁 ) → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ( 1 / 𝑖 ) ≤ ( ( log ‘ 𝑁 ) + 1 ) )
167 164 165 166 syl2anc ⊢ ( 𝑁 ∈ ℕ → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ( 1 / 𝑖 ) ≤ ( ( log ‘ 𝑁 ) + 1 ) )
168 163 167 eqbrtrrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ≤ ( ( log ‘ 𝑁 ) + 1 ) )
169 14 nnrpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ℝ+ )
170 169 rpreccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑖 ) ∈ ℝ+ )
171 170 rpge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ ( 1 / 𝑖 ) )
172 2 15 171 fsumge0 ⊢ ( 𝑁 ∈ ℕ → 0 ≤ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) )
173 49 a1i ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℝ )
174 log1 ⊢ ( log ‘ 1 ) = 0
175 1rp ⊢ 1 ∈ ℝ+
176 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( 1 ≤ 𝑁 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑁 ) ) )
177 175 18 176 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 1 ≤ 𝑁 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑁 ) ) )
178 165 177 mpbid ⊢ ( 𝑁 ∈ ℕ → ( log ‘ 1 ) ≤ ( log ‘ 𝑁 ) )
179 174 178 eqbrtrrid ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( log ‘ 𝑁 ) )
180 19 lep1d ⊢ ( 𝑁 ∈ ℕ → ( log ‘ 𝑁 ) ≤ ( ( log ‘ 𝑁 ) + 1 ) )
181 173 19 21 179 180 letrd ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( ( log ‘ 𝑁 ) + 1 ) )
182 16 21 172 181 le2sqd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ≤ ( ( log ‘ 𝑁 ) + 1 ) ↔ ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) ≤ ( ( ( log ‘ 𝑁 ) + 1 ) ↑ 2 ) ) )
183 168 182 mpbid ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑖 ) ↑ 2 ) ≤ ( ( ( log ‘ 𝑁 ) + 1 ) ↑ 2 ) )
184 12 17 22 159 183 letrd ⊢ ( 𝑁 ∈ ℕ → ( 2 · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( log ‘ 𝑁 ) + 1 ) ↑ 2 ) )
185 1 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
186 2pos ⊢ 0 < 2
187 186 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 2 )
188 lemuldiv2 ⊢ ( ( Σ 𝑛 ∈ ( 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 ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( log ‘ 𝑁 ) + 1 ) ↑ 2 ) ↔ Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( ( ( ( log ‘ 𝑁 ) + 1 ) ↑ 2 ) / 2 ) ) )
190 184 189 mpbid ⊢ ( 𝑁 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( ( ( ( log ‘ 𝑁 ) + 1 ) ↑ 2 ) / 2 ) )