Theorem pntlemp

Description: Lemma for pnt . Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016)

	Ref	Expression
Hypotheses	pntlem3.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntlem3.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	pntlem3.A	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
	pntlemp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	pntlemp.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
	pntlemp.d	⊢ 𝐷 = ( 𝐴 + 1 )
	pntlemp.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
	pntlemp.K	⊢ ( 𝜑 → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
	pntlemp.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
	pntlemp.u2	⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
	pntlemp.e	⊢ 𝐸 = ( 𝑈 / 𝐷 )
	pntlemp.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
	pntlemp.y	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
	pntlemp.U	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
Assertion	pntlemp	⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pntlem3.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntlem3.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3		pntlem3.A	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
4		pntlemp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
5		pntlemp.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
6		pntlemp.d	⊢ 𝐷 = ( 𝐴 + 1 )
7		pntlemp.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
8		pntlemp.K	⊢ ( 𝜑 → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
9		pntlemp.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
10		pntlemp.u2	⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
11		pntlemp.e	⊢ 𝐸 = ( 𝑈 / 𝐷 )
12		pntlemp.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
13		pntlemp.y	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
14		pntlemp.U	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
15		oveq2	⊢ ( 𝑒 = 𝐸 → ( 𝐵 / 𝑒 ) = ( 𝐵 / 𝐸 ) )
16	15	fveq2d	⊢ ( 𝑒 = 𝐸 → ( exp ‘ ( 𝐵 / 𝑒 ) ) = ( exp ‘ ( 𝐵 / 𝐸 ) ) )
17	16 12	eqtr4di	⊢ ( 𝑒 = 𝐸 → ( exp ‘ ( 𝐵 / 𝑒 ) ) = 𝐾 )
18	17	oveq1d	⊢ ( 𝑒 = 𝐸 → ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) = ( 𝐾 [,) +∞ ) )
19		oveq2	⊢ ( 𝑒 = 𝐸 → ( 𝐿 · 𝑒 ) = ( 𝐿 · 𝐸 ) )
20	19	oveq2d	⊢ ( 𝑒 = 𝐸 → ( 1 + ( 𝐿 · 𝑒 ) ) = ( 1 + ( 𝐿 · 𝐸 ) ) )
21	20	oveq1d	⊢ ( 𝑒 = 𝐸 → ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) = ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) )
22	21	breq1d	⊢ ( 𝑒 = 𝐸 → ( ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ↔ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) )
23	22	anbi2d	⊢ ( 𝑒 = 𝐸 → ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ↔ ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ) )
24	21	oveq2d	⊢ ( 𝑒 = 𝐸 → ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) = ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) )
25		breq2	⊢ ( 𝑒 = 𝐸 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
26	24 25	raleqbidv	⊢ ( 𝑒 = 𝐸 → ( ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ↔ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
27	23 26	anbi12d	⊢ ( 𝑒 = 𝐸 → ( ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
28	27	rexbidv	⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
29	28	ralbidv	⊢ ( 𝑒 = 𝐸 → ( ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
30	18 29	raleqbidv	⊢ ( 𝑒 = 𝐸 → ( ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
31	30	rexbidv	⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
32		oveq1	⊢ ( 𝑥 = 𝑡 → ( 𝑥 (,) +∞ ) = ( 𝑡 (,) +∞ ) )
33	32	raleqdv	⊢ ( 𝑥 = 𝑡 → ( ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
34	33	ralbidv	⊢ ( 𝑥 = 𝑡 → ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
35	34	cbvrexvw	⊢ ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
36	31 35	bitrdi	⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
37	1 2 4 5 6 7 9 10 11 12	pntlemc	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
38	37	simp3d	⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
39	38	simp1d	⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
40	36 8 39	rspcdva	⊢ ( 𝜑 → ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
41	13	simpld	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
42	41	rpred	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
43	13	simprd	⊢ ( 𝜑 → 1 ≤ 𝑌 )
44	1	pntrlog2bnd	⊢ ( ( 𝑌 ∈ ℝ ∧ 1 ≤ 𝑌 ) → ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 )
45	42 43 44	syl2anc	⊢ ( 𝜑 → ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 )
46		reeanv	⊢ ( ∃ 𝑡 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ↔ ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) )
47	2	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝐴 ∈ ℝ+ )
48	4	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝐵 ∈ ℝ+ )
49	5	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝐿 ∈ ( 0 (,) 1 ) )
50	9	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝑈 ∈ ℝ+ )
51	10	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝑈 ≤ 𝐴 )
52	13	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
53		simpl	⊢ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) → 𝑡 ∈ ℝ+ )
54		rpaddcl	⊢ ( ( 𝑌 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) → ( 𝑌 + 𝑡 ) ∈ ℝ+ )
55	41 53 54	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( 𝑌 + 𝑡 ) ∈ ℝ+ )
56		ltaddrp	⊢ ( ( 𝑌 ∈ ℝ ∧ 𝑡 ∈ ℝ+ ) → 𝑌 < ( 𝑌 + 𝑡 ) )
57	42 53 56	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑌 < ( 𝑌 + 𝑡 ) )
58	55 57	jca	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( ( 𝑌 + 𝑡 ) ∈ ℝ+ ∧ 𝑌 < ( 𝑌 + 𝑡 ) ) )
59	58	adantrr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ( ( 𝑌 + 𝑡 ) ∈ ℝ+ ∧ 𝑌 < ( 𝑌 + 𝑡 ) ) )
60		simprlr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝑐 ∈ ℝ+ )
61		eqid	⊢ ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( ( 𝑌 + 𝑡 ) · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝑐 ) ) ) ) ) = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( ( 𝑌 + 𝑡 ) · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝑐 ) ) ) ) )
62	14	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
63		rpxr	⊢ ( 𝑡 ∈ ℝ+ → 𝑡 ∈ ℝ* )
64	63	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑡 ∈ ℝ* )
65		rpre	⊢ ( 𝑡 ∈ ℝ+ → 𝑡 ∈ ℝ )
66	65	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑡 ∈ ℝ )
67	55	rpred	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( 𝑌 + 𝑡 ) ∈ ℝ )
68	41	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑌 ∈ ℝ+ )
69	66 68	ltaddrp2d	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑡 < ( 𝑌 + 𝑡 ) )
70	66 67 69	ltled	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑡 ≤ ( 𝑌 + 𝑡 ) )
71		iooss1	⊢ ( ( 𝑡 ∈ ℝ* ∧ 𝑡 ≤ ( 𝑌 + 𝑡 ) ) → ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) )
72	64 70 71	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) )
73	72	adantrr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) )
74		simprrl	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
75		ssralv	⊢ ( ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) → ( ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) → ∀ 𝑦 ∈ ( ( 𝑌 + 𝑡 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
76	75	ralimdv	⊢ ( ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) → ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) → ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( ( 𝑌 + 𝑡 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
77	73 74 76	sylc	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( ( 𝑌 + 𝑡 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
78		simprrr	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 )
79	1 47 48 49 6 7 50 51 11 12 52 59 60 61 62 77 78	pntleme	⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )
80	79	expr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) )
81	80	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) )
82	46 81	biimtrrid	⊢ ( 𝜑 → ( ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) )
83	40 45 82	mp2and	⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )