lgamgulmlem5

	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.g	$⊢ G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
	lgamgulm.t	$⊢ T = (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π))$
Assertion	lgamgulmlem5	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|G (n) (y)\| \leq T (n)$

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.g	$⊢ G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
4		lgamgulm.t	$⊢ T = (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π))$
5		breq2	$⊢ R (\frac{2 (R + 1)}{n^{2}}) = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π) \to (\|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq R (\frac{2 (R + 1)}{n^{2}}) \leftrightarrow \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π))$
6		breq2	$⊢ R \log (\frac{n + 1}{n}) + \log (R + 1) n + π = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π) \to (\|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq R \log (\frac{n + 1}{n}) + \log (R + 1) n + π \leftrightarrow \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π))$
7	1	adantr	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R \in ℕ$
8	7	adantr	$⊢ ((φ \land (n \in ℕ \land y \in U)) \land 2 R \leq n) \to R \in ℕ$
9		fveq2	$⊢ x = t \to \|x\| = \|t\|$
10	9	breq1d	$⊢ x = t \to (\|x\| \leq R \leftrightarrow \|t\| \leq R)$
11		fvoveq1	$⊢ x = t \to \|x + k\| = \|t + k\|$
12	11	breq2d	$⊢ x = t \to (\frac{1}{R} \leq \|x + k\| \leftrightarrow \frac{1}{R} \leq \|t + k\|)$
13	12	ralbidv	$⊢ x = t \to (\forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\| \leftrightarrow \forall k \in ℕ_{0} \frac{1}{R} \leq \|t + k\|)$
14	10 13	anbi12d	$⊢ x = t \to ((\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|) \leftrightarrow (\|t\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|t + k\|))$
15	14	cbvrabv	$⊢ \{x \in ℂ \| (\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|)\} = \{t \in ℂ \| (\|t\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|t + k\|)\}$
16	2 15	eqtri	$⊢ U = \{t \in ℂ \| (\|t\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|t + k\|)\}$
17		simplrl	$⊢ ((φ \land (n \in ℕ \land y \in U)) \land 2 R \leq n) \to n \in ℕ$
18		simprr	$⊢ (φ \land (n \in ℕ \land y \in U)) \to y \in U$
19	18	adantr	$⊢ ((φ \land (n \in ℕ \land y \in U)) \land 2 R \leq n) \to y \in U$
20		simpr	$⊢ ((φ \land (n \in ℕ \land y \in U)) \land 2 R \leq n) \to 2 R \leq n$
21	8 16 17 19 20	lgamgulmlem3	$⊢ ((φ \land (n \in ℕ \land y \in U)) \land 2 R \leq n) \to \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq R (\frac{2 (R + 1)}{n^{2}})$
22	1 2	lgamgulmlem1	$⊢ φ \to U \subseteq ℂ ∖ (ℤ ∖ ℕ)$
23	22	adantr	$⊢ (φ \land (n \in ℕ \land y \in U)) \to U \subseteq ℂ ∖ (ℤ ∖ ℕ)$
24	23 18	sseldd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to y \in (ℂ ∖ (ℤ ∖ ℕ))$
25	24	eldifad	$⊢ (φ \land (n \in ℕ \land y \in U)) \to y \in ℂ$
26		simprl	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n \in ℕ$
27	26	peano2nnd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n + 1 \in ℕ$
28	27	nnrpd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n + 1 \in ℝ^{+}$
29	26	nnrpd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n \in ℝ^{+}$
30	28 29	rpdivcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{n + 1}{n} \in ℝ^{+}$
31	30	relogcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log (\frac{n + 1}{n}) \in ℝ$
32	31	recnd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log (\frac{n + 1}{n}) \in ℂ$
33	25 32	mulcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to y \log (\frac{n + 1}{n}) \in ℂ$
34	26	nncnd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n \in ℂ$
35	26	nnne0d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n \neq 0$
36	25 34 35	divcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{y}{n} \in ℂ$
37		1cnd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 1 \in ℂ$
38	36 37	addcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (\frac{y}{n}) + 1 \in ℂ$
39	24 26	dmgmdivn0	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (\frac{y}{n}) + 1 \neq 0$
40	38 39	logcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log ((\frac{y}{n}) + 1) \in ℂ$
41	33 40	subcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1) \in ℂ$
42	41	abscld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \in ℝ$
43	33	abscld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n})\| \in ℝ$
44	40	abscld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\log ((\frac{y}{n}) + 1)\| \in ℝ$
45	43 44	readdcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n})\| + \|\log ((\frac{y}{n}) + 1)\| \in ℝ$
46	7	nnred	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R \in ℝ$
47	46 31	remulcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R \log (\frac{n + 1}{n}) \in ℝ$
48	7	peano2nnd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R + 1 \in ℕ$
49	48	nnrpd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R + 1 \in ℝ^{+}$
50	49 29	rpmulcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (R + 1) n \in ℝ^{+}$
51	50	relogcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log (R + 1) n \in ℝ$
52		pire	$⊢ π \in ℝ$
53	52	a1i	$⊢ (φ \land (n \in ℕ \land y \in U)) \to π \in ℝ$
54	51 53	readdcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log (R + 1) n + π \in ℝ$
55	47 54	readdcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R \log (\frac{n + 1}{n}) + \log (R + 1) n + π \in ℝ$
56	33 40	abs2dif2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq \|y \log (\frac{n + 1}{n})\| + \|\log ((\frac{y}{n}) + 1)\|$
57	25 32	absmuld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n})\| = \|y\| \|\log (\frac{n + 1}{n})\|$
58	30	rpred	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{n + 1}{n} \in ℝ$
59	34	mulid2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 1 n = n$
60	26	nnred	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n \in ℝ$
61	60	lep1d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n \leq n + 1$
62	59 61	eqbrtrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 1 n \leq n + 1$
63		1red	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 1 \in ℝ$
64	60 63	readdcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n + 1 \in ℝ$
65	63 64 29	lemuldivd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (1 n \leq n + 1 \leftrightarrow 1 \leq \frac{n + 1}{n})$
66	62 65	mpbid	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 1 \leq \frac{n + 1}{n}$
67	58 66	logge0d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 0 \leq \log (\frac{n + 1}{n})$
68	31 67	absidd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\log (\frac{n + 1}{n})\| = \log (\frac{n + 1}{n})$
69	68	oveq2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y\| \|\log (\frac{n + 1}{n})\| = \|y\| \log (\frac{n + 1}{n})$
70	57 69	eqtrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n})\| = \|y\| \log (\frac{n + 1}{n})$
71	25	abscld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y\| \in ℝ$
72		fveq2	$⊢ x = y \to \|x\| = \|y\|$
73	72	breq1d	$⊢ x = y \to (\|x\| \leq R \leftrightarrow \|y\| \leq R)$
74		fvoveq1	$⊢ x = y \to \|x + k\| = \|y + k\|$
75	74	breq2d	$⊢ x = y \to (\frac{1}{R} \leq \|x + k\| \leftrightarrow \frac{1}{R} \leq \|y + k\|)$
76	75	ralbidv	$⊢ x = y \to (\forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\| \leftrightarrow \forall k \in ℕ_{0} \frac{1}{R} \leq \|y + k\|)$
77	73 76	anbi12d	$⊢ x = y \to ((\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|) \leftrightarrow (\|y\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|y + k\|))$
78	77 2	elrab2	$⊢ y \in U \leftrightarrow (y \in ℂ \land (\|y\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|y + k\|))$
79	78	simprbi	$⊢ y \in U \to (\|y\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|y + k\|)$
80	79	ad2antll	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (\|y\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|y + k\|)$
81	80	simpld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y\| \leq R$
82	71 46 31 67 81	lemul1ad	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y\| \log (\frac{n + 1}{n}) \leq R \log (\frac{n + 1}{n})$
83	70 82	eqbrtrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n})\| \leq R \log (\frac{n + 1}{n})$
84	38 39	absrpcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|(\frac{y}{n}) + 1\| \in ℝ^{+}$
85	84	relogcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log \|(\frac{y}{n}) + 1\| \in ℝ$
86	85	recnd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log \|(\frac{y}{n}) + 1\| \in ℂ$
87	86	abscld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\log \|(\frac{y}{n}) + 1\|\| \in ℝ$
88	87 53	readdcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\log \|(\frac{y}{n}) + 1\|\| + π \in ℝ$
89		abslogle	$⊢ ((\frac{y}{n}) + 1 \in ℂ \land (\frac{y}{n}) + 1 \neq 0) \to \|\log ((\frac{y}{n}) + 1)\| \leq \|\log \|(\frac{y}{n}) + 1\|\| + π$
90	38 39 89	syl2anc	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\log ((\frac{y}{n}) + 1)\| \leq \|\log \|(\frac{y}{n}) + 1\|\| + π$
91		1rp	$⊢ 1 \in ℝ^{+}$
92		relogdiv	$⊢ (1 \in ℝ^{+} \land (R + 1) n \in ℝ^{+}) \to \log (\frac{1}{(R + 1) n}) = \log 1 - \log (R + 1) n$
93	91 50 92	sylancr	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log (\frac{1}{(R + 1) n}) = \log 1 - \log (R + 1) n$
94		log1	$⊢ \log 1 = 0$
95	94	oveq1i	$⊢ \log 1 - \log (R + 1) n = 0 - \log (R + 1) n$
96		df-neg	$⊢ - \log (R + 1) n = 0 - \log (R + 1) n$
97	95 96	eqtr4i	$⊢ \log 1 - \log (R + 1) n = - \log (R + 1) n$
98	93 97	eqtr2di	$⊢ (φ \land (n \in ℕ \land y \in U)) \to - \log (R + 1) n = \log (\frac{1}{(R + 1) n})$
99	48	nnrecred	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{1}{R + 1} \in ℝ$
100	25 34	addcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to y + n \in ℂ$
101	100	abscld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y + n\| \in ℝ$
102	7	nnrecred	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{1}{R} \in ℝ$
103	7	nnrpd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R \in ℝ^{+}$
104		0le1	$⊢ 0 \leq 1$
105	104	a1i	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 0 \leq 1$
106	46	lep1d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R \leq R + 1$
107	103 49 63 105 106	lediv2ad	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{1}{R + 1} \leq \frac{1}{R}$
108		oveq2	$⊢ k = n \to y + k = y + n$
109	108	fveq2d	$⊢ k = n \to \|y + k\| = \|y + n\|$
110	109	breq2d	$⊢ k = n \to (\frac{1}{R} \leq \|y + k\| \leftrightarrow \frac{1}{R} \leq \|y + n\|)$
111	80	simprd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \forall k \in ℕ_{0} \frac{1}{R} \leq \|y + k\|$
112	26	nnnn0d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to n \in ℕ_{0}$
113	110 111 112	rspcdva	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{1}{R} \leq \|y + n\|$
114	99 102 101 107 113	letrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{1}{R + 1} \leq \|y + n\|$
115	99 101 29 114	lediv1dd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{\frac{1}{R + 1}}{n} \leq \frac{\|y + n\|}{n}$
116	48	nncnd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R + 1 \in ℂ$
117	48	nnne0d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R + 1 \neq 0$
118	116 34 117 35	recdiv2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{\frac{1}{R + 1}}{n} = \frac{1}{(R + 1) n}$
119	25 34 34 35	divdird	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{y + n}{n} = (\frac{y}{n}) + (\frac{n}{n})$
120	34 35	dividd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{n}{n} = 1$
121	120	oveq2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (\frac{y}{n}) + (\frac{n}{n}) = (\frac{y}{n}) + 1$
122	119 121	eqtr2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (\frac{y}{n}) + 1 = \frac{y + n}{n}$
123	122	fveq2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|(\frac{y}{n}) + 1\| = \|\frac{y + n}{n}\|$
124	100 34 35	absdivd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\frac{y + n}{n}\| = \frac{\|y + n\|}{\|n\|}$
125	29	rpge0d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 0 \leq n$
126	60 125	absidd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|n\| = n$
127	126	oveq2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{\|y + n\|}{\|n\|} = \frac{\|y + n\|}{n}$
128	123 124 127	3eqtrrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{\|y + n\|}{n} = \|(\frac{y}{n}) + 1\|$
129	115 118 128	3brtr3d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{1}{(R + 1) n} \leq \|(\frac{y}{n}) + 1\|$
130	50	rpreccld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{1}{(R + 1) n} \in ℝ^{+}$
131	130 84	logled	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (\frac{1}{(R + 1) n} \leq \|(\frac{y}{n}) + 1\| \leftrightarrow \log (\frac{1}{(R + 1) n}) \leq \log \|(\frac{y}{n}) + 1\|)$
132	129 131	mpbid	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log (\frac{1}{(R + 1) n}) \leq \log \|(\frac{y}{n}) + 1\|$
133	98 132	eqbrtrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to - \log (R + 1) n \leq \log \|(\frac{y}{n}) + 1\|$
134	38	abscld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|(\frac{y}{n}) + 1\| \in ℝ$
135	46 63	readdcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R + 1 \in ℝ$
136	50	rpred	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (R + 1) n \in ℝ$
137	36	abscld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\frac{y}{n}\| \in ℝ$
138	137 63	readdcld	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\frac{y}{n}\| + 1 \in ℝ$
139	36 37	abstrid	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|(\frac{y}{n}) + 1\| \leq \|\frac{y}{n}\| + \|1\|$
140		abs1	$⊢ \|1\| = 1$
141	140	oveq2i	$⊢ \|\frac{y}{n}\| + \|1\| = \|\frac{y}{n}\| + 1$
142	139 141	breqtrdi	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|(\frac{y}{n}) + 1\| \leq \|\frac{y}{n}\| + 1$
143	91	a1i	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 1 \in ℝ^{+}$
144	25	absge0d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 0 \leq \|y\|$
145	26	nnge1d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 1 \leq n$
146	71 46 143 60 144 81 145	lediv12ad	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{\|y\|}{n} \leq \frac{R}{1}$
147	25 34 35	absdivd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\frac{y}{n}\| = \frac{\|y\|}{\|n\|}$
148	126	oveq2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{\|y\|}{\|n\|} = \frac{\|y\|}{n}$
149	147 148	eqtr2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{\|y\|}{n} = \|\frac{y}{n}\|$
150	7	nncnd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R \in ℂ$
151	150	div1d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \frac{R}{1} = R$
152	146 149 151	3brtr3d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\frac{y}{n}\| \leq R$
153	137 46 63 152	leadd1dd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\frac{y}{n}\| + 1 \leq R + 1$
154	134 138 135 142 153	letrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|(\frac{y}{n}) + 1\| \leq R + 1$
155	49	rpge0d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to 0 \leq R + 1$
156	135 60 155 145	lemulge11d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to R + 1 \leq (R + 1) n$
157	134 135 136 154 156	letrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|(\frac{y}{n}) + 1\| \leq (R + 1) n$
158	84 50	logled	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (\|(\frac{y}{n}) + 1\| \leq (R + 1) n \leftrightarrow \log \|(\frac{y}{n}) + 1\| \leq \log (R + 1) n)$
159	157 158	mpbid	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \log \|(\frac{y}{n}) + 1\| \leq \log (R + 1) n$
160	85 51	absled	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (\|\log \|(\frac{y}{n}) + 1\|\| \leq \log (R + 1) n \leftrightarrow (- \log (R + 1) n \leq \log \|(\frac{y}{n}) + 1\| \land \log \|(\frac{y}{n}) + 1\| \leq \log (R + 1) n))$
161	133 159 160	mpbir2and	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\log \|(\frac{y}{n}) + 1\|\| \leq \log (R + 1) n$
162	87 51 53 161	leadd1dd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\log \|(\frac{y}{n}) + 1\|\| + π \leq \log (R + 1) n + π$
163	44 88 54 90 162	letrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|\log ((\frac{y}{n}) + 1)\| \leq \log (R + 1) n + π$
164	43 44 47 54 83 163	le2addd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n})\| + \|\log ((\frac{y}{n}) + 1)\| \leq R \log (\frac{n + 1}{n}) + \log (R + 1) n + π$
165	42 45 55 56 164	letrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq R \log (\frac{n + 1}{n}) + \log (R + 1) n + π$
166	165	adantr	$⊢ ((φ \land (n \in ℕ \land y \in U)) \land \neg 2 R \leq n) \to \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq R \log (\frac{n + 1}{n}) + \log (R + 1) n + π$
167	5 6 21 166	ifbothda	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\| \leq if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π)$
168		oveq1	$⊢ m = n \to m + 1 = n + 1$
169		id	$⊢ m = n \to m = n$
170	168 169	oveq12d	$⊢ m = n \to \frac{m + 1}{m} = \frac{n + 1}{n}$
171	170	fveq2d	$⊢ m = n \to \log (\frac{m + 1}{m}) = \log (\frac{n + 1}{n})$
172	171	oveq2d	$⊢ m = n \to z \log (\frac{m + 1}{m}) = z \log (\frac{n + 1}{n})$
173		oveq2	$⊢ m = n \to \frac{z}{m} = \frac{z}{n}$
174	173	fvoveq1d	$⊢ m = n \to \log ((\frac{z}{m}) + 1) = \log ((\frac{z}{n}) + 1)$
175	172 174	oveq12d	$⊢ m = n \to z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1) = z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)$
176	175	mpteq2dv	$⊢ m = n \to (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)) = (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1))$
177		cnex	$⊢ ℂ \in V$
178	2 177	rabex2	$⊢ U \in V$
179	178	mptex	$⊢ (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) \in V$
180	176 3 179	fvmpt	$⊢ n \in ℕ \to G (n) = (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1))$
181	180	ad2antrl	$⊢ (φ \land (n \in ℕ \land y \in U)) \to G (n) = (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1))$
182	181	fveq1d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to G (n) (y) = (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) (y)$
183		oveq1	$⊢ z = y \to z \log (\frac{n + 1}{n}) = y \log (\frac{n + 1}{n})$
184		oveq1	$⊢ z = y \to \frac{z}{n} = \frac{y}{n}$
185	184	fvoveq1d	$⊢ z = y \to \log ((\frac{z}{n}) + 1) = \log ((\frac{y}{n}) + 1)$
186	183 185	oveq12d	$⊢ z = y \to z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1) = y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)$
187		eqid	$⊢ (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) = (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1))$
188		ovex	$⊢ y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1) \in V$
189	186 187 188	fvmpt	$⊢ y \in U \to (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) (y) = y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)$
190	189	ad2antll	$⊢ (φ \land (n \in ℕ \land y \in U)) \to (z \in U ⟼ z \log (\frac{n + 1}{n}) - \log ((\frac{z}{n}) + 1)) (y) = y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)$
191	182 190	eqtrd	$⊢ (φ \land (n \in ℕ \land y \in U)) \to G (n) (y) = y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)$
192	191	fveq2d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|G (n) (y)\| = \|y \log (\frac{n + 1}{n}) - \log ((\frac{y}{n}) + 1)\|$
193		breq2	$⊢ m = n \to (2 R \leq m \leftrightarrow 2 R \leq n)$
194		oveq1	$⊢ m = n \to m^{2} = n^{2}$
195	194	oveq2d	$⊢ m = n \to \frac{2 (R + 1)}{m^{2}} = \frac{2 (R + 1)}{n^{2}}$
196	195	oveq2d	$⊢ m = n \to R (\frac{2 (R + 1)}{m^{2}}) = R (\frac{2 (R + 1)}{n^{2}})$
197	171	oveq2d	$⊢ m = n \to R \log (\frac{m + 1}{m}) = R \log (\frac{n + 1}{n})$
198		oveq2	$⊢ m = n \to (R + 1) m = (R + 1) n$
199	198	fveq2d	$⊢ m = n \to \log (R + 1) m = \log (R + 1) n$
200	199	oveq1d	$⊢ m = n \to \log (R + 1) m + π = \log (R + 1) n + π$
201	197 200	oveq12d	$⊢ m = n \to R \log (\frac{m + 1}{m}) + \log (R + 1) m + π = R \log (\frac{n + 1}{n}) + \log (R + 1) n + π$
202	193 196 201	ifbieq12d	$⊢ m = n \to if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π) = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π)$
203		ovex	$⊢ R (\frac{2 (R + 1)}{n^{2}}) \in V$
204		ovex	$⊢ R \log (\frac{n + 1}{n}) + \log (R + 1) n + π \in V$
205	203 204	ifex	$⊢ if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π) \in V$
206	202 4 205	fvmpt	$⊢ n \in ℕ \to T (n) = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π)$
207	206	ad2antrl	$⊢ (φ \land (n \in ℕ \land y \in U)) \to T (n) = if (2 R \leq n, R (\frac{2 (R + 1)}{n^{2}}), R \log (\frac{n + 1}{n}) + \log (R + 1) n + π)$
208	167 192 207	3brtr4d	$⊢ (φ \land (n \in ℕ \land y \in U)) \to \|G (n) (y)\| \leq T (n)$

Metamath Proof Explorer

Theorem lgamgulmlem5

Proof