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	$⊢ N \in ℕ \to \sum_{n = 1}^{N} (\frac{\log n}{n}) \leq \frac{{(\log N + 1)}^{2}}{2}$

Proof

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

Metamath Proof Explorer

Theorem logdivbnd

Proof