lgamgulmlem3

	Ref	Expression
Hypotheses	lgamgulm.r	$⊢ φ \to R \in ℕ$
	lgamgulm.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|)\}$
	lgamgulm.n	$⊢ φ \to N \in ℕ$
	lgamgulm.a	$⊢ φ \to A \in U$
	lgamgulm.l	$⊢ φ \to 2 R \leq N$
Assertion	lgamgulmlem3	$⊢ φ \to \|A \log (\frac{N + 1}{N}) - \log ((\frac{A}{N}) + 1)\| \leq R (\frac{2 (R + 1)}{N^{2}})$

Proof

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

Metamath Proof Explorer

Theorem lgamgulmlem3

Proof