Theorem pntibndlem2

Description: Lemma for pntibnd . The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016)

	Ref	Expression
Hypotheses	pntibnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntibndlem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	pntibndlem1.l	⊢ 𝐿 = ( ( 1 / 4 ) / ( 𝐴 + 3 ) )
	pntibndlem3.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
	pntibndlem3.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	pntibndlem3.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) )
	pntibndlem3.c	⊢ 𝐶 = ( ( 2 · 𝐵 ) + ( log ‘ 2 ) )
	pntibndlem3.4	⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
	pntibndlem3.6	⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
	pntibndlem2.10	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	pntibndlem2.5	⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
	pntibndlem2.6	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 2 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑇 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
	pntibndlem2.7	⊢ 𝑋 = ( ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) + 𝑍 )
	pntibndlem2.8	⊢ ( 𝜑 → 𝑀 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) )
	pntibndlem2.9	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,) +∞ ) )
	pntibndlem2.11	⊢ ( 𝜑 → ( ( 𝑌 < 𝑁 ∧ 𝑁 ≤ ( ( 𝑀 / 2 ) · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ≤ ( 𝐸 / 2 ) ) )
Assertion	pntibndlem2	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ+ ( ( 𝑌 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑀 · 𝑌 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		pntibnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntibndlem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3		pntibndlem1.l	⊢ 𝐿 = ( ( 1 / 4 ) / ( 𝐴 + 3 ) )
4		pntibndlem3.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
5		pntibndlem3.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
6		pntibndlem3.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) )
7		pntibndlem3.c	⊢ 𝐶 = ( ( 2 · 𝐵 ) + ( log ‘ 2 ) )
8		pntibndlem3.4	⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
9		pntibndlem3.6	⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
10		pntibndlem2.10	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
11		pntibndlem2.5	⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
12		pntibndlem2.6	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 2 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑇 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
13		pntibndlem2.7	⊢ 𝑋 = ( ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) + 𝑍 )
14		pntibndlem2.8	⊢ ( 𝜑 → 𝑀 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) )
15		pntibndlem2.9	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,) +∞ ) )
16		pntibndlem2.11	⊢ ( 𝜑 → ( ( 𝑌 < 𝑁 ∧ 𝑁 ≤ ( ( 𝑀 / 2 ) · 𝑌 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ≤ ( 𝐸 / 2 ) ) )
17	10	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
18	16	simpld	⊢ ( 𝜑 → ( 𝑌 < 𝑁 ∧ 𝑁 ≤ ( ( 𝑀 / 2 ) · 𝑌 ) ) )
19	18	simpld	⊢ ( 𝜑 → 𝑌 < 𝑁 )
20		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
21		ioossre	⊢ ( 0 (,) 1 ) ⊆ ℝ
22	1 2 3	pntibndlem1	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
23	21 22	sselid	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
24	21 8	sselid	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
25	23 24	remulcld	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ )
26	20 25	readdcld	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ )
27	10	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
28	26 27	remulcld	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ∈ ℝ )
29		2re	⊢ 2 ∈ ℝ
30		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 2 · 𝑁 ) ∈ ℝ )
31	29 27 30	sylancr	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
32	5	rpred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
33		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · 𝐵 ) ∈ ℝ )
34	29 32 33	sylancr	⊢ ( 𝜑 → ( 2 · 𝐵 ) ∈ ℝ )
35		2rp	⊢ 2 ∈ ℝ+
36	35	a1i	⊢ ( 𝜑 → 2 ∈ ℝ+ )
37	36	relogcld	⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ )
38	34 37	readdcld	⊢ ( 𝜑 → ( ( 2 · 𝐵 ) + ( log ‘ 2 ) ) ∈ ℝ )
39	7 38	eqeltrid	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
40		eliooord	⊢ ( 𝐸 ∈ ( 0 (,) 1 ) → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
41	8 40	syl	⊢ ( 𝜑 → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
42	41	simpld	⊢ ( 𝜑 → 0 < 𝐸 )
43	24 42	elrpd	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
44	39 43	rerpdivcld	⊢ ( 𝜑 → ( 𝐶 / 𝐸 ) ∈ ℝ )
45	44	reefcld	⊢ ( 𝜑 → ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ )
46		pnfxr	⊢ +∞ ∈ ℝ*
47		icossre	⊢ ( ( ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ⊆ ℝ )
48	45 46 47	sylancl	⊢ ( 𝜑 → ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ⊆ ℝ )
49	48 14	sseldd	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
50		ioossre	⊢ ( 𝑋 (,) +∞ ) ⊆ ℝ
51	50 15	sselid	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
52	49 51	remulcld	⊢ ( 𝜑 → ( 𝑀 · 𝑌 ) ∈ ℝ )
53	29	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
54		eliooord	⊢ ( 𝐿 ∈ ( 0 (,) 1 ) → ( 0 < 𝐿 ∧ 𝐿 < 1 ) )
55	22 54	syl	⊢ ( 𝜑 → ( 0 < 𝐿 ∧ 𝐿 < 1 ) )
56	55	simpld	⊢ ( 𝜑 → 0 < 𝐿 )
57	23 56	elrpd	⊢ ( 𝜑 → 𝐿 ∈ ℝ+ )
58	57	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝐿 )
59	55	simprd	⊢ ( 𝜑 → 𝐿 < 1 )
60	43	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝐸 )
61	41	simprd	⊢ ( 𝜑 → 𝐸 < 1 )
62	23 20 24 20 58 59 60 61	ltmul12ad	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) < ( 1 · 1 ) )
63		1t1e1	⊢ ( 1 · 1 ) = 1
64	62 63	breqtrdi	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) < 1 )
65	25 20 20 64	ltadd2dd	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) < ( 1 + 1 ) )
66		df-2	⊢ 2 = ( 1 + 1 )
67	65 66	breqtrrdi	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) < 2 )
68	26 53 17 67	ltmul1dd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) < ( 2 · 𝑁 ) )
69	18	simprd	⊢ ( 𝜑 → 𝑁 ≤ ( ( 𝑀 / 2 ) · 𝑌 ) )
70	49	recnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
71	51	recnd	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
72		rpcnne0	⊢ ( 2 ∈ ℝ+ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
73	35 72	mp1i	⊢ ( 𝜑 → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
74		div23	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑀 · 𝑌 ) / 2 ) = ( ( 𝑀 / 2 ) · 𝑌 ) )
75	70 71 73 74	syl3anc	⊢ ( 𝜑 → ( ( 𝑀 · 𝑌 ) / 2 ) = ( ( 𝑀 / 2 ) · 𝑌 ) )
76	69 75	breqtrrd	⊢ ( 𝜑 → 𝑁 ≤ ( ( 𝑀 · 𝑌 ) / 2 ) )
77	27 52 36	lemuldiv2d	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ≤ ( 𝑀 · 𝑌 ) ↔ 𝑁 ≤ ( ( 𝑀 · 𝑌 ) / 2 ) ) )
78	76 77	mpbird	⊢ ( 𝜑 → ( 2 · 𝑁 ) ≤ ( 𝑀 · 𝑌 ) )
79	28 31 52 68 78	ltletrd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) < ( 𝑀 · 𝑌 ) )
80	1 2 3 4 5 6 7 8 2 10	pntibndlem2a	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) )
81	80	simp1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑢 ∈ ℝ )
82	17	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑁 ∈ ℝ+ )
83	80	simp2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑁 ≤ 𝑢 )
84	81 82 83	rpgecld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑢 ∈ ℝ+ )
85	1	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
86	85	ffvelcdmi	⊢ ( 𝑢 ∈ ℝ+ → ( 𝑅 ‘ 𝑢 ) ∈ ℝ )
87	84 86	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑅 ‘ 𝑢 ) ∈ ℝ )
88	87 84	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ∈ ℝ )
89	88	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ∈ ℂ )
90	89	abscld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ∈ ℝ )
91	85	ffvelcdmi	⊢ ( 𝑁 ∈ ℝ+ → ( 𝑅 ‘ 𝑁 ) ∈ ℝ )
92	17 91	syl	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑁 ) ∈ ℝ )
93	92 10	nndivred	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ∈ ℝ )
94	93	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ∈ ℝ )
95	94	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ∈ ℂ )
96	89 95	subcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ∈ ℂ )
97	96	abscld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ∈ ℝ )
98	95	abscld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
99	97 98	readdcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) + ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ∈ ℝ )
100	24	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝐸 ∈ ℝ )
101	89 95	abs2difd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) − ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ≤ ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) )
102	90 98 97	lesubaddd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) − ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ≤ ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) + ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ) )
103	101 102	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) + ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) )
104	100	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐸 / 2 ) ∈ ℝ )
105	27	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑁 ∈ ℝ )
106	81 105	resubcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 − 𝑁 ) ∈ ℝ )
107	106 82	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 − 𝑁 ) / 𝑁 ) ∈ ℝ )
108		3re	⊢ 3 ∈ ℝ
109	108	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 3 ∈ ℝ )
110	90 109	readdcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ∈ ℝ )
111	107 110	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) ∈ ℝ )
112	11	rpred	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
113	112	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑇 ∈ ℝ )
114		1red	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 1 ∈ ℝ )
115		4nn	⊢ 4 ∈ ℕ
116		nnrp	⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
117	115 116	mp1i	⊢ ( 𝜑 → 4 ∈ ℝ+ )
118	43 117	rpdivcld	⊢ ( 𝜑 → ( 𝐸 / 4 ) ∈ ℝ+ )
119	11 118	rpdivcld	⊢ ( 𝜑 → ( 𝑇 / ( 𝐸 / 4 ) ) ∈ ℝ+ )
120	119	rpred	⊢ ( 𝜑 → ( 𝑇 / ( 𝐸 / 4 ) ) ∈ ℝ )
121	120	reefcld	⊢ ( 𝜑 → ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) ∈ ℝ )
122	121	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) ∈ ℝ )
123		efgt1	⊢ ( ( 𝑇 / ( 𝐸 / 4 ) ) ∈ ℝ+ → 1 < ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) )
124	119 123	syl	⊢ ( 𝜑 → 1 < ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) )
125	124	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 1 < ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) )
126	9	rpred	⊢ ( 𝜑 → 𝑍 ∈ ℝ )
127	121 126	readdcld	⊢ ( 𝜑 → ( ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) + 𝑍 ) ∈ ℝ )
128	13 127	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
129	121 9	ltaddrpd	⊢ ( 𝜑 → ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) < ( ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) + 𝑍 ) )
130	129 13	breqtrrdi	⊢ ( 𝜑 → ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) < 𝑋 )
131		eliooord	⊢ ( 𝑌 ∈ ( 𝑋 (,) +∞ ) → ( 𝑋 < 𝑌 ∧ 𝑌 < +∞ ) )
132	15 131	syl	⊢ ( 𝜑 → ( 𝑋 < 𝑌 ∧ 𝑌 < +∞ ) )
133	132	simpld	⊢ ( 𝜑 → 𝑋 < 𝑌 )
134	121 128 51 130 133	lttrd	⊢ ( 𝜑 → ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) < 𝑌 )
135	121 51 27 134 19	lttrd	⊢ ( 𝜑 → ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) < 𝑁 )
136	135	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) < 𝑁 )
137	114 122 105 125 136	lttrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 1 < 𝑁 )
138	105 137	rplogcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( log ‘ 𝑁 ) ∈ ℝ+ )
139	113 138	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( log ‘ 𝑁 ) ) ∈ ℝ )
140	111 139	readdcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) ∈ ℝ )
141		peano2re	⊢ ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ∈ ℝ → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ∈ ℝ )
142	90 141	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ∈ ℝ )
143	107 142	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) ∈ ℝ )
144		chpcl	⊢ ( 𝑢 ∈ ℝ → ( ψ ‘ 𝑢 ) ∈ ℝ )
145	81 144	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ψ ‘ 𝑢 ) ∈ ℝ )
146		chpcl	⊢ ( 𝑁 ∈ ℝ → ( ψ ‘ 𝑁 ) ∈ ℝ )
147	105 146	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ψ ‘ 𝑁 ) ∈ ℝ )
148	145 147	resubcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ∈ ℝ )
149	148 82	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ∈ ℝ )
150	143 149	readdcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) ∈ ℝ )
151	107 90	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) ∈ ℝ )
152	92	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑅 ‘ 𝑁 ) ∈ ℝ )
153	87 152	resubcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ∈ ℝ )
154	153	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ∈ ℂ )
155	154	abscld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) ∈ ℝ )
156	155 82	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) ∈ ℝ )
157	151 156	readdcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) ) ∈ ℝ )
158	107 88	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ∈ ℝ )
159	158	renegcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ∈ ℝ )
160	159	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ∈ ℂ )
161	153 82	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ∈ ℝ )
162	161	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ∈ ℂ )
163	160 162	abstrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ) ) ≤ ( ( abs ‘ - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ) ) )
164	81	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑢 ∈ ℂ )
165	105	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑁 ∈ ℂ )
166	82	rpne0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑁 ≠ 0 )
167	164 165 165 166	divsubdird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 − 𝑁 ) / 𝑁 ) = ( ( 𝑢 / 𝑁 ) − ( 𝑁 / 𝑁 ) ) )
168	165 166	dividd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑁 / 𝑁 ) = 1 )
169	168	oveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 / 𝑁 ) − ( 𝑁 / 𝑁 ) ) = ( ( 𝑢 / 𝑁 ) − 1 ) )
170	167 169	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 − 𝑁 ) / 𝑁 ) = ( ( 𝑢 / 𝑁 ) − 1 ) )
171	170	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( ( ( 𝑢 / 𝑁 ) − 1 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) )
172	81 82	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 / 𝑁 ) ∈ ℝ )
173	172	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 / 𝑁 ) ∈ ℂ )
174		1cnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 1 ∈ ℂ )
175	173 174 89	subdird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 / 𝑁 ) − 1 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( ( ( 𝑢 / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) − ( 1 · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) )
176	84	rpcnne0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 ∈ ℂ ∧ 𝑢 ≠ 0 ) )
177	82	rpcnne0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
178	87	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑅 ‘ 𝑢 ) ∈ ℂ )
179		dmdcan	⊢ ( ( ( 𝑢 ∈ ℂ ∧ 𝑢 ≠ 0 ) ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑅 ‘ 𝑢 ) ∈ ℂ ) → ( ( 𝑢 / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) )
180	176 177 178 179	syl3anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) )
181	89	mullidd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 1 · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) )
182	180 181	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) − ( 1 · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) = ( ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) − ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) )
183	171 175 182	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) − ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) )
184	183	negeqd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = - ( ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) − ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) )
185	87 82	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) ∈ ℝ )
186	185	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) ∈ ℂ )
187	186 89	negsubdi2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → - ( ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) − ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) ) )
188	184 187	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) ) )
189	152	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑅 ‘ 𝑁 ) ∈ ℂ )
190	178 189 165 166	divsubdird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) = ( ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) )
191	188 190	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ) = ( ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) ) + ( ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) )
192	89 186 95	npncand	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) ) + ( ( ( 𝑅 ‘ 𝑢 ) / 𝑁 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) = ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) )
193	191 192	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ) = ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) )
194	193	fveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ) ) = ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) )
195	158	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ∈ ℂ )
196	195	absnegd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) = ( abs ‘ ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) )
197	107	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 − 𝑁 ) / 𝑁 ) ∈ ℂ )
198	197 89	absmuld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) = ( ( abs ‘ ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) )
199	81 105	subge0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 0 ≤ ( 𝑢 − 𝑁 ) ↔ 𝑁 ≤ 𝑢 ) )
200	83 199	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 0 ≤ ( 𝑢 − 𝑁 ) )
201	106 82 200	divge0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 0 ≤ ( ( 𝑢 − 𝑁 ) / 𝑁 ) )
202	107 201	absidd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) = ( ( 𝑢 − 𝑁 ) / 𝑁 ) )
203	202	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) = ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) )
204	196 198 203	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) = ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) )
205	154 165 166	absdivd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / ( abs ‘ 𝑁 ) ) )
206	82	rprege0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) )
207		absid	⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → ( abs ‘ 𝑁 ) = 𝑁 )
208	206 207	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ 𝑁 ) = 𝑁 )
209	208	oveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / ( abs ‘ 𝑁 ) ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) )
210	205 209	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) )
211	204 210	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ - ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) ) )
212	163 194 211	3brtr3d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ≤ ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) ) )
213	106 148	readdcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) ∈ ℝ )
214	213 82	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) / 𝑁 ) ∈ ℝ )
215	148	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ∈ ℂ )
216	165 164	subcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑁 − 𝑢 ) ∈ ℂ )
217	215 216	abstrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) + ( 𝑁 − 𝑢 ) ) ) ≤ ( ( abs ‘ ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) + ( abs ‘ ( 𝑁 − 𝑢 ) ) ) )
218	1	pntrval	⊢ ( 𝑢 ∈ ℝ+ → ( 𝑅 ‘ 𝑢 ) = ( ( ψ ‘ 𝑢 ) − 𝑢 ) )
219	84 218	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑅 ‘ 𝑢 ) = ( ( ψ ‘ 𝑢 ) − 𝑢 ) )
220	1	pntrval	⊢ ( 𝑁 ∈ ℝ+ → ( 𝑅 ‘ 𝑁 ) = ( ( ψ ‘ 𝑁 ) − 𝑁 ) )
221	82 220	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑅 ‘ 𝑁 ) = ( ( ψ ‘ 𝑁 ) − 𝑁 ) )
222	219 221	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) = ( ( ( ψ ‘ 𝑢 ) − 𝑢 ) − ( ( ψ ‘ 𝑁 ) − 𝑁 ) ) )
223	145	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ψ ‘ 𝑢 ) ∈ ℂ )
224	147	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ψ ‘ 𝑁 ) ∈ ℂ )
225		subadd4	⊢ ( ( ( ( ψ ‘ 𝑢 ) ∈ ℂ ∧ ( ψ ‘ 𝑁 ) ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) − ( 𝑢 − 𝑁 ) ) = ( ( ( ψ ‘ 𝑢 ) + 𝑁 ) − ( ( ψ ‘ 𝑁 ) + 𝑢 ) ) )
226		sub4	⊢ ( ( ( ( ψ ‘ 𝑢 ) ∈ ℂ ∧ ( ψ ‘ 𝑁 ) ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) − ( 𝑢 − 𝑁 ) ) = ( ( ( ψ ‘ 𝑢 ) − 𝑢 ) − ( ( ψ ‘ 𝑁 ) − 𝑁 ) ) )
227		addsub4	⊢ ( ( ( ( ψ ‘ 𝑢 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ ( ( ψ ‘ 𝑁 ) ∈ ℂ ∧ 𝑢 ∈ ℂ ) ) → ( ( ( ψ ‘ 𝑢 ) + 𝑁 ) − ( ( ψ ‘ 𝑁 ) + 𝑢 ) ) = ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) + ( 𝑁 − 𝑢 ) ) )
228	227	an42s	⊢ ( ( ( ( ψ ‘ 𝑢 ) ∈ ℂ ∧ ( ψ ‘ 𝑁 ) ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( ( ( ψ ‘ 𝑢 ) + 𝑁 ) − ( ( ψ ‘ 𝑁 ) + 𝑢 ) ) = ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) + ( 𝑁 − 𝑢 ) ) )
229	225 226 228	3eqtr3d	⊢ ( ( ( ( ψ ‘ 𝑢 ) ∈ ℂ ∧ ( ψ ‘ 𝑁 ) ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( ( ( ψ ‘ 𝑢 ) − 𝑢 ) − ( ( ψ ‘ 𝑁 ) − 𝑁 ) ) = ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) + ( 𝑁 − 𝑢 ) ) )
230	223 224 164 165 229	syl22anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ψ ‘ 𝑢 ) − 𝑢 ) − ( ( ψ ‘ 𝑁 ) − 𝑁 ) ) = ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) + ( 𝑁 − 𝑢 ) ) )
231	222 230	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) + ( 𝑁 − 𝑢 ) ) = ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) )
232	231	fveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) + ( 𝑁 − 𝑢 ) ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) )
233	106	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 − 𝑁 ) ∈ ℂ )
234		chpwordi	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ) → ( ψ ‘ 𝑁 ) ≤ ( ψ ‘ 𝑢 ) )
235	105 81 83 234	syl3anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ψ ‘ 𝑁 ) ≤ ( ψ ‘ 𝑢 ) )
236	147 145 235	abssubge0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) = ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) )
237	105 81 83	abssuble0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( 𝑁 − 𝑢 ) ) = ( 𝑢 − 𝑁 ) )
238	236 237	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) + ( abs ‘ ( 𝑁 − 𝑢 ) ) ) = ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) + ( 𝑢 − 𝑁 ) ) )
239	215 233 238	comraddd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) + ( abs ‘ ( 𝑁 − 𝑢 ) ) ) = ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) )
240	217 232 239	3brtr3d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) ≤ ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) )
241	155 213 82 240	lediv1dd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) ≤ ( ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) / 𝑁 ) )
242	156 214 151 241	leadd2dd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) ) ≤ ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) / 𝑁 ) ) )
243	151	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) ∈ ℂ )
244	149	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ∈ ℂ )
245	243 197 244	addassd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) ) )
246	90	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ∈ ℂ )
247	197 246 174	adddid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · 1 ) ) )
248	197	mulridd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · 1 ) = ( ( 𝑢 − 𝑁 ) / 𝑁 ) )
249	248	oveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · 1 ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) )
250	247 249	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) )
251	250	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) = ( ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) )
252	233 215 165 166	divdird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) / 𝑁 ) = ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) )
253	252	oveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) / 𝑁 ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) ) )
254	245 251 253	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( ( 𝑢 − 𝑁 ) + ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ) / 𝑁 ) ) )
255	242 254	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ) + ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) − ( 𝑅 ‘ 𝑁 ) ) ) / 𝑁 ) ) ≤ ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) )
256	97 157 150 212 255	letrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ≤ ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) )
257		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( ( 𝑢 − 𝑁 ) / 𝑁 ) ∈ ℝ ) → ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) ∈ ℝ )
258	29 107 257	sylancr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) ∈ ℝ )
259	258 139	readdcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) ∈ ℝ )
260		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( 𝑢 − 𝑁 ) ∈ ℝ ) → ( 2 · ( 𝑢 − 𝑁 ) ) ∈ ℝ )
261	29 106 260	sylancr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 2 · ( 𝑢 − 𝑁 ) ) ∈ ℝ )
262	105 138	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑁 / ( log ‘ 𝑁 ) ) ∈ ℝ )
263	113 262	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ∈ ℝ )
264	261 263	readdcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 2 · ( 𝑢 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) ∈ ℝ )
265		fveq2	⊢ ( 𝑦 = 𝑢 → ( ψ ‘ 𝑦 ) = ( ψ ‘ 𝑢 ) )
266	265	oveq1d	⊢ ( 𝑦 = 𝑢 → ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑁 ) ) = ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) )
267		oveq1	⊢ ( 𝑦 = 𝑢 → ( 𝑦 − 𝑁 ) = ( 𝑢 − 𝑁 ) )
268	267	oveq2d	⊢ ( 𝑦 = 𝑢 → ( 2 · ( 𝑦 − 𝑁 ) ) = ( 2 · ( 𝑢 − 𝑁 ) ) )
269	268	oveq1d	⊢ ( 𝑦 = 𝑢 → ( ( 2 · ( 𝑦 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) = ( ( 2 · ( 𝑢 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) )
270	266 269	breq12d	⊢ ( 𝑦 = 𝑢 → ( ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑁 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) ↔ ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ≤ ( ( 2 · ( 𝑢 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) ) )
271		id	⊢ ( 𝑥 = 𝑁 → 𝑥 = 𝑁 )
272		oveq2	⊢ ( 𝑥 = 𝑁 → ( 2 · 𝑥 ) = ( 2 · 𝑁 ) )
273	271 272	oveq12d	⊢ ( 𝑥 = 𝑁 → ( 𝑥 [,] ( 2 · 𝑥 ) ) = ( 𝑁 [,] ( 2 · 𝑁 ) ) )
274		fveq2	⊢ ( 𝑥 = 𝑁 → ( ψ ‘ 𝑥 ) = ( ψ ‘ 𝑁 ) )
275	274	oveq2d	⊢ ( 𝑥 = 𝑁 → ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) = ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑁 ) ) )
276		oveq2	⊢ ( 𝑥 = 𝑁 → ( 𝑦 − 𝑥 ) = ( 𝑦 − 𝑁 ) )
277	276	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 2 · ( 𝑦 − 𝑥 ) ) = ( 2 · ( 𝑦 − 𝑁 ) ) )
278		fveq2	⊢ ( 𝑥 = 𝑁 → ( log ‘ 𝑥 ) = ( log ‘ 𝑁 ) )
279	271 278	oveq12d	⊢ ( 𝑥 = 𝑁 → ( 𝑥 / ( log ‘ 𝑥 ) ) = ( 𝑁 / ( log ‘ 𝑁 ) ) )
280	279	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 𝑇 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) )
281	277 280	oveq12d	⊢ ( 𝑥 = 𝑁 → ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑇 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) = ( ( 2 · ( 𝑦 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) )
282	275 281	breq12d	⊢ ( 𝑥 = 𝑁 → ( ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑇 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ↔ ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑁 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) ) )
283	273 282	raleqbidv	⊢ ( 𝑥 = 𝑁 → ( ∀ 𝑦 ∈ ( 𝑥 [,] ( 2 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑇 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑦 ∈ ( 𝑁 [,] ( 2 · 𝑁 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑁 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) ) )
284	12	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ∀ 𝑥 ∈ ( 1 (,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 [,] ( 2 · 𝑥 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑥 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑥 ) ) + ( 𝑇 · ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
285		1xr	⊢ 1 ∈ ℝ*
286		elioopnf	⊢ ( 1 ∈ ℝ* → ( 𝑁 ∈ ( 1 (,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) ) )
287	285 286	ax-mp	⊢ ( 𝑁 ∈ ( 1 (,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) )
288	105 137 287	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑁 ∈ ( 1 (,) +∞ ) )
289	283 284 288	rspcdva	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ∀ 𝑦 ∈ ( 𝑁 [,] ( 2 · 𝑁 ) ) ( ( ψ ‘ 𝑦 ) − ( ψ ‘ 𝑁 ) ) ≤ ( ( 2 · ( 𝑦 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) )
290	28	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ∈ ℝ )
291	31	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 2 · 𝑁 ) ∈ ℝ )
292	80	simp3d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑢 ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) )
293		ltle	⊢ ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) < 2 → ( 1 + ( 𝐿 · 𝐸 ) ) ≤ 2 ) )
294	26 29 293	sylancl	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) < 2 → ( 1 + ( 𝐿 · 𝐸 ) ) ≤ 2 ) )
295	67 294	mpd	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ≤ 2 )
296	295	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 1 + ( 𝐿 · 𝐸 ) ) ≤ 2 )
297	26	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ )
298	29	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 2 ∈ ℝ )
299	297 298 82	lemul1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) ≤ 2 ↔ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ≤ ( 2 · 𝑁 ) ) )
300	296 299	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ≤ ( 2 · 𝑁 ) )
301	81 290 291 292 300	letrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑢 ≤ ( 2 · 𝑁 ) )
302		elicc2	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ) → ( 𝑢 ∈ ( 𝑁 [,] ( 2 · 𝑁 ) ) ↔ ( 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ( 2 · 𝑁 ) ) ) )
303	105 291 302	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 ∈ ( 𝑁 [,] ( 2 · 𝑁 ) ) ↔ ( 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ( 2 · 𝑁 ) ) ) )
304	81 83 301 303	mpbir3and	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑢 ∈ ( 𝑁 [,] ( 2 · 𝑁 ) ) )
305	270 289 304	rspcdva	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) ≤ ( ( 2 · ( 𝑢 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) )
306	148 264 82 305	lediv1dd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ≤ ( ( ( 2 · ( 𝑢 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) / 𝑁 ) )
307	261	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 2 · ( 𝑢 − 𝑁 ) ) ∈ ℂ )
308	11	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑇 ∈ ℝ+ )
309	308	rpred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑇 ∈ ℝ )
310	309 262	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ∈ ℝ )
311	310	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ∈ ℂ )
312		divdir	⊢ ( ( ( 2 · ( 𝑢 − 𝑁 ) ) ∈ ℂ ∧ ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ∈ ℂ ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( ( 2 · ( 𝑢 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) / 𝑁 ) = ( ( ( 2 · ( 𝑢 − 𝑁 ) ) / 𝑁 ) + ( ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) / 𝑁 ) ) )
313	307 311 177 312	syl3anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 2 · ( 𝑢 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) / 𝑁 ) = ( ( ( 2 · ( 𝑢 − 𝑁 ) ) / 𝑁 ) + ( ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) / 𝑁 ) ) )
314		2cnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 2 ∈ ℂ )
315	314 233 165 166	divassd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 2 · ( 𝑢 − 𝑁 ) ) / 𝑁 ) = ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) )
316	113	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝑇 ∈ ℂ )
317	138	rpcnne0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( log ‘ 𝑁 ) ∈ ℂ ∧ ( log ‘ 𝑁 ) ≠ 0 ) )
318		div12	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( ( log ‘ 𝑁 ) ∈ ℂ ∧ ( log ‘ 𝑁 ) ≠ 0 ) ) → ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) = ( 𝑁 · ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
319	316 165 317 318	syl3anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) = ( 𝑁 · ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
320	319	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) / 𝑁 ) = ( ( 𝑁 · ( 𝑇 / ( log ‘ 𝑁 ) ) ) / 𝑁 ) )
321	308 138	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( log ‘ 𝑁 ) ) ∈ ℝ+ )
322	321	rpcnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( log ‘ 𝑁 ) ) ∈ ℂ )
323	322 165 166	divcan3d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑁 · ( 𝑇 / ( log ‘ 𝑁 ) ) ) / 𝑁 ) = ( 𝑇 / ( log ‘ 𝑁 ) ) )
324	320 323	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) / 𝑁 ) = ( 𝑇 / ( log ‘ 𝑁 ) ) )
325	315 324	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 2 · ( 𝑢 − 𝑁 ) ) / 𝑁 ) + ( ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) / 𝑁 ) ) = ( ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
326	313 325	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 2 · ( 𝑢 − 𝑁 ) ) + ( 𝑇 · ( 𝑁 / ( log ‘ 𝑁 ) ) ) ) / 𝑁 ) = ( ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
327	306 326	breqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ≤ ( ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
328	149 259 143 327	leadd2dd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) ≤ ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) ) )
329	143	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) ∈ ℂ )
330	258	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) ∈ ℂ )
331	139	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( log ‘ 𝑁 ) ) ∈ ℂ )
332	329 330 331	addassd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) ) )
333		2cn	⊢ 2 ∈ ℂ
334		mulcom	⊢ ( ( 2 ∈ ℂ ∧ ( ( 𝑢 − 𝑁 ) / 𝑁 ) ∈ ℂ ) → ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) = ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · 2 ) )
335	333 197 334	sylancr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) = ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · 2 ) )
336	335	oveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · 2 ) ) )
337	142	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ∈ ℂ )
338	197 337 314	adddid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) + 2 ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · 2 ) ) )
339	246 174 314	addassd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) + 2 ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + ( 1 + 2 ) ) )
340		1p2e3	⊢ ( 1 + 2 ) = 3
341	340	oveq2i	⊢ ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + ( 1 + 2 ) ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 )
342	339 341	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) + 2 ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) )
343	342	oveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) + 2 ) ) = ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) )
344	336 338 343	3eqtr2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) ) = ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) )
345	344	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
346	332 345	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( 2 · ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) ) = ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
347	328 346	breqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 1 ) ) + ( ( ( ψ ‘ 𝑢 ) − ( ψ ‘ 𝑁 ) ) / 𝑁 ) ) ≤ ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
348	97 150 140 256 347	letrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ≤ ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) )
349	104	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝐸 / 2 ) / 2 ) ∈ ℝ )
350	81 297 82	ledivmul2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 / 𝑁 ) ≤ ( 1 + ( 𝐿 · 𝐸 ) ) ↔ 𝑢 ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) )
351	292 350	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 / 𝑁 ) ≤ ( 1 + ( 𝐿 · 𝐸 ) ) )
352		ax-1cn	⊢ 1 ∈ ℂ
353	25	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐿 · 𝐸 ) ∈ ℝ )
354	353	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐿 · 𝐸 ) ∈ ℂ )
355		addcom	⊢ ( ( 1 ∈ ℂ ∧ ( 𝐿 · 𝐸 ) ∈ ℂ ) → ( 1 + ( 𝐿 · 𝐸 ) ) = ( ( 𝐿 · 𝐸 ) + 1 ) )
356	352 354 355	sylancr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 1 + ( 𝐿 · 𝐸 ) ) = ( ( 𝐿 · 𝐸 ) + 1 ) )
357	351 356	breqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑢 / 𝑁 ) ≤ ( ( 𝐿 · 𝐸 ) + 1 ) )
358	172 114 353	lesubaddd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 / 𝑁 ) − 1 ) ≤ ( 𝐿 · 𝐸 ) ↔ ( 𝑢 / 𝑁 ) ≤ ( ( 𝐿 · 𝐸 ) + 1 ) ) )
359	357 358	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 / 𝑁 ) − 1 ) ≤ ( 𝐿 · 𝐸 ) )
360	170 359	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑢 − 𝑁 ) / 𝑁 ) ≤ ( 𝐿 · 𝐸 ) )
361	2	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝐴 ∈ ℝ+ )
362	361	rpred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝐴 ∈ ℝ )
363		fveq2	⊢ ( 𝑥 = 𝑢 → ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑢 ) )
364		id	⊢ ( 𝑥 = 𝑢 → 𝑥 = 𝑢 )
365	363 364	oveq12d	⊢ ( 𝑥 = 𝑢 → ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) = ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) )
366	365	fveq2d	⊢ ( 𝑥 = 𝑢 → ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) )
367	366	breq1d	⊢ ( 𝑥 = 𝑢 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐴 ) )
368	4	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
369	367 368 84	rspcdva	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐴 )
370	90 362 109 369	leadd1dd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ≤ ( 𝐴 + 3 ) )
371	107 201	jca	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) )
372		3rp	⊢ 3 ∈ ℝ+
373		rpaddcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( 𝐴 + 3 ) ∈ ℝ+ )
374	361 372 373	sylancl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐴 + 3 ) ∈ ℝ+ )
375	374	rprege0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝐴 + 3 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 + 3 ) ) )
376		lemul12b	⊢ ( ( ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑢 − 𝑁 ) / 𝑁 ) ) ∧ ( 𝐿 · 𝐸 ) ∈ ℝ ) ∧ ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ∈ ℝ ∧ ( ( 𝐴 + 3 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 + 3 ) ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) ≤ ( 𝐿 · 𝐸 ) ∧ ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ≤ ( 𝐴 + 3 ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) ≤ ( ( 𝐿 · 𝐸 ) · ( 𝐴 + 3 ) ) ) )
377	371 353 110 375 376	syl22anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) ≤ ( 𝐿 · 𝐸 ) ∧ ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ≤ ( 𝐴 + 3 ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) ≤ ( ( 𝐿 · 𝐸 ) · ( 𝐴 + 3 ) ) ) )
378	360 370 377	mp2and	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) ≤ ( ( 𝐿 · 𝐸 ) · ( 𝐴 + 3 ) ) )
379	43	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝐸 ∈ ℝ+ )
380	115 116	mp1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 4 ∈ ℝ+ )
381	379 380	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐸 / 4 ) ∈ ℝ+ )
382	381	rpcnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐸 / 4 ) ∈ ℂ )
383	374	rpcnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐴 + 3 ) ∈ ℂ )
384	374	rpne0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐴 + 3 ) ≠ 0 )
385	382 383 384	divcan1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝐸 / 4 ) / ( 𝐴 + 3 ) ) · ( 𝐴 + 3 ) ) = ( 𝐸 / 4 ) )
386	24	recnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
387	386	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 𝐸 ∈ ℂ )
388	380	rpcnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 4 ∈ ℂ )
389	380	rpne0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 4 ≠ 0 )
390	387 388 389	divrec2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐸 / 4 ) = ( ( 1 / 4 ) · 𝐸 ) )
391	390	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝐸 / 4 ) / ( 𝐴 + 3 ) ) = ( ( ( 1 / 4 ) · 𝐸 ) / ( 𝐴 + 3 ) ) )
392		4cn	⊢ 4 ∈ ℂ
393		4ne0	⊢ 4 ≠ 0
394	392 393	reccli	⊢ ( 1 / 4 ) ∈ ℂ
395	394	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 1 / 4 ) ∈ ℂ )
396	395 387 383 384	div23d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 1 / 4 ) · 𝐸 ) / ( 𝐴 + 3 ) ) = ( ( ( 1 / 4 ) / ( 𝐴 + 3 ) ) · 𝐸 ) )
397	3	oveq1i	⊢ ( 𝐿 · 𝐸 ) = ( ( ( 1 / 4 ) / ( 𝐴 + 3 ) ) · 𝐸 )
398	396 397	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 1 / 4 ) · 𝐸 ) / ( 𝐴 + 3 ) ) = ( 𝐿 · 𝐸 ) )
399	391 398	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐿 · 𝐸 ) = ( ( 𝐸 / 4 ) / ( 𝐴 + 3 ) ) )
400	399	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝐿 · 𝐸 ) · ( 𝐴 + 3 ) ) = ( ( ( 𝐸 / 4 ) / ( 𝐴 + 3 ) ) · ( 𝐴 + 3 ) ) )
401		2ne0	⊢ 2 ≠ 0
402	401	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → 2 ≠ 0 )
403	387 314 314 402 402	divdiv1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝐸 / 2 ) / 2 ) = ( 𝐸 / ( 2 · 2 ) ) )
404		2t2e4	⊢ ( 2 · 2 ) = 4
405	404	oveq2i	⊢ ( 𝐸 / ( 2 · 2 ) ) = ( 𝐸 / 4 )
406	403 405	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝐸 / 2 ) / 2 ) = ( 𝐸 / 4 ) )
407	385 400 406	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝐿 · 𝐸 ) · ( 𝐴 + 3 ) ) = ( ( 𝐸 / 2 ) / 2 ) )
408	378 407	breqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) ≤ ( ( 𝐸 / 2 ) / 2 ) )
409	120	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( 𝐸 / 4 ) ) ∈ ℝ )
410	138	rpred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( log ‘ 𝑁 ) ∈ ℝ )
411	82	reeflogd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( exp ‘ ( log ‘ 𝑁 ) ) = 𝑁 )
412	136 411	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) < ( exp ‘ ( log ‘ 𝑁 ) ) )
413		eflt	⊢ ( ( ( 𝑇 / ( 𝐸 / 4 ) ) ∈ ℝ ∧ ( log ‘ 𝑁 ) ∈ ℝ ) → ( ( 𝑇 / ( 𝐸 / 4 ) ) < ( log ‘ 𝑁 ) ↔ ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) < ( exp ‘ ( log ‘ 𝑁 ) ) ) )
414	409 410 413	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑇 / ( 𝐸 / 4 ) ) < ( log ‘ 𝑁 ) ↔ ( exp ‘ ( 𝑇 / ( 𝐸 / 4 ) ) ) < ( exp ‘ ( log ‘ 𝑁 ) ) ) )
415	412 414	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( 𝐸 / 4 ) ) < ( log ‘ 𝑁 ) )
416	409 410 415	ltled	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( 𝐸 / 4 ) ) ≤ ( log ‘ 𝑁 ) )
417	113 381 138 416	lediv23d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( log ‘ 𝑁 ) ) ≤ ( 𝐸 / 4 ) )
418	417 406	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑇 / ( log ‘ 𝑁 ) ) ≤ ( ( 𝐸 / 2 ) / 2 ) )
419	111 139 349 349 408 418	le2addd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) ≤ ( ( ( 𝐸 / 2 ) / 2 ) + ( ( 𝐸 / 2 ) / 2 ) ) )
420	104	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝐸 / 2 ) ∈ ℂ )
421	420	2halvesd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( 𝐸 / 2 ) / 2 ) + ( ( 𝐸 / 2 ) / 2 ) ) = ( 𝐸 / 2 ) )
422	419 421	breqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( ( ( 𝑢 − 𝑁 ) / 𝑁 ) · ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) + 3 ) ) + ( 𝑇 / ( log ‘ 𝑁 ) ) ) ≤ ( 𝐸 / 2 ) )
423	97 140 104 348 422	letrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ≤ ( 𝐸 / 2 ) )
424	16	simprd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ≤ ( 𝐸 / 2 ) )
425	424	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ≤ ( 𝐸 / 2 ) )
426	97 98 104 104 423 425	le2addd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) + ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ≤ ( ( 𝐸 / 2 ) + ( 𝐸 / 2 ) ) )
427	387	2halvesd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝐸 / 2 ) + ( 𝐸 / 2 ) ) = 𝐸 )
428	426 427	breqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( abs ‘ ( ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) − ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) + ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ) ≤ 𝐸 )
429	90 99 100 103 428	letrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 )
430	429	ralrimiva	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 )
431	19 79 430	jca31	⊢ ( 𝜑 → ( ( 𝑌 < 𝑁 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) < ( 𝑀 · 𝑌 ) ) ∧ ∀ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
432		breq2	⊢ ( 𝑧 = 𝑁 → ( 𝑌 < 𝑧 ↔ 𝑌 < 𝑁 ) )
433		oveq2	⊢ ( 𝑧 = 𝑁 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) = ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) )
434	433	breq1d	⊢ ( 𝑧 = 𝑁 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑀 · 𝑌 ) ↔ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) < ( 𝑀 · 𝑌 ) ) )
435	432 434	anbi12d	⊢ ( 𝑧 = 𝑁 → ( ( 𝑌 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑀 · 𝑌 ) ) ↔ ( 𝑌 < 𝑁 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) < ( 𝑀 · 𝑌 ) ) ) )
436		id	⊢ ( 𝑧 = 𝑁 → 𝑧 = 𝑁 )
437	436 433	oveq12d	⊢ ( 𝑧 = 𝑁 → ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) = ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) )
438	437	raleqdv	⊢ ( 𝑧 = 𝑁 → ( ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ↔ ∀ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
439	435 438	anbi12d	⊢ ( 𝑧 = 𝑁 → ( ( ( 𝑌 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑀 · 𝑌 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ( ( 𝑌 < 𝑁 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) < ( 𝑀 · 𝑌 ) ) ∧ ∀ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
440	439	rspcev	⊢ ( ( 𝑁 ∈ ℝ+ ∧ ( ( 𝑌 < 𝑁 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) < ( 𝑀 · 𝑌 ) ) ∧ ∀ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) → ∃ 𝑧 ∈ ℝ+ ( ( 𝑌 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑀 · 𝑌 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
441	17 431 440	syl2anc	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ+ ( ( 𝑌 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑀 · 𝑌 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )