Metamath Proof Explorer

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 sseldi ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
24 21 8 sseldi ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
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 sseldi ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
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 ffvelrni ⊢ ( 𝑢 ∈ ℝ+ → ( 𝑅 ‘ 𝑢 ) ∈ ℝ )
87 84 86 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( 𝑅 ‘ 𝑢 ) ∈ ℝ )
88 87 84 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ∈ ℝ )
89 88 recnd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ∈ ℂ )
90 89 abscld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑁 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ∈ ℝ )
91 85 ffvelrni ⊢ ( 𝑁 ∈ ℝ+ → ( 𝑅 ‘ 𝑁 ) ∈ ℝ )
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 mulid2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 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 mulid1d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 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 syl6eq ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 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 syl6eqr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 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 syl6eq ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 [,] ( ( 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 ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )