lgamgulmlem2

	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	lgamgulmlem2	$⊢ φ \to \|(\frac{A}{N}) - \log ((\frac{A}{N}) + 1)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{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.n	$⊢ φ \to N \in ℕ$
4		lgamgulm.a	$⊢ φ \to A \in U$
5		lgamgulm.l	$⊢ φ \to 2 R \leq N$
6		1elunit	$⊢ 1 \in [0, 1]$
7		0elunit	$⊢ 0 \in [0, 1]$
8		0red	$⊢ φ \to 0 \in ℝ$
9		1red	$⊢ φ \to 1 \in ℝ$
10		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
11	10	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
12	11	a1i	$⊢ φ \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
13	1 2	lgamgulmlem1	$⊢ φ \to U \subseteq ℂ ∖ (ℤ ∖ ℕ)$
14	13 4	sseldd	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
15	14	eldifad	$⊢ φ \to A \in ℂ$
16	3	nnred	$⊢ φ \to N \in ℝ$
17	16	recnd	$⊢ φ \to N \in ℂ$
18	3	nnne0d	$⊢ φ \to N \neq 0$
19	15 17 18	divcld	$⊢ φ \to \frac{A}{N} \in ℂ$
20		unitssre	$⊢ [0, 1] \subseteq ℝ$
21		ax-resscn	$⊢ ℝ \subseteq ℂ$
22	20 21	sstri	$⊢ [0, 1] \subseteq ℂ$
23	22	a1i	$⊢ φ \to [0, 1] \subseteq ℂ$
24		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
25		cncfmptc	$⊢ (\frac{A}{N} \in ℂ \land [0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [0, 1] ⟼ \frac{A}{N}) : [0, 1] \underset{cn}{⟶} ℂ$
26	19 23 24 25	syl3anc	$⊢ φ \to (t \in [0, 1] ⟼ \frac{A}{N}) : [0, 1] \underset{cn}{⟶} ℂ$
27		cncfmptid	$⊢ ([0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [0, 1] ⟼ t) : [0, 1] \underset{cn}{⟶} ℂ$
28	22 24 27	sylancr	$⊢ φ \to (t \in [0, 1] ⟼ t) : [0, 1] \underset{cn}{⟶} ℂ$
29	26 28	mulcncf	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t) : [0, 1] \underset{cn}{⟶} ℂ$
30		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
31	30	logcn	$⊢ ({log ↾}_{(ℂ ∖ (−∞, 0])}) : (ℂ ∖ (−∞, 0]) \underset{cn}{⟶} ℂ$
32	31	a1i	$⊢ φ \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) : (ℂ ∖ (−∞, 0]) \underset{cn}{⟶} ℂ$
33		cncff	$⊢ ({log ↾}_{(ℂ ∖ (−∞, 0])}) : (ℂ ∖ (−∞, 0]) \underset{cn}{⟶} ℂ \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) : ℂ ∖ (−∞, 0] ⟶ ℂ$
34	32 33	syl	$⊢ φ \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) : ℂ ∖ (−∞, 0] ⟶ ℂ$
35	19	adantr	$⊢ (φ \land t \in [0, 1]) \to \frac{A}{N} \in ℂ$
36		simpr	$⊢ (φ \land t \in [0, 1]) \to t \in [0, 1]$
37	20 36	sselid	$⊢ (φ \land t \in [0, 1]) \to t \in ℝ$
38	37	recnd	$⊢ (φ \land t \in [0, 1]) \to t \in ℂ$
39	35 38	mulcld	$⊢ (φ \land t \in [0, 1]) \to (\frac{A}{N}) t \in ℂ$
40		1cnd	$⊢ (φ \land t \in [0, 1]) \to 1 \in ℂ$
41	39 40	addcld	$⊢ (φ \land t \in [0, 1]) \to (\frac{A}{N}) t + 1 \in ℂ$
42		rere	$⊢ (\frac{A}{N}) t + 1 \in ℝ \to ℜ ((\frac{A}{N}) t + 1) = (\frac{A}{N}) t + 1$
43	42	adantl	$⊢ ((φ \land t \in [0, 1]) \land (\frac{A}{N}) t + 1 \in ℝ) \to ℜ ((\frac{A}{N}) t + 1) = (\frac{A}{N}) t + 1$
44	41	recld	$⊢ (φ \land t \in [0, 1]) \to ℜ ((\frac{A}{N}) t + 1) \in ℝ$
45	39	recld	$⊢ (φ \land t \in [0, 1]) \to ℜ ((\frac{A}{N}) t) \in ℝ$
46	45	recnd	$⊢ (φ \land t \in [0, 1]) \to ℜ ((\frac{A}{N}) t) \in ℂ$
47	46	abscld	$⊢ (φ \land t \in [0, 1]) \to \|ℜ ((\frac{A}{N}) t)\| \in ℝ$
48	39	abscld	$⊢ (φ \land t \in [0, 1]) \to \|(\frac{A}{N}) t\| \in ℝ$
49		1red	$⊢ (φ \land t \in [0, 1]) \to 1 \in ℝ$
50		absrele	$⊢ (\frac{A}{N}) t \in ℂ \to \|ℜ ((\frac{A}{N}) t)\| \leq \|(\frac{A}{N}) t\|$
51	39 50	syl	$⊢ (φ \land t \in [0, 1]) \to \|ℜ ((\frac{A}{N}) t)\| \leq \|(\frac{A}{N}) t\|$
52	49	rehalfcld	$⊢ (φ \land t \in [0, 1]) \to \frac{1}{2} \in ℝ$
53	1	nnred	$⊢ φ \to R \in ℝ$
54	53	adantr	$⊢ (φ \land t \in [0, 1]) \to R \in ℝ$
55	3	adantr	$⊢ (φ \land t \in [0, 1]) \to N \in ℕ$
56	54 55	nndivred	$⊢ (φ \land t \in [0, 1]) \to \frac{R}{N} \in ℝ$
57	19	abscld	$⊢ φ \to \|\frac{A}{N}\| \in ℝ$
58	57	adantr	$⊢ (φ \land t \in [0, 1]) \to \|\frac{A}{N}\| \in ℝ$
59	35	absge0d	$⊢ (φ \land t \in [0, 1]) \to 0 \leq \|\frac{A}{N}\|$
60		elicc01	$⊢ t \in [0, 1] \leftrightarrow (t \in ℝ \land 0 \leq t \land t \leq 1)$
61	60	simp2bi	$⊢ t \in [0, 1] \to 0 \leq t$
62	61	adantl	$⊢ (φ \land t \in [0, 1]) \to 0 \leq t$
63	15 17 18	absdivd	$⊢ φ \to \|\frac{A}{N}\| = \frac{\|A\|}{\|N\|}$
64	3	nnrpd	$⊢ φ \to N \in ℝ^{+}$
65	64	rpge0d	$⊢ φ \to 0 \leq N$
66	16 65	absidd	$⊢ φ \to \|N\| = N$
67	66	oveq2d	$⊢ φ \to \frac{\|A\|}{\|N\|} = \frac{\|A\|}{N}$
68	63 67	eqtr2d	$⊢ φ \to \frac{\|A\|}{N} = \|\frac{A}{N}\|$
69	15	abscld	$⊢ φ \to \|A\| \in ℝ$
70		fveq2	$⊢ x = A \to \|x\| = \|A\|$
71	70	breq1d	$⊢ x = A \to (\|x\| \leq R \leftrightarrow \|A\| \leq R)$
72		fvoveq1	$⊢ x = A \to \|x + k\| = \|A + k\|$
73	72	breq2d	$⊢ x = A \to (\frac{1}{R} \leq \|x + k\| \leftrightarrow \frac{1}{R} \leq \|A + k\|)$
74	73	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\|)$
75	71 74	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\|))$
76	75 2	elrab2	$⊢ A \in U \leftrightarrow (A \in ℂ \land (\|A\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|A + k\|))$
77	76	simprbi	$⊢ A \in U \to (\|A\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|A + k\|)$
78	4 77	syl	$⊢ φ \to (\|A\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|A + k\|)$
79	78	simpld	$⊢ φ \to \|A\| \leq R$
80	69 53 64 79	lediv1dd	$⊢ φ \to \frac{\|A\|}{N} \leq \frac{R}{N}$
81	68 80	eqbrtrrd	$⊢ φ \to \|\frac{A}{N}\| \leq \frac{R}{N}$
82	81	adantr	$⊢ (φ \land t \in [0, 1]) \to \|\frac{A}{N}\| \leq \frac{R}{N}$
83	60	simp3bi	$⊢ t \in [0, 1] \to t \leq 1$
84	83	adantl	$⊢ (φ \land t \in [0, 1]) \to t \leq 1$
85	58 56 37 49 59 62 82 84	lemul12ad	$⊢ (φ \land t \in [0, 1]) \to \|\frac{A}{N}\| t \leq (\frac{R}{N}) \cdot 1$
86	35 38	absmuld	$⊢ (φ \land t \in [0, 1]) \to \|(\frac{A}{N}) t\| = \|\frac{A}{N}\| \|t\|$
87	37 62	absidd	$⊢ (φ \land t \in [0, 1]) \to \|t\| = t$
88	87	oveq2d	$⊢ (φ \land t \in [0, 1]) \to \|\frac{A}{N}\| \|t\| = \|\frac{A}{N}\| t$
89	86 88	eqtr2d	$⊢ (φ \land t \in [0, 1]) \to \|\frac{A}{N}\| t = \|(\frac{A}{N}) t\|$
90	56	recnd	$⊢ (φ \land t \in [0, 1]) \to \frac{R}{N} \in ℂ$
91	90	mulridd	$⊢ (φ \land t \in [0, 1]) \to (\frac{R}{N}) \cdot 1 = \frac{R}{N}$
92	85 89 91	3brtr3d	$⊢ (φ \land t \in [0, 1]) \to \|(\frac{A}{N}) t\| \leq \frac{R}{N}$
93		2rp	$⊢ 2 \in ℝ^{+}$
94	93	a1i	$⊢ φ \to 2 \in ℝ^{+}$
95	53 16 94	lemuldiv2d	$⊢ φ \to (2 R \leq N \leftrightarrow R \leq \frac{N}{2})$
96	5 95	mpbid	$⊢ φ \to R \leq \frac{N}{2}$
97		2cnd	$⊢ φ \to 2 \in ℂ$
98		2ne0	$⊢ 2 \neq 0$
99	98	a1i	$⊢ φ \to 2 \neq 0$
100	17 97 99	divrecd	$⊢ φ \to \frac{N}{2} = N (\frac{1}{2})$
101	96 100	breqtrd	$⊢ φ \to R \leq N (\frac{1}{2})$
102	9	rehalfcld	$⊢ φ \to \frac{1}{2} \in ℝ$
103	53 102 64	ledivmuld	$⊢ φ \to (\frac{R}{N} \leq \frac{1}{2} \leftrightarrow R \leq N (\frac{1}{2}))$
104	101 103	mpbird	$⊢ φ \to \frac{R}{N} \leq \frac{1}{2}$
105	104	adantr	$⊢ (φ \land t \in [0, 1]) \to \frac{R}{N} \leq \frac{1}{2}$
106	48 56 52 92 105	letrd	$⊢ (φ \land t \in [0, 1]) \to \|(\frac{A}{N}) t\| \leq \frac{1}{2}$
107		halflt1	$⊢ \frac{1}{2} < 1$
108	107	a1i	$⊢ (φ \land t \in [0, 1]) \to \frac{1}{2} < 1$
109	48 52 49 106 108	lelttrd	$⊢ (φ \land t \in [0, 1]) \to \|(\frac{A}{N}) t\| < 1$
110	47 48 49 51 109	lelttrd	$⊢ (φ \land t \in [0, 1]) \to \|ℜ ((\frac{A}{N}) t)\| < 1$
111	45 49	absltd	$⊢ (φ \land t \in [0, 1]) \to (\|ℜ ((\frac{A}{N}) t)\| < 1 \leftrightarrow (- 1 < ℜ ((\frac{A}{N}) t) \land ℜ ((\frac{A}{N}) t) < 1))$
112	110 111	mpbid	$⊢ (φ \land t \in [0, 1]) \to (- 1 < ℜ ((\frac{A}{N}) t) \land ℜ ((\frac{A}{N}) t) < 1)$
113	112	simpld	$⊢ (φ \land t \in [0, 1]) \to - 1 < ℜ ((\frac{A}{N}) t)$
114	49	renegcld	$⊢ (φ \land t \in [0, 1]) \to - 1 \in ℝ$
115	114 45	posdifd	$⊢ (φ \land t \in [0, 1]) \to (- 1 < ℜ ((\frac{A}{N}) t) \leftrightarrow 0 < ℜ ((\frac{A}{N}) t) - -1)$
116	113 115	mpbid	$⊢ (φ \land t \in [0, 1]) \to 0 < ℜ ((\frac{A}{N}) t) - -1$
117	46 40	subnegd	$⊢ (φ \land t \in [0, 1]) \to ℜ ((\frac{A}{N}) t) - -1 = ℜ ((\frac{A}{N}) t) + 1$
118	116 117	breqtrd	$⊢ (φ \land t \in [0, 1]) \to 0 < ℜ ((\frac{A}{N}) t) + 1$
119	39 40	readdd	$⊢ (φ \land t \in [0, 1]) \to ℜ ((\frac{A}{N}) t + 1) = ℜ ((\frac{A}{N}) t) + ℜ (1)$
120		re1	$⊢ ℜ (1) = 1$
121	120	oveq2i	$⊢ ℜ ((\frac{A}{N}) t) + ℜ (1) = ℜ ((\frac{A}{N}) t) + 1$
122	119 121	eqtrdi	$⊢ (φ \land t \in [0, 1]) \to ℜ ((\frac{A}{N}) t + 1) = ℜ ((\frac{A}{N}) t) + 1$
123	118 122	breqtrrd	$⊢ (φ \land t \in [0, 1]) \to 0 < ℜ ((\frac{A}{N}) t + 1)$
124	44 123	elrpd	$⊢ (φ \land t \in [0, 1]) \to ℜ ((\frac{A}{N}) t + 1) \in ℝ^{+}$
125	124	adantr	$⊢ ((φ \land t \in [0, 1]) \land (\frac{A}{N}) t + 1 \in ℝ) \to ℜ ((\frac{A}{N}) t + 1) \in ℝ^{+}$
126	43 125	eqeltrrd	$⊢ ((φ \land t \in [0, 1]) \land (\frac{A}{N}) t + 1 \in ℝ) \to (\frac{A}{N}) t + 1 \in ℝ^{+}$
127	126	ex	$⊢ (φ \land t \in [0, 1]) \to ((\frac{A}{N}) t + 1 \in ℝ \to (\frac{A}{N}) t + 1 \in ℝ^{+})$
128	30	ellogdm	$⊢ (\frac{A}{N}) t + 1 \in (ℂ ∖ (−∞, 0]) \leftrightarrow ((\frac{A}{N}) t + 1 \in ℂ \land ((\frac{A}{N}) t + 1 \in ℝ \to (\frac{A}{N}) t + 1 \in ℝ^{+}))$
129	41 127 128	sylanbrc	$⊢ (φ \land t \in [0, 1]) \to (\frac{A}{N}) t + 1 \in (ℂ ∖ (−∞, 0])$
130	34 129	cofmpt	$⊢ φ \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) \circ (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) = (t \in [0, 1] ⟼ ({log ↾}_{(ℂ ∖ (−∞, 0])}) ((\frac{A}{N}) t + 1))$
131	129	fvresd	$⊢ (φ \land t \in [0, 1]) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) ((\frac{A}{N}) t + 1) = \log ((\frac{A}{N}) t + 1)$
132	131	mpteq2dva	$⊢ φ \to (t \in [0, 1] ⟼ ({log ↾}_{(ℂ ∖ (−∞, 0])}) ((\frac{A}{N}) t + 1)) = (t \in [0, 1] ⟼ \log ((\frac{A}{N}) t + 1))$
133	130 132	eqtrd	$⊢ φ \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) \circ (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) = (t \in [0, 1] ⟼ \log ((\frac{A}{N}) t + 1))$
134	129	fmpttd	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) : [0, 1] ⟶ ℂ ∖ (−∞, 0]$
135		difss	$⊢ ℂ ∖ (−∞, 0] \subseteq ℂ$
136	10	addcn	$⊢ + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
137	136	a1i	$⊢ φ \to + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
138		1cnd	$⊢ φ \to 1 \in ℂ$
139		cncfmptc	$⊢ (1 \in ℂ \land [0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [0, 1] ⟼ 1) : [0, 1] \underset{cn}{⟶} ℂ$
140	138 23 24 139	syl3anc	$⊢ φ \to (t \in [0, 1] ⟼ 1) : [0, 1] \underset{cn}{⟶} ℂ$
141	10 137 29 140	cncfmpt2f	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) : [0, 1] \underset{cn}{⟶} ℂ$
142		cncfcdm	$⊢ (ℂ ∖ (−∞, 0] \subseteq ℂ \land (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) : [0, 1] \underset{cn}{⟶} ℂ) \to ((t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) : [0, 1] \underset{cn}{⟶} (ℂ ∖ (−∞, 0]) \leftrightarrow (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) : [0, 1] ⟶ ℂ ∖ (−∞, 0])$
143	135 141 142	sylancr	$⊢ φ \to ((t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) : [0, 1] \underset{cn}{⟶} (ℂ ∖ (−∞, 0]) \leftrightarrow (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) : [0, 1] ⟶ ℂ ∖ (−∞, 0])$
144	134 143	mpbird	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1) : [0, 1] \underset{cn}{⟶} (ℂ ∖ (−∞, 0])$
145	144 32	cncfco	$⊢ φ \to (({log ↾}_{(ℂ ∖ (−∞, 0])}) \circ (t \in [0, 1] ⟼ (\frac{A}{N}) t + 1)) : [0, 1] \underset{cn}{⟶} ℂ$
146	133 145	eqeltrrd	$⊢ φ \to (t \in [0, 1] ⟼ \log ((\frac{A}{N}) t + 1)) : [0, 1] \underset{cn}{⟶} ℂ$
147	10 12 29 146	cncfmpt2f	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) : [0, 1] \underset{cn}{⟶} ℂ$
148	21	a1i	$⊢ φ \to ℝ \subseteq ℂ$
149	20	a1i	$⊢ φ \to [0, 1] \subseteq ℝ$
150	30	logdmn0	$⊢ (\frac{A}{N}) t + 1 \in (ℂ ∖ (−∞, 0]) \to (\frac{A}{N}) t + 1 \neq 0$
151	129 150	syl	$⊢ (φ \land t \in [0, 1]) \to (\frac{A}{N}) t + 1 \neq 0$
152	41 151	logcld	$⊢ (φ \land t \in [0, 1]) \to \log ((\frac{A}{N}) t + 1) \in ℂ$
153	39 152	subcld	$⊢ (φ \land t \in [0, 1]) \to (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1) \in ℂ$
154		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
155		0re	$⊢ 0 \in ℝ$
156		iccntr	$⊢ (0 \in ℝ \land 1 \in ℝ) \to int (topGen (ran (.))) ([0, 1]) = (0, 1)$
157	155 9 156	sylancr	$⊢ φ \to int (topGen (ran (.))) ([0, 1]) = (0, 1)$
158	148 149 153 154 10 157	dvmptntr	$⊢ φ \to \frac{d (t \in [0, 1]⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} = \frac{d (t \in (0, 1)⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t}$
159		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
160	159	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
161	15	adantr	$⊢ (φ \land t \in (0, 1)) \to A \in ℂ$
162	17	adantr	$⊢ (φ \land t \in (0, 1)) \to N \in ℂ$
163	18	adantr	$⊢ (φ \land t \in (0, 1)) \to N \neq 0$
164	161 162 163	divcld	$⊢ (φ \land t \in (0, 1)) \to \frac{A}{N} \in ℂ$
165		ioossicc	$⊢ (0, 1) \subseteq [0, 1]$
166	165	sseli	$⊢ t \in (0, 1) \to t \in [0, 1]$
167	166 38	sylan2	$⊢ (φ \land t \in (0, 1)) \to t \in ℂ$
168	164 167	mulcld	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) t \in ℂ$
169	15	adantr	$⊢ (φ \land t \in ℝ) \to A \in ℂ$
170	17	adantr	$⊢ (φ \land t \in ℝ) \to N \in ℂ$
171	18	adantr	$⊢ (φ \land t \in ℝ) \to N \neq 0$
172	169 170 171	divcld	$⊢ (φ \land t \in ℝ) \to \frac{A}{N} \in ℂ$
173	148	sselda	$⊢ (φ \land t \in ℝ) \to t \in ℂ$
174	172 173	mulcld	$⊢ (φ \land t \in ℝ) \to (\frac{A}{N}) t \in ℂ$
175		1cnd	$⊢ (φ \land t \in ℝ) \to 1 \in ℂ$
176	160	dvmptid	$⊢ φ \to \frac{d (t \in ℝ⟼ t)}{d_{ℝ} t} = (t \in ℝ ⟼ 1)$
177	160 173 175 176 19	dvmptcmul	$⊢ φ \to \frac{d (t \in ℝ⟼ (\frac{A}{N}) t)}{d_{ℝ} t} = (t \in ℝ ⟼ (\frac{A}{N}) \cdot 1)$
178	19	mulridd	$⊢ φ \to (\frac{A}{N}) \cdot 1 = \frac{A}{N}$
179	178	mpteq2dv	$⊢ φ \to (t \in ℝ ⟼ (\frac{A}{N}) \cdot 1) = (t \in ℝ ⟼ \frac{A}{N})$
180	177 179	eqtrd	$⊢ φ \to \frac{d (t \in ℝ⟼ (\frac{A}{N}) t)}{d_{ℝ} t} = (t \in ℝ ⟼ \frac{A}{N})$
181	165 149	sstrid	$⊢ φ \to (0, 1) \subseteq ℝ$
182		retop	$⊢ topGen (ran (.)) \in Top$
183		iooretop	$⊢ (0, 1) \in topGen (ran (.))$
184		isopn3i	$⊢ (topGen (ran (.)) \in Top \land (0, 1) \in topGen (ran (.))) \to int (topGen (ran (.))) ((0, 1)) = (0, 1)$
185	182 183 184	mp2an	$⊢ int (topGen (ran (.))) ((0, 1)) = (0, 1)$
186	185	a1i	$⊢ φ \to int (topGen (ran (.))) ((0, 1)) = (0, 1)$
187	160 174 172 180 181 154 10 186	dvmptres2	$⊢ φ \to \frac{d (t \in (0, 1)⟼ (\frac{A}{N}) t)}{d_{ℝ} t} = (t \in (0, 1) ⟼ \frac{A}{N})$
188	166 152	sylan2	$⊢ (φ \land t \in (0, 1)) \to \log ((\frac{A}{N}) t + 1) \in ℂ$
189		1cnd	$⊢ (φ \land t \in (0, 1)) \to 1 \in ℂ$
190	168 189	addcld	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) t + 1 \in ℂ$
191	166 151	sylan2	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) t + 1 \neq 0$
192	190 191	reccld	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{(\frac{A}{N}) t + 1} \in ℂ$
193	192 164	mulcld	$⊢ (φ \land t \in (0, 1)) \to (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}) \in ℂ$
194		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
195	194	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
196	166 129	sylan2	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) t + 1 \in (ℂ ∖ (−∞, 0])$
197		eldifi	$⊢ y \in (ℂ ∖ (−∞, 0]) \to y \in ℂ$
198	197	adantl	$⊢ (φ \land y \in (ℂ ∖ (−∞, 0])) \to y \in ℂ$
199	30	logdmn0	$⊢ y \in (ℂ ∖ (−∞, 0]) \to y \neq 0$
200	199	adantl	$⊢ (φ \land y \in (ℂ ∖ (−∞, 0])) \to y \neq 0$
201	198 200	logcld	$⊢ (φ \land y \in (ℂ ∖ (−∞, 0])) \to \log y \in ℂ$
202	198 200	reccld	$⊢ (φ \land y \in (ℂ ∖ (−∞, 0])) \to \frac{1}{y} \in ℂ$
203	174 175	addcld	$⊢ (φ \land t \in ℝ) \to (\frac{A}{N}) t + 1 \in ℂ$
204		0cnd	$⊢ (φ \land t \in ℝ) \to 0 \in ℂ$
205	160 138	dvmptc	$⊢ φ \to \frac{d (t \in ℝ⟼ 1)}{d_{ℝ} t} = (t \in ℝ ⟼ 0)$
206	160 174 172 180 175 204 205	dvmptadd	$⊢ φ \to \frac{d (t \in ℝ⟼ (\frac{A}{N}) t + 1)}{d_{ℝ} t} = (t \in ℝ ⟼ (\frac{A}{N}) + 0)$
207	19	addridd	$⊢ φ \to (\frac{A}{N}) + 0 = \frac{A}{N}$
208	207	mpteq2dv	$⊢ φ \to (t \in ℝ ⟼ (\frac{A}{N}) + 0) = (t \in ℝ ⟼ \frac{A}{N})$
209	206 208	eqtrd	$⊢ φ \to \frac{d (t \in ℝ⟼ (\frac{A}{N}) t + 1)}{d_{ℝ} t} = (t \in ℝ ⟼ \frac{A}{N})$
210	160 203 172 209 181 154 10 186	dvmptres2	$⊢ φ \to \frac{d (t \in (0, 1)⟼ (\frac{A}{N}) t + 1)}{d_{ℝ} t} = (t \in (0, 1) ⟼ \frac{A}{N})$
211	34	feqmptd	$⊢ φ \to {log ↾}_{(ℂ ∖ (−∞, 0])} = (y \in (ℂ ∖ (−∞, 0]) ⟼ ({log ↾}_{(ℂ ∖ (−∞, 0])}) (y))$
212		fvres	$⊢ y \in (ℂ ∖ (−∞, 0]) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) (y) = \log y$
213	212	mpteq2ia	$⊢ (y \in (ℂ ∖ (−∞, 0]) ⟼ ({log ↾}_{(ℂ ∖ (−∞, 0])}) (y)) = (y \in (ℂ ∖ (−∞, 0]) ⟼ \log y)$
214	211 213	eqtr2di	$⊢ φ \to (y \in (ℂ ∖ (−∞, 0]) ⟼ \log y) = {log ↾}_{(ℂ ∖ (−∞, 0])}$
215	214	oveq2d	$⊢ φ \to \frac{d (y \in (ℂ ∖ (−∞, 0])⟼ \log y)}{d_{ℂ} y} = ℂ D ({log ↾}_{(ℂ ∖ (−∞, 0])})$
216	30	dvlog	$⊢ ℂ D ({log ↾}_{(ℂ ∖ (−∞, 0])}) = (y \in (ℂ ∖ (−∞, 0]) ⟼ \frac{1}{y})$
217	215 216	eqtrdi	$⊢ φ \to \frac{d (y \in (ℂ ∖ (−∞, 0])⟼ \log y)}{d_{ℂ} y} = (y \in (ℂ ∖ (−∞, 0]) ⟼ \frac{1}{y})$
218		fveq2	$⊢ y = (\frac{A}{N}) t + 1 \to \log y = \log ((\frac{A}{N}) t + 1)$
219		oveq2	$⊢ y = (\frac{A}{N}) t + 1 \to \frac{1}{y} = \frac{1}{(\frac{A}{N}) t + 1}$
220	160 195 196 164 201 202 210 217 218 219	dvmptco	$⊢ φ \to \frac{d (t \in (0, 1)⟼ \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} = (t \in (0, 1) ⟼ (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}))$
221	160 168 164 187 188 193 220	dvmptsub	$⊢ φ \to \frac{d (t \in (0, 1)⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} = (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}))$
222	158 221	eqtrd	$⊢ φ \to \frac{d (t \in [0, 1]⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} = (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}))$
223	222	dmeqd	$⊢ φ \to dom \frac{d (t \in [0, 1]⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} = dom (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}))$
224		ovex	$⊢ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}) \in V$
225		eqid	$⊢ (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) = (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}))$
226	224 225	dmmpti	$⊢ dom (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) = (0, 1)$
227	223 226	eqtrdi	$⊢ φ \to dom \frac{d (t \in [0, 1]⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} = (0, 1)$
228		2re	$⊢ 2 \in ℝ$
229	228	a1i	$⊢ φ \to 2 \in ℝ$
230	229 53	remulcld	$⊢ φ \to 2 R \in ℝ$
231	1	nnrpd	$⊢ φ \to R \in ℝ^{+}$
232	53 231	ltaddrpd	$⊢ φ \to R < R + R$
233	53	recnd	$⊢ φ \to R \in ℂ$
234	233	2timesd	$⊢ φ \to 2 R = R + R$
235	232 234	breqtrrd	$⊢ φ \to R < 2 R$
236	53 230 16 235 5	ltletrd	$⊢ φ \to R < N$
237		difrp	$⊢ (R \in ℝ \land N \in ℝ) \to (R < N \leftrightarrow N - R \in ℝ^{+})$
238	53 16 237	syl2anc	$⊢ φ \to (R < N \leftrightarrow N - R \in ℝ^{+})$
239	236 238	mpbid	$⊢ φ \to N - R \in ℝ^{+}$
240	239	rprecred	$⊢ φ \to \frac{1}{N - R} \in ℝ$
241	3	nnrecred	$⊢ φ \to \frac{1}{N} \in ℝ$
242	240 241	resubcld	$⊢ φ \to (\frac{1}{N - R}) - (\frac{1}{N}) \in ℝ$
243	53 242	remulcld	$⊢ φ \to R ((\frac{1}{N - R}) - (\frac{1}{N})) \in ℝ$
244	222	fveq1d	$⊢ φ \to \frac{d (t \in [0, 1]⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} (y) = (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)$
245	244	fveq2d	$⊢ φ \to \|\frac{d (t \in [0, 1]⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} (y)\| = \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\|$
246	245	adantr	$⊢ (φ \land y \in (0, 1)) \to \|\frac{d (t \in [0, 1]⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} (y)\| = \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\|$
247		nfv	$⊢ Ⅎ t (φ \land y \in (0, 1))$
248		nfcv	$⊢ \underline{Ⅎ} t abs$
249		nffvmpt1	$⊢ \underline{Ⅎ} t (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)$
250	248 249	nffv	$⊢ \underline{Ⅎ} t \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\|$
251		nfcv	$⊢ \underline{Ⅎ} t \leq$
252		nfcv	$⊢ \underline{Ⅎ} t R ((\frac{1}{N - R}) - (\frac{1}{N}))$
253	250 251 252	nfbr	$⊢ Ⅎ t \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N}))$
254	247 253	nfim	$⊢ Ⅎ t ((φ \land y \in (0, 1)) \to \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N})))$
255		eleq1w	$⊢ t = y \to (t \in (0, 1) \leftrightarrow y \in (0, 1))$
256	255	anbi2d	$⊢ t = y \to ((φ \land t \in (0, 1)) \leftrightarrow (φ \land y \in (0, 1)))$
257		2fveq3	$⊢ t = y \to \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (t)\| = \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\|$
258	257	breq1d	$⊢ t = y \to (\|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (t)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N})) \leftrightarrow \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N})))$
259	256 258	imbi12d	$⊢ t = y \to (((φ \land t \in (0, 1)) \to \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (t)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N}))) \leftrightarrow ((φ \land y \in (0, 1)) \to \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N}))))$
260		simpr	$⊢ (φ \land t \in (0, 1)) \to t \in (0, 1)$
261	225	fvmpt2	$⊢ (t \in (0, 1) \land (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}) \in V) \to (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (t) = (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})$
262	260 224 261	sylancl	$⊢ (φ \land t \in (0, 1)) \to (t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (t) = (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})$
263	262	fveq2d	$⊢ (φ \land t \in (0, 1)) \to \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (t)\| = \|(\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})\|$
264	164 189 192	subdid	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) (1 - (\frac{1}{(\frac{A}{N}) t + 1})) = (\frac{A}{N}) \cdot 1 - (\frac{A}{N}) (\frac{1}{(\frac{A}{N}) t + 1})$
265	164	mulridd	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) \cdot 1 = \frac{A}{N}$
266	164 192	mulcomd	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) (\frac{1}{(\frac{A}{N}) t + 1}) = (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})$
267	265 266	oveq12d	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) \cdot 1 - (\frac{A}{N}) (\frac{1}{(\frac{A}{N}) t + 1}) = (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})$
268	264 267	eqtr2d	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N}) = (\frac{A}{N}) (1 - (\frac{1}{(\frac{A}{N}) t + 1}))$
269	268	fveq2d	$⊢ (φ \land t \in (0, 1)) \to \|(\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})\| = \|(\frac{A}{N}) (1 - (\frac{1}{(\frac{A}{N}) t + 1}))\|$
270	161 162 163	absdivd	$⊢ (φ \land t \in (0, 1)) \to \|\frac{A}{N}\| = \frac{\|A\|}{\|N\|}$
271	16	adantr	$⊢ (φ \land t \in (0, 1)) \to N \in ℝ$
272	65	adantr	$⊢ (φ \land t \in (0, 1)) \to 0 \leq N$
273	271 272	absidd	$⊢ (φ \land t \in (0, 1)) \to \|N\| = N$
274	273	oveq2d	$⊢ (φ \land t \in (0, 1)) \to \frac{\|A\|}{\|N\|} = \frac{\|A\|}{N}$
275	270 274	eqtrd	$⊢ (φ \land t \in (0, 1)) \to \|\frac{A}{N}\| = \frac{\|A\|}{N}$
276	275	oveq1d	$⊢ (φ \land t \in (0, 1)) \to \|\frac{A}{N}\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| = (\frac{\|A\|}{N}) \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|$
277	189 192	subcld	$⊢ (φ \land t \in (0, 1)) \to 1 - (\frac{1}{(\frac{A}{N}) t + 1}) \in ℂ$
278	164 277	absmuld	$⊢ (φ \land t \in (0, 1)) \to \|(\frac{A}{N}) (1 - (\frac{1}{(\frac{A}{N}) t + 1}))\| = \|\frac{A}{N}\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|$
279	69	adantr	$⊢ (φ \land t \in (0, 1)) \to \|A\| \in ℝ$
280	279	recnd	$⊢ (φ \land t \in (0, 1)) \to \|A\| \in ℂ$
281	277	abscld	$⊢ (φ \land t \in (0, 1)) \to \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| \in ℝ$
282	281	recnd	$⊢ (φ \land t \in (0, 1)) \to \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| \in ℂ$
283	280 282 162 163	div23d	$⊢ (φ \land t \in (0, 1)) \to \frac{\|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|}{N} = (\frac{\|A\|}{N}) \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|$
284	276 278 283	3eqtr4d	$⊢ (φ \land t \in (0, 1)) \to \|(\frac{A}{N}) (1 - (\frac{1}{(\frac{A}{N}) t + 1}))\| = \frac{\|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|}{N}$
285	263 269 284	3eqtrd	$⊢ (φ \land t \in (0, 1)) \to \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (t)\| = \frac{\|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|}{N}$
286	53	adantr	$⊢ (φ \land t \in (0, 1)) \to R \in ℝ$
287	240	adantr	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{N - R} \in ℝ$
288	241	adantr	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{N} \in ℝ$
289	287 288	resubcld	$⊢ (φ \land t \in (0, 1)) \to (\frac{1}{N - R}) - (\frac{1}{N}) \in ℝ$
290	271 289	remulcld	$⊢ (φ \land t \in (0, 1)) \to N ((\frac{1}{N - R}) - (\frac{1}{N})) \in ℝ$
291	15	absge0d	$⊢ φ \to 0 \leq \|A\|$
292	291	adantr	$⊢ (φ \land t \in (0, 1)) \to 0 \leq \|A\|$
293	277	absge0d	$⊢ (φ \land t \in (0, 1)) \to 0 \leq \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|$
294	79	adantr	$⊢ (φ \land t \in (0, 1)) \to \|A\| \leq R$
295	239	adantr	$⊢ (φ \land t \in (0, 1)) \to N - R \in ℝ^{+}$
296	231	adantr	$⊢ (φ \land t \in (0, 1)) \to R \in ℝ^{+}$
297	295 296	rpdivcld	$⊢ (φ \land t \in (0, 1)) \to \frac{N - R}{R} \in ℝ^{+}$
298	14	dmgmn0	$⊢ φ \to A \neq 0$
299	298	adantr	$⊢ (φ \land t \in (0, 1)) \to A \neq 0$
300	161 162 299 163	divne0d	$⊢ (φ \land t \in (0, 1)) \to \frac{A}{N} \neq 0$
301		eliooord	$⊢ t \in (0, 1) \to (0 < t \land t < 1)$
302	301	adantl	$⊢ (φ \land t \in (0, 1)) \to (0 < t \land t < 1)$
303	302	simpld	$⊢ (φ \land t \in (0, 1)) \to 0 < t$
304	303	gt0ne0d	$⊢ (φ \land t \in (0, 1)) \to t \neq 0$
305	164 167 300 304	mulne0d	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) t \neq 0$
306	168 305	reccld	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{(\frac{A}{N}) t} \in ℂ$
307	189 306	addcld	$⊢ (φ \land t \in (0, 1)) \to 1 + (\frac{1}{(\frac{A}{N}) t}) \in ℂ$
308	168 189 168 305	divdird	$⊢ (φ \land t \in (0, 1)) \to \frac{(\frac{A}{N}) t + 1}{(\frac{A}{N}) t} = (\frac{(\frac{A}{N}) t}{(\frac{A}{N}) t}) + (\frac{1}{(\frac{A}{N}) t})$
309	168 305	dividd	$⊢ (φ \land t \in (0, 1)) \to \frac{(\frac{A}{N}) t}{(\frac{A}{N}) t} = 1$
310	309	oveq1d	$⊢ (φ \land t \in (0, 1)) \to (\frac{(\frac{A}{N}) t}{(\frac{A}{N}) t}) + (\frac{1}{(\frac{A}{N}) t}) = 1 + (\frac{1}{(\frac{A}{N}) t})$
311	308 310	eqtrd	$⊢ (φ \land t \in (0, 1)) \to \frac{(\frac{A}{N}) t + 1}{(\frac{A}{N}) t} = 1 + (\frac{1}{(\frac{A}{N}) t})$
312	190 168 191 305	divne0d	$⊢ (φ \land t \in (0, 1)) \to \frac{(\frac{A}{N}) t + 1}{(\frac{A}{N}) t} \neq 0$
313	311 312	eqnetrrd	$⊢ (φ \land t \in (0, 1)) \to 1 + (\frac{1}{(\frac{A}{N}) t}) \neq 0$
314	307 313	absrpcld	$⊢ (φ \land t \in (0, 1)) \to \|1 + (\frac{1}{(\frac{A}{N}) t})\| \in ℝ^{+}$
315		1red	$⊢ (φ \land t \in (0, 1)) \to 1 \in ℝ$
316		0le1	$⊢ 0 \leq 1$
317	316	a1i	$⊢ (φ \land t \in (0, 1)) \to 0 \leq 1$
318	297	rpred	$⊢ (φ \land t \in (0, 1)) \to \frac{N - R}{R} \in ℝ$
319	306	negcld	$⊢ (φ \land t \in (0, 1)) \to - \frac{1}{(\frac{A}{N}) t} \in ℂ$
320	319	abscld	$⊢ (φ \land t \in (0, 1)) \to \|- \frac{1}{(\frac{A}{N}) t}\| \in ℝ$
321	320 315	resubcld	$⊢ (φ \land t \in (0, 1)) \to \|- \frac{1}{(\frac{A}{N}) t}\| - 1 \in ℝ$
322	307	abscld	$⊢ (φ \land t \in (0, 1)) \to \|1 + (\frac{1}{(\frac{A}{N}) t})\| \in ℝ$
323	233	adantr	$⊢ (φ \land t \in (0, 1)) \to R \in ℂ$
324	296	rpne0d	$⊢ (φ \land t \in (0, 1)) \to R \neq 0$
325	162 323 323 324	divsubdird	$⊢ (φ \land t \in (0, 1)) \to \frac{N - R}{R} = (\frac{N}{R}) - (\frac{R}{R})$
326	323 324	dividd	$⊢ (φ \land t \in (0, 1)) \to \frac{R}{R} = 1$
327	326	oveq2d	$⊢ (φ \land t \in (0, 1)) \to (\frac{N}{R}) - (\frac{R}{R}) = (\frac{N}{R}) - 1$
328	325 327	eqtrd	$⊢ (φ \land t \in (0, 1)) \to \frac{N - R}{R} = (\frac{N}{R}) - 1$
329	271 296	rerpdivcld	$⊢ (φ \land t \in (0, 1)) \to \frac{N}{R} \in ℝ$
330	323 162 324 163	recdivd	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{\frac{R}{N}} = \frac{N}{R}$
331	166 92	sylan2	$⊢ (φ \land t \in (0, 1)) \to \|(\frac{A}{N}) t\| \leq \frac{R}{N}$
332	168 305	absrpcld	$⊢ (φ \land t \in (0, 1)) \to \|(\frac{A}{N}) t\| \in ℝ^{+}$
333	64	adantr	$⊢ (φ \land t \in (0, 1)) \to N \in ℝ^{+}$
334	296 333	rpdivcld	$⊢ (φ \land t \in (0, 1)) \to \frac{R}{N} \in ℝ^{+}$
335	332 334	lerecd	$⊢ (φ \land t \in (0, 1)) \to (\|(\frac{A}{N}) t\| \leq \frac{R}{N} \leftrightarrow \frac{1}{\frac{R}{N}} \leq \frac{1}{\|(\frac{A}{N}) t\|})$
336	331 335	mpbid	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{\frac{R}{N}} \leq \frac{1}{\|(\frac{A}{N}) t\|}$
337	330 336	eqbrtrrd	$⊢ (φ \land t \in (0, 1)) \to \frac{N}{R} \leq \frac{1}{\|(\frac{A}{N}) t\|}$
338	306	absnegd	$⊢ (φ \land t \in (0, 1)) \to \|- \frac{1}{(\frac{A}{N}) t}\| = \|\frac{1}{(\frac{A}{N}) t}\|$
339	189 168 305	absdivd	$⊢ (φ \land t \in (0, 1)) \to \|\frac{1}{(\frac{A}{N}) t}\| = \frac{\|1\|}{\|(\frac{A}{N}) t\|}$
340		abs1	$⊢ \|1\| = 1$
341	340	oveq1i	$⊢ \frac{\|1\|}{\|(\frac{A}{N}) t\|} = \frac{1}{\|(\frac{A}{N}) t\|}$
342	339 341	eqtrdi	$⊢ (φ \land t \in (0, 1)) \to \|\frac{1}{(\frac{A}{N}) t}\| = \frac{1}{\|(\frac{A}{N}) t\|}$
343	338 342	eqtrd	$⊢ (φ \land t \in (0, 1)) \to \|- \frac{1}{(\frac{A}{N}) t}\| = \frac{1}{\|(\frac{A}{N}) t\|}$
344	337 343	breqtrrd	$⊢ (φ \land t \in (0, 1)) \to \frac{N}{R} \leq \|- \frac{1}{(\frac{A}{N}) t}\|$
345	329 320 315 344	lesub1dd	$⊢ (φ \land t \in (0, 1)) \to (\frac{N}{R}) - 1 \leq \|- \frac{1}{(\frac{A}{N}) t}\| - 1$
346	328 345	eqbrtrd	$⊢ (φ \land t \in (0, 1)) \to \frac{N - R}{R} \leq \|- \frac{1}{(\frac{A}{N}) t}\| - 1$
347	340	oveq2i	$⊢ \|- \frac{1}{(\frac{A}{N}) t}\| - \|1\| = \|- \frac{1}{(\frac{A}{N}) t}\| - 1$
348	319 189	abs2difd	$⊢ (φ \land t \in (0, 1)) \to \|- \frac{1}{(\frac{A}{N}) t}\| - \|1\| \leq \|- (\frac{1}{(\frac{A}{N}) t}) - 1\|$
349	347 348	eqbrtrrid	$⊢ (φ \land t \in (0, 1)) \to \|- \frac{1}{(\frac{A}{N}) t}\| - 1 \leq \|- (\frac{1}{(\frac{A}{N}) t}) - 1\|$
350	189 306	addcomd	$⊢ (φ \land t \in (0, 1)) \to 1 + (\frac{1}{(\frac{A}{N}) t}) = (\frac{1}{(\frac{A}{N}) t}) + 1$
351	350	negeqd	$⊢ (φ \land t \in (0, 1)) \to - (1 + (\frac{1}{(\frac{A}{N}) t})) = - ((\frac{1}{(\frac{A}{N}) t}) + 1)$
352	306 189	negdi2d	$⊢ (φ \land t \in (0, 1)) \to - ((\frac{1}{(\frac{A}{N}) t}) + 1) = - (\frac{1}{(\frac{A}{N}) t}) - 1$
353	351 352	eqtrd	$⊢ (φ \land t \in (0, 1)) \to - (1 + (\frac{1}{(\frac{A}{N}) t})) = - (\frac{1}{(\frac{A}{N}) t}) - 1$
354	353	fveq2d	$⊢ (φ \land t \in (0, 1)) \to \|- (1 + (\frac{1}{(\frac{A}{N}) t}))\| = \|- (\frac{1}{(\frac{A}{N}) t}) - 1\|$
355	307	absnegd	$⊢ (φ \land t \in (0, 1)) \to \|- (1 + (\frac{1}{(\frac{A}{N}) t}))\| = \|1 + (\frac{1}{(\frac{A}{N}) t})\|$
356	354 355	eqtr3d	$⊢ (φ \land t \in (0, 1)) \to \|- (\frac{1}{(\frac{A}{N}) t}) - 1\| = \|1 + (\frac{1}{(\frac{A}{N}) t})\|$
357	349 356	breqtrd	$⊢ (φ \land t \in (0, 1)) \to \|- \frac{1}{(\frac{A}{N}) t}\| - 1 \leq \|1 + (\frac{1}{(\frac{A}{N}) t})\|$
358	318 321 322 346 357	letrd	$⊢ (φ \land t \in (0, 1)) \to \frac{N - R}{R} \leq \|1 + (\frac{1}{(\frac{A}{N}) t})\|$
359	297 314 315 317 358	lediv2ad	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{\|1 + (\frac{1}{(\frac{A}{N}) t})\|} \leq \frac{1}{\frac{N - R}{R}}$
360	17 233	subcld	$⊢ φ \to N - R \in ℂ$
361	360	adantr	$⊢ (φ \land t \in (0, 1)) \to N - R \in ℂ$
362	53 236	gtned	$⊢ φ \to N \neq R$
363	17 233 362	subne0d	$⊢ φ \to N - R \neq 0$
364	363	adantr	$⊢ (φ \land t \in (0, 1)) \to N - R \neq 0$
365	361 323 364 324	recdivd	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{\frac{N - R}{R}} = \frac{R}{N - R}$
366	162 323	nncand	$⊢ (φ \land t \in (0, 1)) \to N - (N - R) = R$
367	366	oveq1d	$⊢ (φ \land t \in (0, 1)) \to \frac{N - (N - R)}{N - R} = \frac{R}{N - R}$
368	162 361 361 364	divsubdird	$⊢ (φ \land t \in (0, 1)) \to \frac{N - (N - R)}{N - R} = (\frac{N}{N - R}) - (\frac{N - R}{N - R})$
369	367 368	eqtr3d	$⊢ (φ \land t \in (0, 1)) \to \frac{R}{N - R} = (\frac{N}{N - R}) - (\frac{N - R}{N - R})$
370	361 364	dividd	$⊢ (φ \land t \in (0, 1)) \to \frac{N - R}{N - R} = 1$
371	370	oveq2d	$⊢ (φ \land t \in (0, 1)) \to (\frac{N}{N - R}) - (\frac{N - R}{N - R}) = (\frac{N}{N - R}) - 1$
372	365 369 371	3eqtrd	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{\frac{N - R}{R}} = (\frac{N}{N - R}) - 1$
373	359 372	breqtrd	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{\|1 + (\frac{1}{(\frac{A}{N}) t})\|} \leq (\frac{N}{N - R}) - 1$
374	190 189 190 191	divsubdird	$⊢ (φ \land t \in (0, 1)) \to \frac{(\frac{A}{N}) t + 1 - 1}{(\frac{A}{N}) t + 1} = (\frac{(\frac{A}{N}) t + 1}{(\frac{A}{N}) t + 1}) - (\frac{1}{(\frac{A}{N}) t + 1})$
375	168 189	pncand	$⊢ (φ \land t \in (0, 1)) \to (\frac{A}{N}) t + 1 - 1 = (\frac{A}{N}) t$
376	375	oveq1d	$⊢ (φ \land t \in (0, 1)) \to \frac{(\frac{A}{N}) t + 1 - 1}{(\frac{A}{N}) t + 1} = \frac{(\frac{A}{N}) t}{(\frac{A}{N}) t + 1}$
377	190 191	dividd	$⊢ (φ \land t \in (0, 1)) \to \frac{(\frac{A}{N}) t + 1}{(\frac{A}{N}) t + 1} = 1$
378	377	oveq1d	$⊢ (φ \land t \in (0, 1)) \to (\frac{(\frac{A}{N}) t + 1}{(\frac{A}{N}) t + 1}) - (\frac{1}{(\frac{A}{N}) t + 1}) = 1 - (\frac{1}{(\frac{A}{N}) t + 1})$
379	374 376 378	3eqtr3rd	$⊢ (φ \land t \in (0, 1)) \to 1 - (\frac{1}{(\frac{A}{N}) t + 1}) = \frac{(\frac{A}{N}) t}{(\frac{A}{N}) t + 1}$
380	190 168 191 305	recdivd	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{\frac{(\frac{A}{N}) t + 1}{(\frac{A}{N}) t}} = \frac{(\frac{A}{N}) t}{(\frac{A}{N}) t + 1}$
381	311	oveq2d	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{\frac{(\frac{A}{N}) t + 1}{(\frac{A}{N}) t}} = \frac{1}{1 + (\frac{1}{(\frac{A}{N}) t})}$
382	379 380 381	3eqtr2d	$⊢ (φ \land t \in (0, 1)) \to 1 - (\frac{1}{(\frac{A}{N}) t + 1}) = \frac{1}{1 + (\frac{1}{(\frac{A}{N}) t})}$
383	382	fveq2d	$⊢ (φ \land t \in (0, 1)) \to \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| = \|\frac{1}{1 + (\frac{1}{(\frac{A}{N}) t})}\|$
384	189 307 313	absdivd	$⊢ (φ \land t \in (0, 1)) \to \|\frac{1}{1 + (\frac{1}{(\frac{A}{N}) t})}\| = \frac{\|1\|}{\|1 + (\frac{1}{(\frac{A}{N}) t})\|}$
385	340	oveq1i	$⊢ \frac{\|1\|}{\|1 + (\frac{1}{(\frac{A}{N}) t})\|} = \frac{1}{\|1 + (\frac{1}{(\frac{A}{N}) t})\|}$
386	384 385	eqtrdi	$⊢ (φ \land t \in (0, 1)) \to \|\frac{1}{1 + (\frac{1}{(\frac{A}{N}) t})}\| = \frac{1}{\|1 + (\frac{1}{(\frac{A}{N}) t})\|}$
387	383 386	eqtrd	$⊢ (φ \land t \in (0, 1)) \to \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| = \frac{1}{\|1 + (\frac{1}{(\frac{A}{N}) t})\|}$
388	360 363	reccld	$⊢ φ \to \frac{1}{N - R} \in ℂ$
389	388	adantr	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{N - R} \in ℂ$
390	241	recnd	$⊢ φ \to \frac{1}{N} \in ℂ$
391	390	adantr	$⊢ (φ \land t \in (0, 1)) \to \frac{1}{N} \in ℂ$
392	162 389 391	subdid	$⊢ (φ \land t \in (0, 1)) \to N ((\frac{1}{N - R}) - (\frac{1}{N})) = N (\frac{1}{N - R}) - N (\frac{1}{N})$
393	162 361 364	divrecd	$⊢ (φ \land t \in (0, 1)) \to \frac{N}{N - R} = N (\frac{1}{N - R})$
394	393	eqcomd	$⊢ (φ \land t \in (0, 1)) \to N (\frac{1}{N - R}) = \frac{N}{N - R}$
395	162 163	recidd	$⊢ (φ \land t \in (0, 1)) \to N (\frac{1}{N}) = 1$
396	394 395	oveq12d	$⊢ (φ \land t \in (0, 1)) \to N (\frac{1}{N - R}) - N (\frac{1}{N}) = (\frac{N}{N - R}) - 1$
397	392 396	eqtrd	$⊢ (φ \land t \in (0, 1)) \to N ((\frac{1}{N - R}) - (\frac{1}{N})) = (\frac{N}{N - R}) - 1$
398	373 387 397	3brtr4d	$⊢ (φ \land t \in (0, 1)) \to \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| \leq N ((\frac{1}{N - R}) - (\frac{1}{N}))$
399	279 286 281 290 292 293 294 398	lemul12ad	$⊢ (φ \land t \in (0, 1)) \to \|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| \leq R N ((\frac{1}{N - R}) - (\frac{1}{N}))$
400	242	recnd	$⊢ φ \to (\frac{1}{N - R}) - (\frac{1}{N}) \in ℂ$
401	400	adantr	$⊢ (φ \land t \in (0, 1)) \to (\frac{1}{N - R}) - (\frac{1}{N}) \in ℂ$
402	323 162 401	mul12d	$⊢ (φ \land t \in (0, 1)) \to R N ((\frac{1}{N - R}) - (\frac{1}{N})) = N R ((\frac{1}{N - R}) - (\frac{1}{N}))$
403	399 402	breqtrd	$⊢ (φ \land t \in (0, 1)) \to \|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| \leq N R ((\frac{1}{N - R}) - (\frac{1}{N}))$
404	279 281	remulcld	$⊢ (φ \land t \in (0, 1)) \to \|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| \in ℝ$
405	243	adantr	$⊢ (φ \land t \in (0, 1)) \to R ((\frac{1}{N - R}) - (\frac{1}{N})) \in ℝ$
406	404 405 333	ledivmuld	$⊢ (φ \land t \in (0, 1)) \to (\frac{\|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|}{N} \leq R ((\frac{1}{N - R}) - (\frac{1}{N})) \leftrightarrow \|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\| \leq N R ((\frac{1}{N - R}) - (\frac{1}{N})))$
407	403 406	mpbird	$⊢ (φ \land t \in (0, 1)) \to \frac{\|A\| \|1 - (\frac{1}{(\frac{A}{N}) t + 1})\|}{N} \leq R ((\frac{1}{N - R}) - (\frac{1}{N}))$
408	285 407	eqbrtrd	$⊢ (φ \land t \in (0, 1)) \to \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (t)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N}))$
409	254 259 408	chvarfv	$⊢ (φ \land y \in (0, 1)) \to \|(t \in (0, 1) ⟼ (\frac{A}{N}) - (\frac{1}{(\frac{A}{N}) t + 1}) (\frac{A}{N})) (y)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N}))$
410	246 409	eqbrtrd	$⊢ (φ \land y \in (0, 1)) \to \|\frac{d (t \in [0, 1]⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))}{d_{ℝ} t} (y)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N}))$
411	8 9 147 227 243 410	dvlip	$⊢ (φ \land (1 \in [0, 1] \land 0 \in [0, 1])) \to \|(t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (1) - (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (0)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N})) \|1 - 0\|$
412	6 7 411	mpanr12	$⊢ φ \to \|(t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (1) - (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (0)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N})) \|1 - 0\|$
413		eqidd	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) = (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1))$
414		oveq2	$⊢ t = 1 \to (\frac{A}{N}) t = (\frac{A}{N}) \cdot 1$
415	414 178	sylan9eqr	$⊢ (φ \land t = 1) \to (\frac{A}{N}) t = \frac{A}{N}$
416	415	fvoveq1d	$⊢ (φ \land t = 1) \to \log ((\frac{A}{N}) t + 1) = \log ((\frac{A}{N}) + 1)$
417	415 416	oveq12d	$⊢ (φ \land t = 1) \to (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1) = (\frac{A}{N}) - \log ((\frac{A}{N}) + 1)$
418	6	a1i	$⊢ φ \to 1 \in [0, 1]$
419		ovexd	$⊢ φ \to (\frac{A}{N}) - \log ((\frac{A}{N}) + 1) \in V$
420	413 417 418 419	fvmptd	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (1) = (\frac{A}{N}) - \log ((\frac{A}{N}) + 1)$
421		oveq2	$⊢ t = 0 \to (\frac{A}{N}) t = (\frac{A}{N}) \cdot 0$
422	19	mul01d	$⊢ φ \to (\frac{A}{N}) \cdot 0 = 0$
423	421 422	sylan9eqr	$⊢ (φ \land t = 0) \to (\frac{A}{N}) t = 0$
424	423	oveq1d	$⊢ (φ \land t = 0) \to (\frac{A}{N}) t + 1 = 0 + 1$
425		0p1e1	$⊢ 0 + 1 = 1$
426	424 425	eqtrdi	$⊢ (φ \land t = 0) \to (\frac{A}{N}) t + 1 = 1$
427	426	fveq2d	$⊢ (φ \land t = 0) \to \log ((\frac{A}{N}) t + 1) = \log 1$
428		log1	$⊢ \log 1 = 0$
429	427 428	eqtrdi	$⊢ (φ \land t = 0) \to \log ((\frac{A}{N}) t + 1) = 0$
430	423 429	oveq12d	$⊢ (φ \land t = 0) \to (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1) = 0 - 0$
431		0m0e0	$⊢ 0 - 0 = 0$
432	430 431	eqtrdi	$⊢ (φ \land t = 0) \to (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1) = 0$
433	7	a1i	$⊢ φ \to 0 \in [0, 1]$
434	413 432 433 433	fvmptd	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (0) = 0$
435	420 434	oveq12d	$⊢ φ \to (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (1) - (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (0) = (\frac{A}{N}) - \log ((\frac{A}{N}) + 1) - 0$
436	19 138	addcld	$⊢ φ \to (\frac{A}{N}) + 1 \in ℂ$
437	14 3	dmgmdivn0	$⊢ φ \to (\frac{A}{N}) + 1 \neq 0$
438	436 437	logcld	$⊢ φ \to \log ((\frac{A}{N}) + 1) \in ℂ$
439	19 438	subcld	$⊢ φ \to (\frac{A}{N}) - \log ((\frac{A}{N}) + 1) \in ℂ$
440	439	subid1d	$⊢ φ \to (\frac{A}{N}) - \log ((\frac{A}{N}) + 1) - 0 = (\frac{A}{N}) - \log ((\frac{A}{N}) + 1)$
441	435 440	eqtr2d	$⊢ φ \to (\frac{A}{N}) - \log ((\frac{A}{N}) + 1) = (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (1) - (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (0)$
442	441	fveq2d	$⊢ φ \to \|(\frac{A}{N}) - \log ((\frac{A}{N}) + 1)\| = \|(t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (1) - (t \in [0, 1] ⟼ (\frac{A}{N}) t - \log ((\frac{A}{N}) t + 1)) (0)\|$
443		1m0e1	$⊢ 1 - 0 = 1$
444	443	fveq2i	$⊢ \|1 - 0\| = \|1\|$
445	444 340	eqtri	$⊢ \|1 - 0\| = 1$
446	445	oveq2i	$⊢ R ((\frac{1}{N - R}) - (\frac{1}{N})) \|1 - 0\| = R ((\frac{1}{N - R}) - (\frac{1}{N})) \cdot 1$
447	233 400	mulcld	$⊢ φ \to R ((\frac{1}{N - R}) - (\frac{1}{N})) \in ℂ$
448	447	mulridd	$⊢ φ \to R ((\frac{1}{N - R}) - (\frac{1}{N})) \cdot 1 = R ((\frac{1}{N - R}) - (\frac{1}{N}))$
449	446 448	eqtr2id	$⊢ φ \to R ((\frac{1}{N - R}) - (\frac{1}{N})) = R ((\frac{1}{N - R}) - (\frac{1}{N})) \|1 - 0\|$
450	412 442 449	3brtr4d	$⊢ φ \to \|(\frac{A}{N}) - \log ((\frac{A}{N}) + 1)\| \leq R ((\frac{1}{N - R}) - (\frac{1}{N}))$

Metamath Proof Explorer

Theorem lgamgulmlem2

Proof