rplogsumlem1

		Ref	Expression
	Assertion	rplogsumlem1	$⊢ A \in ℕ \to \sum_{n = 2}^{A} (\frac{\log n}{n (n - 1)}) \leq 2$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ A \in ℕ \to (2 \dots A) \in Fin$
2		elfzuz	$⊢ n \in (2 \dots A) \to n \in ℤ_{\geq 2}$
3		eluz2nn	$⊢ n \in ℤ_{\geq 2} \to n \in ℕ$
4	2 3	syl	$⊢ n \in (2 \dots A) \to n \in ℕ$
5	4	adantl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n \in ℕ$
6	5	nnrpd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n \in ℝ^{+}$
7	6	relogcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \log n \in ℝ$
8	2	adantl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n \in ℤ_{\geq 2}$
9		uz2m1nn	$⊢ n \in ℤ_{\geq 2} \to n - 1 \in ℕ$
10	8 9	syl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n - 1 \in ℕ$
11	5 10	nnmulcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n (n - 1) \in ℕ$
12	7 11	nndivred	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \frac{\log n}{n (n - 1)} \in ℝ$
13	1 12	fsumrecl	$⊢ A \in ℕ \to \sum_{n = 2}^{A} (\frac{\log n}{n (n - 1)}) \in ℝ$
14		2re	$⊢ 2 \in ℝ$
15	10	nnrpd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n - 1 \in ℝ^{+}$
16	15	rpsqrtcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n - 1} \in ℝ^{+}$
17		rerpdivcl	$⊢ (2 \in ℝ \land \sqrt{n - 1} \in ℝ^{+}) \to \frac{2}{\sqrt{n - 1}} \in ℝ$
18	14 16 17	sylancr	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \frac{2}{\sqrt{n - 1}} \in ℝ$
19	6	rpsqrtcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \in ℝ^{+}$
20		rerpdivcl	$⊢ (2 \in ℝ \land \sqrt{n} \in ℝ^{+}) \to \frac{2}{\sqrt{n}} \in ℝ$
21	14 19 20	sylancr	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \frac{2}{\sqrt{n}} \in ℝ$
22	18 21	resubcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}) \in ℝ$
23	1 22	fsumrecl	$⊢ A \in ℕ \to \sum_{n = 2}^{A} ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})) \in ℝ$
24	14	a1i	$⊢ A \in ℕ \to 2 \in ℝ$
25	16	rpred	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n - 1} \in ℝ$
26	5	nnred	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n \in ℝ$
27		peano2rem	$⊢ n \in ℝ \to n - 1 \in ℝ$
28	26 27	syl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n - 1 \in ℝ$
29	26 28	remulcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n (n - 1) \in ℝ$
30	29 22	remulcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n (n - 1) ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})) \in ℝ$
31	5	nncnd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n \in ℂ$
32		ax-1cn	$⊢ 1 \in ℂ$
33		npcan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 + 1 = n$
34	31 32 33	sylancl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n - 1 + 1 = n$
35	34	fveq2d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \log (n - 1 + 1) = \log n$
36	15	rpge0d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 0 \leq n - 1$
37		loglesqrt	$⊢ (n - 1 \in ℝ \land 0 \leq n - 1) \to \log (n - 1 + 1) \leq \sqrt{n - 1}$
38	28 36 37	syl2anc	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \log (n - 1 + 1) \leq \sqrt{n - 1}$
39	35 38	eqbrtrrd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \log n \leq \sqrt{n - 1}$
40	19	rpred	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \in ℝ$
41	40 25	readdcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} + \sqrt{n - 1} \in ℝ$
42		remulcl	$⊢ (\sqrt{n} \in ℝ \land 2 \in ℝ) \to \sqrt{n} \cdot 2 \in ℝ$
43	40 14 42	sylancl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \cdot 2 \in ℝ$
44	40 25	resubcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} - \sqrt{n - 1} \in ℝ$
45	26	lem1d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n - 1 \leq n$
46	6	rpge0d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 0 \leq n$
47	28 36 26 46	sqrtled	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (n - 1 \leq n \leftrightarrow \sqrt{n - 1} \leq \sqrt{n})$
48	45 47	mpbid	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n - 1} \leq \sqrt{n}$
49	40 25	subge0d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (0 \leq \sqrt{n} - \sqrt{n - 1} \leftrightarrow \sqrt{n - 1} \leq \sqrt{n})$
50	48 49	mpbird	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 0 \leq \sqrt{n} - \sqrt{n - 1}$
51	25 40 40 48	leadd2dd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} + \sqrt{n - 1} \leq \sqrt{n} + \sqrt{n}$
52	19	rpcnd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \in ℂ$
53	52	times2d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \cdot 2 = \sqrt{n} + \sqrt{n}$
54	51 53	breqtrrd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} + \sqrt{n - 1} \leq \sqrt{n} \cdot 2$
55	41 43 44 50 54	lemul1ad	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\sqrt{n} + \sqrt{n - 1}) (\sqrt{n} - \sqrt{n - 1}) \leq \sqrt{n} \cdot 2 (\sqrt{n} - \sqrt{n - 1})$
56	31	sqsqrtd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to {\sqrt{n}}^{2} = n$
57		subcl	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 \in ℂ$
58	31 32 57	sylancl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n - 1 \in ℂ$
59	58	sqsqrtd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to {\sqrt{n - 1}}^{2} = n - 1$
60	56 59	oveq12d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to {\sqrt{n}}^{2} - {\sqrt{n - 1}}^{2} = n - (n - 1)$
61	16	rpcnd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n - 1} \in ℂ$
62		subsq	$⊢ (\sqrt{n} \in ℂ \land \sqrt{n - 1} \in ℂ) \to {\sqrt{n}}^{2} - {\sqrt{n - 1}}^{2} = (\sqrt{n} + \sqrt{n - 1}) (\sqrt{n} - \sqrt{n - 1})$
63	52 61 62	syl2anc	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to {\sqrt{n}}^{2} - {\sqrt{n - 1}}^{2} = (\sqrt{n} + \sqrt{n - 1}) (\sqrt{n} - \sqrt{n - 1})$
64		nncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - (n - 1) = 1$
65	31 32 64	sylancl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n - (n - 1) = 1$
66	60 63 65	3eqtr3d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\sqrt{n} + \sqrt{n - 1}) (\sqrt{n} - \sqrt{n - 1}) = 1$
67		2cn	$⊢ 2 \in ℂ$
68	67	a1i	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 2 \in ℂ$
69	44	recnd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} - \sqrt{n - 1} \in ℂ$
70	52 68 69	mulassd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \cdot 2 (\sqrt{n} - \sqrt{n - 1}) = \sqrt{n} 2 (\sqrt{n} - \sqrt{n - 1})$
71	55 66 70	3brtr3d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 1 \leq \sqrt{n} 2 (\sqrt{n} - \sqrt{n - 1})$
72		1red	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 1 \in ℝ$
73		remulcl	$⊢ (2 \in ℝ \land \sqrt{n} - \sqrt{n - 1} \in ℝ) \to 2 (\sqrt{n} - \sqrt{n - 1}) \in ℝ$
74	14 44 73	sylancr	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 2 (\sqrt{n} - \sqrt{n - 1}) \in ℝ$
75	40 74	remulcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} 2 (\sqrt{n} - \sqrt{n - 1}) \in ℝ$
76	72 75 16	lemul1d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (1 \leq \sqrt{n} 2 (\sqrt{n} - \sqrt{n - 1}) \leftrightarrow 1 \sqrt{n - 1} \leq \sqrt{n} 2 (\sqrt{n} - \sqrt{n - 1}) \sqrt{n - 1})$
77	71 76	mpbid	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 1 \sqrt{n - 1} \leq \sqrt{n} 2 (\sqrt{n} - \sqrt{n - 1}) \sqrt{n - 1}$
78	61	mulid2d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 1 \sqrt{n - 1} = \sqrt{n - 1}$
79	74	recnd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 2 (\sqrt{n} - \sqrt{n - 1}) \in ℂ$
80	52 79 61	mul32d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} 2 (\sqrt{n} - \sqrt{n - 1}) \sqrt{n - 1} = \sqrt{n} \sqrt{n - 1} 2 (\sqrt{n} - \sqrt{n - 1})$
81	77 78 80	3brtr3d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n - 1} \leq \sqrt{n} \sqrt{n - 1} 2 (\sqrt{n} - \sqrt{n - 1})$
82		remsqsqrt	$⊢ (n \in ℝ \land 0 \leq n) \to \sqrt{n} \sqrt{n} = n$
83	26 46 82	syl2anc	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n} = n$
84		remsqsqrt	$⊢ (n - 1 \in ℝ \land 0 \leq n - 1) \to \sqrt{n - 1} \sqrt{n - 1} = n - 1$
85	28 36 84	syl2anc	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n - 1} \sqrt{n - 1} = n - 1$
86	83 85	oveq12d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n} \sqrt{n - 1} \sqrt{n - 1} = n (n - 1)$
87	52 52 61 61	mul4d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n} \sqrt{n - 1} \sqrt{n - 1} = \sqrt{n} \sqrt{n - 1} \sqrt{n} \sqrt{n - 1}$
88	86 87	eqtr3d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n (n - 1) = \sqrt{n} \sqrt{n - 1} \sqrt{n} \sqrt{n - 1}$
89	16	rpcnne0d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\sqrt{n - 1} \in ℂ \land \sqrt{n - 1} \neq 0)$
90	19	rpcnne0d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\sqrt{n} \in ℂ \land \sqrt{n} \neq 0)$
91		divsubdiv	$⊢ ((2 \in ℂ \land 2 \in ℂ) \land ((\sqrt{n - 1} \in ℂ \land \sqrt{n - 1} \neq 0) \land (\sqrt{n} \in ℂ \land \sqrt{n} \neq 0))) \to (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}) = \frac{2 \sqrt{n} - 2 \sqrt{n - 1}}{\sqrt{n - 1} \sqrt{n}}$
92	68 68 89 90 91	syl22anc	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}) = \frac{2 \sqrt{n} - 2 \sqrt{n - 1}}{\sqrt{n - 1} \sqrt{n}}$
93	68 52 61	subdid	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 2 (\sqrt{n} - \sqrt{n - 1}) = 2 \sqrt{n} - 2 \sqrt{n - 1}$
94	52 61	mulcomd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n - 1} = \sqrt{n - 1} \sqrt{n}$
95	93 94	oveq12d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}} = \frac{2 \sqrt{n} - 2 \sqrt{n - 1}}{\sqrt{n - 1} \sqrt{n}}$
96	92 95	eqtr4d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}) = \frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}}$
97	88 96	oveq12d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n (n - 1) ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})) = \sqrt{n} \sqrt{n - 1} \sqrt{n} \sqrt{n - 1} (\frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}})$
98	52 61	mulcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n - 1} \in ℂ$
99	19 16	rpmulcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n - 1} \in ℝ^{+}$
100	74 99	rerpdivcld	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}} \in ℝ$
101	100	recnd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}} \in ℂ$
102	98 98 101	mulassd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n - 1} \sqrt{n} \sqrt{n - 1} (\frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}}) = \sqrt{n} \sqrt{n - 1} \sqrt{n} \sqrt{n - 1} (\frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}})$
103	99	rpne0d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n - 1} \neq 0$
104	79 98 103	divcan2d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n - 1} (\frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}}) = 2 (\sqrt{n} - \sqrt{n - 1})$
105	104	oveq2d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n} \sqrt{n - 1} \sqrt{n} \sqrt{n - 1} (\frac{2 (\sqrt{n} - \sqrt{n - 1})}{\sqrt{n} \sqrt{n - 1}}) = \sqrt{n} \sqrt{n - 1} 2 (\sqrt{n} - \sqrt{n - 1})$
106	97 102 105	3eqtrd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n (n - 1) ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})) = \sqrt{n} \sqrt{n - 1} 2 (\sqrt{n} - \sqrt{n - 1})$
107	81 106	breqtrrd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n - 1} \leq n (n - 1) ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}))$
108	7 25 30 39 107	letrd	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \log n \leq n (n - 1) ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}))$
109	11	nngt0d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to 0 < n (n - 1)$
110		ledivmul	$⊢ (\log n \in ℝ \land (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}) \in ℝ \land (n (n - 1) \in ℝ \land 0 < n (n - 1))) \to (\frac{\log n}{n (n - 1)} \leq (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}) \leftrightarrow \log n \leq n (n - 1) ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})))$
111	7 22 29 109 110	syl112anc	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\frac{\log n}{n (n - 1)} \leq (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}) \leftrightarrow \log n \leq n (n - 1) ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})))$
112	108 111	mpbird	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \frac{\log n}{n (n - 1)} \leq (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})$
113	1 12 22 112	fsumle	$⊢ A \in ℕ \to \sum_{n = 2}^{A} (\frac{\log n}{n (n - 1)}) \leq \sum_{n = 2}^{A} ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}))$
114		fvoveq1	$⊢ k = n \to \sqrt{k - 1} = \sqrt{n - 1}$
115	114	oveq2d	$⊢ k = n \to \frac{2}{\sqrt{k - 1}} = \frac{2}{\sqrt{n - 1}}$
116		fvoveq1	$⊢ k = n + 1 \to \sqrt{k - 1} = \sqrt{n + 1 - 1}$
117	116	oveq2d	$⊢ k = n + 1 \to \frac{2}{\sqrt{k - 1}} = \frac{2}{\sqrt{n + 1 - 1}}$
118		oveq1	$⊢ k = 2 \to k - 1 = 2 - 1$
119		2m1e1	$⊢ 2 - 1 = 1$
120	118 119	eqtrdi	$⊢ k = 2 \to k - 1 = 1$
121	120	fveq2d	$⊢ k = 2 \to \sqrt{k - 1} = \sqrt{1}$
122		sqrt1	$⊢ \sqrt{1} = 1$
123	121 122	eqtrdi	$⊢ k = 2 \to \sqrt{k - 1} = 1$
124	123	oveq2d	$⊢ k = 2 \to \frac{2}{\sqrt{k - 1}} = \frac{2}{1}$
125	67	div1i	$⊢ \frac{2}{1} = 2$
126	124 125	eqtrdi	$⊢ k = 2 \to \frac{2}{\sqrt{k - 1}} = 2$
127		fvoveq1	$⊢ k = A + 1 \to \sqrt{k - 1} = \sqrt{A + 1 - 1}$
128	127	oveq2d	$⊢ k = A + 1 \to \frac{2}{\sqrt{k - 1}} = \frac{2}{\sqrt{A + 1 - 1}}$
129		nnz	$⊢ A \in ℕ \to A \in ℤ$
130		eluzp1p1	$⊢ A \in ℤ_{\geq 1} \to A + 1 \in ℤ_{\geq (1 + 1)}$
131		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
132	130 131	eleq2s	$⊢ A \in ℕ \to A + 1 \in ℤ_{\geq (1 + 1)}$
133		df-2	$⊢ 2 = 1 + 1$
134	133	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
135	132 134	eleqtrrdi	$⊢ A \in ℕ \to A + 1 \in ℤ_{\geq 2}$
136		elfzuz	$⊢ k \in (2 \dots A + 1) \to k \in ℤ_{\geq 2}$
137		uz2m1nn	$⊢ k \in ℤ_{\geq 2} \to k - 1 \in ℕ$
138	136 137	syl	$⊢ k \in (2 \dots A + 1) \to k - 1 \in ℕ$
139	138	adantl	$⊢ (A \in ℕ \land k \in (2 \dots A + 1)) \to k - 1 \in ℕ$
140	139	nnrpd	$⊢ (A \in ℕ \land k \in (2 \dots A + 1)) \to k - 1 \in ℝ^{+}$
141	140	rpsqrtcld	$⊢ (A \in ℕ \land k \in (2 \dots A + 1)) \to \sqrt{k - 1} \in ℝ^{+}$
142		rerpdivcl	$⊢ (2 \in ℝ \land \sqrt{k - 1} \in ℝ^{+}) \to \frac{2}{\sqrt{k - 1}} \in ℝ$
143	14 141 142	sylancr	$⊢ (A \in ℕ \land k \in (2 \dots A + 1)) \to \frac{2}{\sqrt{k - 1}} \in ℝ$
144	143	recnd	$⊢ (A \in ℕ \land k \in (2 \dots A + 1)) \to \frac{2}{\sqrt{k - 1}} \in ℂ$
145	115 117 126 128 129 135 144	telfsum	$⊢ A \in ℕ \to \sum_{n = 2}^{A} ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n + 1 - 1}})) = 2 - (\frac{2}{\sqrt{A + 1 - 1}})$
146		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
147	31 32 146	sylancl	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to n + 1 - 1 = n$
148	147	fveq2d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \sqrt{n + 1 - 1} = \sqrt{n}$
149	148	oveq2d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to \frac{2}{\sqrt{n + 1 - 1}} = \frac{2}{\sqrt{n}}$
150	149	oveq2d	$⊢ (A \in ℕ \land n \in (2 \dots A)) \to (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n + 1 - 1}}) = (\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})$
151	150	sumeq2dv	$⊢ A \in ℕ \to \sum_{n = 2}^{A} ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n + 1 - 1}})) = \sum_{n = 2}^{A} ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}}))$
152		nncn	$⊢ A \in ℕ \to A \in ℂ$
153		pncan	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 - 1 = A$
154	152 32 153	sylancl	$⊢ A \in ℕ \to A + 1 - 1 = A$
155	154	fveq2d	$⊢ A \in ℕ \to \sqrt{A + 1 - 1} = \sqrt{A}$
156	155	oveq2d	$⊢ A \in ℕ \to \frac{2}{\sqrt{A + 1 - 1}} = \frac{2}{\sqrt{A}}$
157	156	oveq2d	$⊢ A \in ℕ \to 2 - (\frac{2}{\sqrt{A + 1 - 1}}) = 2 - (\frac{2}{\sqrt{A}})$
158	145 151 157	3eqtr3d	$⊢ A \in ℕ \to \sum_{n = 2}^{A} ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})) = 2 - (\frac{2}{\sqrt{A}})$
159		2rp	$⊢ 2 \in ℝ^{+}$
160		nnrp	$⊢ A \in ℕ \to A \in ℝ^{+}$
161	160	rpsqrtcld	$⊢ A \in ℕ \to \sqrt{A} \in ℝ^{+}$
162		rpdivcl	$⊢ (2 \in ℝ^{+} \land \sqrt{A} \in ℝ^{+}) \to \frac{2}{\sqrt{A}} \in ℝ^{+}$
163	159 161 162	sylancr	$⊢ A \in ℕ \to \frac{2}{\sqrt{A}} \in ℝ^{+}$
164	163	rpge0d	$⊢ A \in ℕ \to 0 \leq \frac{2}{\sqrt{A}}$
165	163	rpred	$⊢ A \in ℕ \to \frac{2}{\sqrt{A}} \in ℝ$
166		subge02	$⊢ (2 \in ℝ \land \frac{2}{\sqrt{A}} \in ℝ) \to (0 \leq \frac{2}{\sqrt{A}} \leftrightarrow 2 - (\frac{2}{\sqrt{A}}) \leq 2)$
167	14 165 166	sylancr	$⊢ A \in ℕ \to (0 \leq \frac{2}{\sqrt{A}} \leftrightarrow 2 - (\frac{2}{\sqrt{A}}) \leq 2)$
168	164 167	mpbid	$⊢ A \in ℕ \to 2 - (\frac{2}{\sqrt{A}}) \leq 2$
169	158 168	eqbrtrd	$⊢ A \in ℕ \to \sum_{n = 2}^{A} ((\frac{2}{\sqrt{n - 1}}) - (\frac{2}{\sqrt{n}})) \leq 2$
170	13 23 24 113 169	letrd	$⊢ A \in ℕ \to \sum_{n = 2}^{A} (\frac{\log n}{n (n - 1)}) \leq 2$

Metamath Proof Explorer

Theorem rplogsumlem1

Proof