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 ) )