Theorem lgamgulmlem3

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-Jul-2017)

	Ref	Expression
Hypotheses	lgamgulm.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	lgamgulm.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
	lgamgulm.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	lgamgulm.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	lgamgulm.l	⊢ ( 𝜑 → ( 2 · 𝑅 ) ≤ 𝑁 )
Assertion	lgamgulmlem3	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lgamgulm.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2		lgamgulm.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3		lgamgulm.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		lgamgulm.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
5		lgamgulm.l	⊢ ( 𝜑 → ( 2 · 𝑅 ) ≤ 𝑁 )
6	1 2	lgamgulmlem1	⊢ ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
7	6 4	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
8	7	eldifad	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
9	3	peano2nnd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
10	9	nnrpd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ+ )
11	3	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
12	10 11	rpdivcld	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) / 𝑁 ) ∈ ℝ+ )
13	12	relogcld	⊢ ( 𝜑 → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ∈ ℝ )
14	13	recnd	⊢ ( 𝜑 → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ∈ ℂ )
15	8 14	mulcld	⊢ ( 𝜑 → ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) ∈ ℂ )
16	3	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
17	3	nnne0d	⊢ ( 𝜑 → 𝑁 ≠ 0 )
18	8 16 17	divcld	⊢ ( 𝜑 → ( 𝐴 / 𝑁 ) ∈ ℂ )
19		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
20	18 19	addcld	⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) + 1 ) ∈ ℂ )
21	7 3	dmgmdivn0	⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) + 1 ) ≠ 0 )
22	20 21	logcld	⊢ ( 𝜑 → ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ∈ ℂ )
23	15 22	subcld	⊢ ( 𝜑 → ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ∈ ℂ )
24	23	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ∈ ℝ )
25	15 18	subcld	⊢ ( 𝜑 → ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ∈ ℂ )
26	25	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) ∈ ℝ )
27	18 22	subcld	⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ∈ ℂ )
28	27	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ∈ ℝ )
29	26 28	readdcld	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) + ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ) ∈ ℝ )
30	1	nnred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
31		2re	⊢ 2 ∈ ℝ
32	31	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
33		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
34	30 33	readdcld	⊢ ( 𝜑 → ( 𝑅 + 1 ) ∈ ℝ )
35	32 34	remulcld	⊢ ( 𝜑 → ( 2 · ( 𝑅 + 1 ) ) ∈ ℝ )
36	3	nnsqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )
37	35 36	nndivred	⊢ ( 𝜑 → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ∈ ℝ )
38	30 37	remulcld	⊢ ( 𝜑 → ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) ∈ ℝ )
39	15 22 18	abs3difd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) + ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ) )
40	3	nnrecred	⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ )
41	9	nnrecred	⊢ ( 𝜑 → ( 1 / ( 𝑁 + 1 ) ) ∈ ℝ )
42	40 41	resubcld	⊢ ( 𝜑 → ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ∈ ℝ )
43	30 42	remulcld	⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) ∈ ℝ )
44	32 30	remulcld	⊢ ( 𝜑 → ( 2 · 𝑅 ) ∈ ℝ )
45	3	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
46	1	nnrpd	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
47	30 46	ltaddrpd	⊢ ( 𝜑 → 𝑅 < ( 𝑅 + 𝑅 ) )
48	1	nncnd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
49	48	2timesd	⊢ ( 𝜑 → ( 2 · 𝑅 ) = ( 𝑅 + 𝑅 ) )
50	47 49	breqtrrd	⊢ ( 𝜑 → 𝑅 < ( 2 · 𝑅 ) )
51	30 44 45 50 5	ltletrd	⊢ ( 𝜑 → 𝑅 < 𝑁 )
52		difrp	⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑅 < 𝑁 ↔ ( 𝑁 − 𝑅 ) ∈ ℝ+ ) )
53	30 45 52	syl2anc	⊢ ( 𝜑 → ( 𝑅 < 𝑁 ↔ ( 𝑁 − 𝑅 ) ∈ ℝ+ ) )
54	51 53	mpbid	⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ∈ ℝ+ )
55	54	rprecred	⊢ ( 𝜑 → ( 1 / ( 𝑁 − 𝑅 ) ) ∈ ℝ )
56	55 40	resubcld	⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ∈ ℝ )
57	30 56	remulcld	⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ∈ ℝ )
58	43 57	readdcld	⊢ ( 𝜑 → ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ∈ ℝ )
59	8 16 17	divrecd	⊢ ( 𝜑 → ( 𝐴 / 𝑁 ) = ( 𝐴 · ( 1 / 𝑁 ) ) )
60	59	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) = ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 · ( 1 / 𝑁 ) ) ) )
61	40	recnd	⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℂ )
62	8 14 61	subdid	⊢ ( 𝜑 → ( 𝐴 · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 · ( 1 / 𝑁 ) ) ) )
63	60 62	eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) = ( 𝐴 · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) )
64	63	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) = ( abs ‘ ( 𝐴 · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) )
65	14 61	subcld	⊢ ( 𝜑 → ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ∈ ℂ )
66	8 65	absmuld	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) )
67	64 66	eqtrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) )
68	8	abscld	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ )
69	65	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ∈ ℝ )
70	8	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐴 ) )
71	65	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) )
72		fveq2	⊢ ( 𝑥 = 𝐴 → ( abs ‘ 𝑥 ) = ( abs ‘ 𝐴 ) )
73	72	breq1d	⊢ ( 𝑥 = 𝐴 → ( ( abs ‘ 𝑥 ) ≤ 𝑅 ↔ ( abs ‘ 𝐴 ) ≤ 𝑅 ) )
74		fvoveq1	⊢ ( 𝑥 = 𝐴 → ( abs ‘ ( 𝑥 + 𝑘 ) ) = ( abs ‘ ( 𝐴 + 𝑘 ) ) )
75	74	breq2d	⊢ ( 𝑥 = 𝐴 → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) )
76	75	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) )
77	73 76	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ↔ ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) ) )
78	77 2	elrab2	⊢ ( 𝐴 ∈ 𝑈 ↔ ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) ) )
79	78	simprbi	⊢ ( 𝐴 ∈ 𝑈 → ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) )
80	4 79	syl	⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) )
81	80	simpld	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 𝑅 )
82	10 11	relogdivd	⊢ ( 𝜑 → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) = ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
83		logdifbnd	⊢ ( 𝑁 ∈ ℝ+ → ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) ≤ ( 1 / 𝑁 ) )
84	11 83	syl	⊢ ( 𝜑 → ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) ≤ ( 1 / 𝑁 ) )
85	82 84	eqbrtrd	⊢ ( 𝜑 → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ≤ ( 1 / 𝑁 ) )
86	13 40 85	abssuble0d	⊢ ( 𝜑 → ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 1 / 𝑁 ) − ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
87		logdiflbnd	⊢ ( 𝑁 ∈ ℝ+ → ( 1 / ( 𝑁 + 1 ) ) ≤ ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
88	11 87	syl	⊢ ( 𝜑 → ( 1 / ( 𝑁 + 1 ) ) ≤ ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
89	88 82	breqtrrd	⊢ ( 𝜑 → ( 1 / ( 𝑁 + 1 ) ) ≤ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) )
90	41 13 40 89	lesub2dd	⊢ ( 𝜑 → ( ( 1 / 𝑁 ) − ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) ≤ ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) )
91	86 90	eqbrtrd	⊢ ( 𝜑 → ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ≤ ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) )
92	68 30 69 42 70 71 81 91	lemul12ad	⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) ≤ ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) )
93	67 92	eqbrtrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) ≤ ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) )
94	1 2 3 4 5	lgamgulmlem2	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) )
95	26 28 43 57 93 94	le2addd	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) + ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ) ≤ ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) )
96	16 48	subcld	⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ∈ ℂ )
97	16 19	addcld	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
98	30 51	gtned	⊢ ( 𝜑 → 𝑁 ≠ 𝑅 )
99	16 48 98	subne0d	⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ≠ 0 )
100	9	nnne0d	⊢ ( 𝜑 → ( 𝑁 + 1 ) ≠ 0 )
101	96 97 99 100	subrecd	⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) = ( ( ( 𝑁 + 1 ) − ( 𝑁 − 𝑅 ) ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) )
102	16 19 48	pnncand	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 𝑁 − 𝑅 ) ) = ( 1 + 𝑅 ) )
103	19 48 102	comraddd	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 𝑁 − 𝑅 ) ) = ( 𝑅 + 1 ) )
104	103	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) − ( 𝑁 − 𝑅 ) ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) = ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) )
105	101 104	eqtr2d	⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) = ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) )
106	105	oveq2d	⊢ ( 𝜑 → ( 𝑅 · ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ) = ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) ) )
107	97 100	reccld	⊢ ( 𝜑 → ( 1 / ( 𝑁 + 1 ) ) ∈ ℂ )
108	96 99	reccld	⊢ ( 𝜑 → ( 1 / ( 𝑁 − 𝑅 ) ) ∈ ℂ )
109	61 107 108	npncan3d	⊢ ( 𝜑 → ( ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) + ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) )
110	109	eqcomd	⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) = ( ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) + ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) )
111	110	oveq2d	⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) ) = ( 𝑅 · ( ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) + ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) )
112	42	recnd	⊢ ( 𝜑 → ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ∈ ℂ )
113	56	recnd	⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ∈ ℂ )
114	48 112 113	adddid	⊢ ( 𝜑 → ( 𝑅 · ( ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) + ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) = ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) )
115	106 111 114	3eqtrd	⊢ ( 𝜑 → ( 𝑅 · ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ) = ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) )
116	54 10	rpmulcld	⊢ ( 𝜑 → ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ∈ ℝ+ )
117	34 116	rerpdivcld	⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ∈ ℝ )
118	46	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝑅 )
119		2z	⊢ 2 ∈ ℤ
120	119	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
121	11 120	rpexpcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℝ+ )
122	121	rphalfcld	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / 2 ) ∈ ℝ+ )
123		0le1	⊢ 0 ≤ 1
124	123	a1i	⊢ ( 𝜑 → 0 ≤ 1 )
125	30 33 118 124	addge0d	⊢ ( 𝜑 → 0 ≤ ( 𝑅 + 1 ) )
126	16	sqvald	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
127	126	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / 2 ) = ( ( 𝑁 · 𝑁 ) / 2 ) )
128	32	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
129		2ne0	⊢ 2 ≠ 0
130	129	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
131	16 16 128 130	div23d	⊢ ( 𝜑 → ( ( 𝑁 · 𝑁 ) / 2 ) = ( ( 𝑁 / 2 ) · 𝑁 ) )
132	127 131	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / 2 ) = ( ( 𝑁 / 2 ) · 𝑁 ) )
133	45	rehalfcld	⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℝ )
134	45 30	resubcld	⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ∈ ℝ )
135	45 33	readdcld	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ )
136		2rp	⊢ 2 ∈ ℝ+
137	136	a1i	⊢ ( 𝜑 → 2 ∈ ℝ+ )
138	11	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝑁 )
139	45 137 138	divge0d	⊢ ( 𝜑 → 0 ≤ ( 𝑁 / 2 ) )
140	30 45 137	lemuldiv2d	⊢ ( 𝜑 → ( ( 2 · 𝑅 ) ≤ 𝑁 ↔ 𝑅 ≤ ( 𝑁 / 2 ) ) )
141	5 140	mpbid	⊢ ( 𝜑 → 𝑅 ≤ ( 𝑁 / 2 ) )
142	16	2halvesd	⊢ ( 𝜑 → ( ( 𝑁 / 2 ) + ( 𝑁 / 2 ) ) = 𝑁 )
143	133	recnd	⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℂ )
144	16 143 143	subaddd	⊢ ( 𝜑 → ( ( 𝑁 − ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) ↔ ( ( 𝑁 / 2 ) + ( 𝑁 / 2 ) ) = 𝑁 ) )
145	142 144	mpbird	⊢ ( 𝜑 → ( 𝑁 − ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
146	141 145	breqtrrd	⊢ ( 𝜑 → 𝑅 ≤ ( 𝑁 − ( 𝑁 / 2 ) ) )
147	30 45 133 146	lesubd	⊢ ( 𝜑 → ( 𝑁 / 2 ) ≤ ( 𝑁 − 𝑅 ) )
148	45	lep1d	⊢ ( 𝜑 → 𝑁 ≤ ( 𝑁 + 1 ) )
149	133 134 45 135 139 138 147 148	lemul12ad	⊢ ( 𝜑 → ( ( 𝑁 / 2 ) · 𝑁 ) ≤ ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) )
150	132 149	eqbrtrd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / 2 ) ≤ ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) )
151	122 116 34 125 150	lediv2ad	⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ≤ ( ( 𝑅 + 1 ) / ( ( 𝑁 ↑ 2 ) / 2 ) ) )
152	1	peano2nnd	⊢ ( 𝜑 → ( 𝑅 + 1 ) ∈ ℕ )
153	152	nncnd	⊢ ( 𝜑 → ( 𝑅 + 1 ) ∈ ℂ )
154	36	nncnd	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
155	36	nnne0d	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ≠ 0 )
156	153 154 128 155 130	divdiv2d	⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 ↑ 2 ) / 2 ) ) = ( ( ( 𝑅 + 1 ) · 2 ) / ( 𝑁 ↑ 2 ) ) )
157	153 128	mulcomd	⊢ ( 𝜑 → ( ( 𝑅 + 1 ) · 2 ) = ( 2 · ( 𝑅 + 1 ) ) )
158	157	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑅 + 1 ) · 2 ) / ( 𝑁 ↑ 2 ) ) = ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) )
159	156 158	eqtr2d	⊢ ( 𝜑 → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) = ( ( 𝑅 + 1 ) / ( ( 𝑁 ↑ 2 ) / 2 ) ) )
160	151 159	breqtrrd	⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ≤ ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) )
161	117 37 30 118 160	lemul2ad	⊢ ( 𝜑 → ( 𝑅 · ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
162	115 161	eqbrtrrd	⊢ ( 𝜑 → ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
163	29 58 38 95 162	letrd	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) + ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
164	24 29 38 39 163	letrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )