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	bitrid	⊢ ( 𝑣 = 𝑦 → ( ∃ 𝑖 ∈ ℕ ( ( 𝑣 < 𝑖 ∧ 𝑖 ≤ ( ( 𝑘 / 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 ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )