Metamath Proof Explorer

Theorem pntibndlem3

Description: Lemma for pntibnd . Package up pntibndlem2 in 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 ⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
pntibndlem3.5 ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑣 ∈ ( 𝑍 (,) +∞ ) ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) )
Assertion pntibndlem3 ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 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 pntibndlem3.5 ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑣 ∈ ( 𝑍 (,) +∞ ) ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) )
11 2re ⊢ 2 ∈ ℝ
12 1le2 ⊢ 1 ≤ 2
13 chpdifbnd ⊢ ( ( 2 ∈ ℝ ∧ 1 ≤ 2 ) → ∃ 𝑡 ∈ ℝ+ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) )
14 11 12 13 mp2an ⊢ ∃ 𝑡 ∈ ℝ+ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑡 ∈ ℝ+ )
16 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
17 16 8 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
18 eliooord ⊢ ( 𝐸 ∈ ( 0 (,) 1 ) → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
19 8 18 syl ⊢ ( 𝜑 → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
20 19 simpld ⊢ ( 𝜑 → 0 < 𝐸 )
21 17 20 elrpd ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐸 ∈ ℝ+ )
23 4nn ⊢ 4 ∈ ℕ
24 nnrp ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
25 23 24 ax-mp ⊢ 4 ∈ ℝ+
26 rpdivcl ⊢ ( ( 𝐸 ∈ ℝ+ ∧ 4 ∈ ℝ+ ) → ( 𝐸 / 4 ) ∈ ℝ+ )
27 22 25 26 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐸 / 4 ) ∈ ℝ+ )
28 15 27 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑡 / ( 𝐸 / 4 ) ) ∈ ℝ+ )
29 28 rpred ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑡 / ( 𝐸 / 4 ) ) ∈ ℝ )
30 29 rpefcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) ∈ ℝ+ )
31 9 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑍 ∈ ℝ+ )
32 30 31 rpaddcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) ∈ ℝ+ )
33 32 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) → ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) ∈ ℝ+ )
34 breq2 ⊢ ( 𝑖 = 𝑛 → ( 𝑣 < 𝑖 ↔ 𝑣 < 𝑛 ) )
35 breq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ↔ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) )
36 34 35 anbi12d ⊢ ( 𝑖 = 𝑛 → ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ↔ ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ) )
37 fveq2 ⊢ ( 𝑖 = 𝑛 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑛 ) )
38 id ⊢ ( 𝑖 = 𝑛 → 𝑖 = 𝑛 )
39 37 38 oveq12d ⊢ ( 𝑖 = 𝑛 → ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) = ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) )
40 39 fveq2d ⊢ ( 𝑖 = 𝑛 → ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) )
41 40 breq1d ⊢ ( 𝑖 = 𝑛 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) )
42 36 41 anbi12d ⊢ ( 𝑖 = 𝑛 → ( ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ↔ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) )
43 42 cbvrexvw ⊢ ( ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) )
44 breq1 ⊢ ( 𝑣 = 𝑦 → ( 𝑣 < 𝑛 ↔ 𝑦 < 𝑛 ) )
45 oveq2 ⊢ ( 𝑣 = 𝑦 → ( ( 𝑘 / 2 ) · 𝑣 ) = ( ( 𝑘 / 2 ) · 𝑦 ) )
46 45 breq2d ⊢ ( 𝑣 = 𝑦 → ( 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ↔ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) )
47 44 46 anbi12d ⊢ ( 𝑣 = 𝑦 → ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ↔ ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ) )
48 47 anbi1d ⊢ ( 𝑣 = 𝑦 → ( ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ↔ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) )
49 48 rexbidv ⊢ ( 𝑣 = 𝑦 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) )
50 43 49 syl5bb ⊢ ( 𝑣 = 𝑦 → ( ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) )
51 oveq1 ⊢ ( 𝑚 = ( 𝑘 / 2 ) → ( 𝑚 · 𝑣 ) = ( ( 𝑘 / 2 ) · 𝑣 ) )
52 51 breq2d ⊢ ( 𝑚 = ( 𝑘 / 2 ) → ( 𝑖 ≤ ( 𝑚 · 𝑣 ) ↔ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) )
53 52 anbi2d ⊢ ( 𝑚 = ( 𝑘 / 2 ) → ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( 𝑚 · 𝑣 ) ) ↔ ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ) )
54 53 anbi1d ⊢ ( 𝑚 = ( 𝑘 / 2 ) → ( ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ↔ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ) )
55 54 rexbidv ⊢ ( 𝑚 = ( 𝑘 / 2 ) → ( ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ↔ ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ) )
56 55 ralbidv ⊢ ( 𝑚 = ( 𝑘 / 2 ) → ( ∀ 𝑣 ∈ ( 𝑍 (,) +∞ ) ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ↔ ∀ 𝑣 ∈ ( 𝑍 (,) +∞ ) ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) ) )
57 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ∀ 𝑚 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑣 ∈ ( 𝑍 (,) +∞ ) ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) )
58 5 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
59 58 rpred ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
60 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · 𝐵 ) ∈ ℝ )
61 11 59 60 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 2 · 𝐵 ) ∈ ℝ )
62 2rp ⊢ 2 ∈ ℝ+
63 relogcl ⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
64 62 63 ax-mp ⊢ ( log ‘ 2 ) ∈ ℝ
65 readdcl ⊢ ( ( ( 2 · 𝐵 ) ∈ ℝ ∧ ( log ‘ 2 ) ∈ ℝ ) → ( ( 2 · 𝐵 ) + ( log ‘ 2 ) ) ∈ ℝ )
66 61 64 65 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 2 · 𝐵 ) + ( log ‘ 2 ) ) ∈ ℝ )
67 7 66 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
68 67 22 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐶 / 𝐸 ) ∈ ℝ )
69 68 reefcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ )
70 elicopnf ⊢ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ → ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ↔ ( 𝑘 ∈ ℝ ∧ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝑘 ) ) )
71 69 70 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ↔ ( 𝑘 ∈ ℝ ∧ ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝑘 ) ) )
72 71 simprbda ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → 𝑘 ∈ ℝ )
73 72 rehalfcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( 𝑘 / 2 ) ∈ ℝ )
74 22 rphalfcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐸 / 2 ) ∈ ℝ+ )
75 59 74 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐵 / ( 𝐸 / 2 ) ) ∈ ℝ )
76 75 reefcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) ∈ ℝ )
77 remulcl ⊢ ( ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) ∈ ℝ )
78 76 11 77 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) ∈ ℝ )
79 78 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) ∈ ℝ )
80 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( exp ‘ ( 𝐶 / 𝐸 ) ) ∈ ℝ )
81 75 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐵 / ( 𝐸 / 2 ) ) ∈ ℂ )
82 64 recni ⊢ ( log ‘ 2 ) ∈ ℂ
83 efadd ⊢ ( ( ( 𝐵 / ( 𝐸 / 2 ) ) ∈ ℂ ∧ ( log ‘ 2 ) ∈ ℂ ) → ( exp ‘ ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ) = ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · ( exp ‘ ( log ‘ 2 ) ) ) )
84 81 82 83 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( exp ‘ ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ) = ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · ( exp ‘ ( log ‘ 2 ) ) ) )
85 reeflog ⊢ ( 2 ∈ ℝ+ → ( exp ‘ ( log ‘ 2 ) ) = 2 )
86 62 85 ax-mp ⊢ ( exp ‘ ( log ‘ 2 ) ) = 2
87 86 oveq2i ⊢ ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · ( exp ‘ ( log ‘ 2 ) ) ) = ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 )
88 84 87 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( exp ‘ ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ) = ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) )
89 64 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( log ‘ 2 ) ∈ ℝ )
90 rerpdivcl ⊢ ( ( ( log ‘ 2 ) ∈ ℝ ∧ 𝐸 ∈ ℝ+ ) → ( ( log ‘ 2 ) / 𝐸 ) ∈ ℝ )
91 64 22 90 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( log ‘ 2 ) / 𝐸 ) ∈ ℝ )
92 82 div1i ⊢ ( ( log ‘ 2 ) / 1 ) = ( log ‘ 2 )
93 19 simprd ⊢ ( 𝜑 → 𝐸 < 1 )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐸 < 1 )
95 17 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐸 ∈ ℝ )
96 1re ⊢ 1 ∈ ℝ
97 ltle ⊢ ( ( 𝐸 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐸 < 1 → 𝐸 ≤ 1 ) )
98 95 96 97 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐸 < 1 → 𝐸 ≤ 1 ) )
99 94 98 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐸 ≤ 1 )
100 22 rpregt0d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
101 1rp ⊢ 1 ∈ ℝ+
102 rpregt0 ⊢ ( 1 ∈ ℝ+ → ( 1 ∈ ℝ ∧ 0 < 1 ) )
103 101 102 mp1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 1 ∈ ℝ ∧ 0 < 1 ) )
104 1lt2 ⊢ 1 < 2
105 rplogcl ⊢ ( ( 2 ∈ ℝ ∧ 1 < 2 ) → ( log ‘ 2 ) ∈ ℝ+ )
106 11 104 105 mp2an ⊢ ( log ‘ 2 ) ∈ ℝ+
107 rpregt0 ⊢ ( ( log ‘ 2 ) ∈ ℝ+ → ( ( log ‘ 2 ) ∈ ℝ ∧ 0 < ( log ‘ 2 ) ) )
108 106 107 mp1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( log ‘ 2 ) ∈ ℝ ∧ 0 < ( log ‘ 2 ) ) )
109 lediv2 ⊢ ( ( ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ∧ ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( log ‘ 2 ) ∈ ℝ ∧ 0 < ( log ‘ 2 ) ) ) → ( 𝐸 ≤ 1 ↔ ( ( log ‘ 2 ) / 1 ) ≤ ( ( log ‘ 2 ) / 𝐸 ) ) )
110 100 103 108 109 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐸 ≤ 1 ↔ ( ( log ‘ 2 ) / 1 ) ≤ ( ( log ‘ 2 ) / 𝐸 ) ) )
111 99 110 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( log ‘ 2 ) / 1 ) ≤ ( ( log ‘ 2 ) / 𝐸 ) )
112 92 111 eqbrtrrid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( log ‘ 2 ) ≤ ( ( log ‘ 2 ) / 𝐸 ) )
113 89 91 75 112 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ≤ ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( ( log ‘ 2 ) / 𝐸 ) ) )
114 7 oveq1i ⊢ ( 𝐶 / 𝐸 ) = ( ( ( 2 · 𝐵 ) + ( log ‘ 2 ) ) / 𝐸 )
115 61 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 2 · 𝐵 ) ∈ ℂ )
116 82 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( log ‘ 2 ) ∈ ℂ )
117 rpcnne0 ⊢ ( 𝐸 ∈ ℝ+ → ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) )
118 22 117 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) )
119 divdir ⊢ ( ( ( 2 · 𝐵 ) ∈ ℂ ∧ ( log ‘ 2 ) ∈ ℂ ∧ ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) ) → ( ( ( 2 · 𝐵 ) + ( log ‘ 2 ) ) / 𝐸 ) = ( ( ( 2 · 𝐵 ) / 𝐸 ) + ( ( log ‘ 2 ) / 𝐸 ) ) )
120 115 116 118 119 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( ( 2 · 𝐵 ) + ( log ‘ 2 ) ) / 𝐸 ) = ( ( ( 2 · 𝐵 ) / 𝐸 ) + ( ( log ‘ 2 ) / 𝐸 ) ) )
121 114 120 eqtrid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐶 / 𝐸 ) = ( ( ( 2 · 𝐵 ) / 𝐸 ) + ( ( log ‘ 2 ) / 𝐸 ) ) )
122 11 recni ⊢ 2 ∈ ℂ
123 59 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
124 mulcom ⊢ ( ( 2 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐵 ) = ( 𝐵 · 2 ) )
125 122 123 124 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 2 · 𝐵 ) = ( 𝐵 · 2 ) )
126 125 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 2 · 𝐵 ) / 𝐸 ) = ( ( 𝐵 · 2 ) / 𝐸 ) )
127 rpcnne0 ⊢ ( 2 ∈ ℝ+ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
128 62 127 mp1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
129 divdiv2 ⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( 𝐵 / ( 𝐸 / 2 ) ) = ( ( 𝐵 · 2 ) / 𝐸 ) )
130 123 118 128 129 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐵 / ( 𝐸 / 2 ) ) = ( ( 𝐵 · 2 ) / 𝐸 ) )
131 126 130 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 2 · 𝐵 ) / 𝐸 ) = ( 𝐵 / ( 𝐸 / 2 ) ) )
132 131 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( ( 2 · 𝐵 ) / 𝐸 ) + ( ( log ‘ 2 ) / 𝐸 ) ) = ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( ( log ‘ 2 ) / 𝐸 ) ) )
133 121 132 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝐶 / 𝐸 ) = ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( ( log ‘ 2 ) / 𝐸 ) ) )
134 113 133 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ≤ ( 𝐶 / 𝐸 ) )
135 readdcl ⊢ ( ( ( 𝐵 / ( 𝐸 / 2 ) ) ∈ ℝ ∧ ( log ‘ 2 ) ∈ ℝ ) → ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ∈ ℝ )
136 75 64 135 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ∈ ℝ )
137 efle ⊢ ( ( ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ∈ ℝ ∧ ( 𝐶 / 𝐸 ) ∈ ℝ ) → ( ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ≤ ( 𝐶 / 𝐸 ) ↔ ( exp ‘ ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ) ≤ ( exp ‘ ( 𝐶 / 𝐸 ) ) ) )
138 136 68 137 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ≤ ( 𝐶 / 𝐸 ) ↔ ( exp ‘ ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ) ≤ ( exp ‘ ( 𝐶 / 𝐸 ) ) ) )
139 134 138 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( exp ‘ ( ( 𝐵 / ( 𝐸 / 2 ) ) + ( log ‘ 2 ) ) ) ≤ ( exp ‘ ( 𝐶 / 𝐸 ) ) )
140 88 139 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) ≤ ( exp ‘ ( 𝐶 / 𝐸 ) ) )
141 140 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) ≤ ( exp ‘ ( 𝐶 / 𝐸 ) ) )
142 71 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( exp ‘ ( 𝐶 / 𝐸 ) ) ≤ 𝑘 )
143 79 80 72 141 142 letrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) ≤ 𝑘 )
144 76 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) ∈ ℝ )
145 rpregt0 ⊢ ( 2 ∈ ℝ+ → ( 2 ∈ ℝ ∧ 0 < 2 ) )
146 62 145 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
147 lemuldiv ⊢ ( ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) ≤ 𝑘 ↔ ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) ≤ ( 𝑘 / 2 ) ) )
148 144 72 146 147 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( ( ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) · 2 ) ≤ 𝑘 ↔ ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) ≤ ( 𝑘 / 2 ) ) )
149 143 148 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( exp ‘ ( 𝐵 / ( 𝐸 / 2 ) ) ) ≤ ( 𝑘 / 2 ) )
150 6 149 eqbrtrid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → 𝐾 ≤ ( 𝑘 / 2 ) )
151 6 144 eqeltrid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → 𝐾 ∈ ℝ )
152 elicopnf ⊢ ( 𝐾 ∈ ℝ → ( ( 𝑘 / 2 ) ∈ ( 𝐾 [,) +∞ ) ↔ ( ( 𝑘 / 2 ) ∈ ℝ ∧ 𝐾 ≤ ( 𝑘 / 2 ) ) ) )
153 151 152 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( ( 𝑘 / 2 ) ∈ ( 𝐾 [,) +∞ ) ↔ ( ( 𝑘 / 2 ) ∈ ℝ ∧ 𝐾 ≤ ( 𝑘 / 2 ) ) ) )
154 73 150 153 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ) → ( 𝑘 / 2 ) ∈ ( 𝐾 [,) +∞ ) )
155 154 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ( 𝑘 / 2 ) ∈ ( 𝐾 [,) +∞ ) )
156 155 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ( 𝑘 / 2 ) ∈ ( 𝐾 [,) +∞ ) )
157 56 57 156 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ∀ 𝑣 ∈ ( 𝑍 (,) +∞ ) ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 2 ) · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) / 𝑖 ) ) ≤ ( 𝐸 / 2 ) ) )
158 elioore ⊢ ( 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) → 𝑦 ∈ ℝ )
159 158 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → 𝑦 ∈ ℝ )
160 31 rpred ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑍 ∈ ℝ )
161 160 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → 𝑍 ∈ ℝ )
162 29 reefcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) ∈ ℝ )
163 162 160 readdcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) ∈ ℝ )
164 163 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) ∈ ℝ )
165 160 30 ltaddrp2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑍 < ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) )
166 165 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → 𝑍 < ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) )
167 eliooord ⊢ ( 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) → ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) < 𝑦 ∧ 𝑦 < +∞ ) )
168 167 simpld ⊢ ( 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) → ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) < 𝑦 )
169 168 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) < 𝑦 )
170 161 164 159 166 169 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → 𝑍 < 𝑦 )
171 161 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → 𝑍 ∈ ℝ* )
172 elioopnf ⊢ ( 𝑍 ∈ ℝ* → ( 𝑦 ∈ ( 𝑍 (,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑍 < 𝑦 ) ) )
173 171 172 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ( 𝑦 ∈ ( 𝑍 (,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑍 < 𝑦 ) ) )
174 159 170 173 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → 𝑦 ∈ ( 𝑍 (,) +∞ ) )
175 174 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → 𝑦 ∈ ( 𝑍 (,) +∞ ) )
176 50 157 175 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) )
177 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → 𝐴 ∈ ℝ+ )
178 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑣 ) )
179 id ⊢ ( 𝑥 = 𝑣 → 𝑥 = 𝑣 )
180 178 179 oveq12d ⊢ ( 𝑥 = 𝑣 → ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) = ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) )
181 180 fveq2d ⊢ ( 𝑥 = 𝑣 → ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) )
182 181 breq1d ⊢ ( 𝑥 = 𝑣 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ 𝐴 ) )
183 182 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 ↔ ∀ 𝑣 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ 𝐴 )
184 4 183 sylib ⊢ ( 𝜑 → ∀ 𝑣 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ 𝐴 )
185 184 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → ∀ 𝑣 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ 𝐴 )
186 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → 𝐵 ∈ ℝ+ )
187 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → 𝐸 ∈ ( 0 (,) 1 ) )
188 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → 𝑍 ∈ ℝ+ )
189 simprrl ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → 𝑛 ∈ ℕ )
190 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → 𝑡 ∈ ℝ+ )
191 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) )
192 eqid ⊢ ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) = ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 )
193 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) )
194 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) )
195 simprrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) )
196 1 177 3 185 186 6 7 187 188 189 190 191 192 193 194 195 pntibndlem2 ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) ) → ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
197 196 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 𝑦 < 𝑛 ∧ 𝑛 ≤ ( ( 𝑘 / 2 ) · 𝑦 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝐸 / 2 ) ) ) ) → ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
198 176 197 rexlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) ∧ ( 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∧ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ) ) → ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
199 198 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) → ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
200 oveq1 ⊢ ( 𝑥 = ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) → ( 𝑥 (,) +∞ ) = ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) )
201 200 raleqdv ⊢ ( 𝑥 = ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) → ( ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∀ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
202 201 ralbidv ⊢ ( 𝑥 = ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) → ( ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
203 202 rspcev ⊢ ( ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) ∈ ℝ+ ∧ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( ( ( exp ‘ ( 𝑡 / ( 𝐸 / 4 ) ) ) + 𝑍 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
204 33 199 203 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
205 204 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑣 ∈ ( 1 (,) +∞ ) ∀ 𝑤 ∈ ( 𝑣 [,] ( 2 · 𝑣 ) ) ( ( ψ ‘ 𝑤 ) − ( ψ ‘ 𝑣 ) ) ≤ ( ( 2 · ( 𝑤 − 𝑣 ) ) + ( 𝑡 · ( 𝑣 / ( log ‘ 𝑣 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
206 14 205 mpi ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐶 / 𝐸 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )