Theorem rplogsumlem1

Description: Lemma for rplogsum . (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Assertion	rplogsumlem1	⊢ ( 𝐴 ∈ ℕ → Σ 𝑛 ∈ ( 2 ... 𝐴 ) ( ( log ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 − 1 ) ) ) ≤ 2 )

Proof

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