Theorem lgamgulmlem2

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	lgamgulmlem2	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) )

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