Theorem pntlemo

Description: Lemma for pnt . Combine all the estimates to establish a smaller eventual bound on R ( Z ) / Z . (Contributed by Mario Carneiro, 14-Apr-2016)

	Ref	Expression
Hypotheses	pntlem1.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntlem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	pntlem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	pntlem1.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
	pntlem1.d	⊢ 𝐷 = ( 𝐴 + 1 )
	pntlem1.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
	pntlem1.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
	pntlem1.u2	⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
	pntlem1.e	⊢ 𝐸 = ( 𝑈 / 𝐷 )
	pntlem1.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
	pntlem1.y	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
	pntlem1.x	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
	pntlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
	pntlem1.w	⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
	pntlem1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
	pntlem1.m	⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
	pntlem1.n	⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
	pntlem1.U	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
	pntlem1.K	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
	pntlem1.C	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) ) / 𝑧 ) ≤ 𝐶 )
Assertion	pntlemo	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntlem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3		pntlem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4		pntlem1.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
5		pntlem1.d	⊢ 𝐷 = ( 𝐴 + 1 )
6		pntlem1.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
7		pntlem1.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
8		pntlem1.u2	⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
9		pntlem1.e	⊢ 𝐸 = ( 𝑈 / 𝐷 )
10		pntlem1.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
11		pntlem1.y	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
12		pntlem1.x	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
13		pntlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
14		pntlem1.w	⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
15		pntlem1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
16		pntlem1.m	⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
17		pntlem1.n	⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
18		pntlem1.U	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
19		pntlem1.K	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
20		pntlem1.C	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) ) / 𝑧 ) ≤ 𝐶 )
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pntlemb	⊢ ( 𝜑 → ( 𝑍 ∈ ℝ+ ∧ ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) ∧ ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
22	21	simp1d	⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
23	1	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
24	23	ffvelcdmi	⊢ ( 𝑍 ∈ ℝ+ → ( 𝑅 ‘ 𝑍 ) ∈ ℝ )
25	22 24	syl	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑍 ) ∈ ℝ )
26	25 22	rerpdivcld	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ∈ ℝ )
27	26	recnd	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ∈ ℂ )
28	27	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) ∈ ℝ )
29	22	relogcld	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ )
30	28 29	remulcld	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
31	7	rpred	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
32		3re	⊢ 3 ∈ ℝ
33	32	a1i	⊢ ( 𝜑 → 3 ∈ ℝ )
34	29 33	readdcld	⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) + 3 ) ∈ ℝ )
35	31 34	remulcld	⊢ ( 𝜑 → ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) ∈ ℝ )
36		2re	⊢ 2 ∈ ℝ
37	36	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
38	1 2 3 4 5 6 7 8 9 10	pntlemc	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
39	38	simp3d	⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
40	39	simp3d	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ+ )
41	40	rpred	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ )
42	1 2 3 4 5 6	pntlemd	⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
43	42	simp1d	⊢ ( 𝜑 → 𝐿 ∈ ℝ+ )
44	38	simp1d	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
45		2z	⊢ 2 ∈ ℤ
46		rpexpcl	⊢ ( ( 𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
47	44 45 46	sylancl	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
48	43 47	rpmulcld	⊢ ( 𝜑 → ( 𝐿 · ( 𝐸 ↑ 2 ) ) ∈ ℝ+ )
49		3nn0	⊢ 3 ∈ ℕ0
50		2nn	⊢ 2 ∈ ℕ
51	49 50	decnncl	⊢ ; 3 2 ∈ ℕ
52		nnrp	⊢ ( ; 3 2 ∈ ℕ → ; 3 2 ∈ ℝ+ )
53	51 52	ax-mp	⊢ ; 3 2 ∈ ℝ+
54		rpmulcl	⊢ ( ( ; 3 2 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ; 3 2 · 𝐵 ) ∈ ℝ+ )
55	53 3 54	sylancr	⊢ ( 𝜑 → ( ; 3 2 · 𝐵 ) ∈ ℝ+ )
56	48 55	rpdivcld	⊢ ( 𝜑 → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ∈ ℝ+ )
57	56	rpred	⊢ ( 𝜑 → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ∈ ℝ )
58	41 57	remulcld	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) ∈ ℝ )
59	58 29	remulcld	⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
60	37 59	remulcld	⊢ ( 𝜑 → ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ )
61	35 60	resubcld	⊢ ( 𝜑 → ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) ∈ ℝ )
62	13	rpred	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
63	61 62	readdcld	⊢ ( 𝜑 → ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) + 𝐶 ) ∈ ℝ )
64	7	rpcnd	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
65	58	recnd	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) ∈ ℂ )
66	29	recnd	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℂ )
67	64 65 66	subdird	⊢ ( 𝜑 → ( ( 𝑈 − ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) ) · ( log ‘ 𝑍 ) ) = ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
68	43	rpcnd	⊢ ( 𝜑 → 𝐿 ∈ ℂ )
69	47	rpcnd	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
70	55	rpcnne0d	⊢ ( 𝜑 → ( ( ; 3 2 · 𝐵 ) ∈ ℂ ∧ ( ; 3 2 · 𝐵 ) ≠ 0 ) )
71		div23	⊢ ( ( 𝐿 ∈ ℂ ∧ ( 𝐸 ↑ 2 ) ∈ ℂ ∧ ( ( ; 3 2 · 𝐵 ) ∈ ℂ ∧ ( ; 3 2 · 𝐵 ) ≠ 0 ) ) → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) = ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( 𝐸 ↑ 2 ) ) )
72	68 69 70 71	syl3anc	⊢ ( 𝜑 → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) = ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( 𝐸 ↑ 2 ) ) )
73	9	oveq1i	⊢ ( 𝐸 ↑ 2 ) = ( ( 𝑈 / 𝐷 ) ↑ 2 )
74	42	simp2d	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
75	74	rpcnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
76	74	rpne0d	⊢ ( 𝜑 → 𝐷 ≠ 0 )
77	64 75 76	sqdivd	⊢ ( 𝜑 → ( ( 𝑈 / 𝐷 ) ↑ 2 ) = ( ( 𝑈 ↑ 2 ) / ( 𝐷 ↑ 2 ) ) )
78	73 77	eqtrid	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) = ( ( 𝑈 ↑ 2 ) / ( 𝐷 ↑ 2 ) ) )
79	78	oveq2d	⊢ ( 𝜑 → ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( 𝐸 ↑ 2 ) ) = ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( ( 𝑈 ↑ 2 ) / ( 𝐷 ↑ 2 ) ) ) )
80	43 55	rpdivcld	⊢ ( 𝜑 → ( 𝐿 / ( ; 3 2 · 𝐵 ) ) ∈ ℝ+ )
81	80	rpcnd	⊢ ( 𝜑 → ( 𝐿 / ( ; 3 2 · 𝐵 ) ) ∈ ℂ )
82	64	sqcld	⊢ ( 𝜑 → ( 𝑈 ↑ 2 ) ∈ ℂ )
83		rpexpcl	⊢ ( ( 𝐷 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝐷 ↑ 2 ) ∈ ℝ+ )
84	74 45 83	sylancl	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℝ+ )
85	84	rpcnne0d	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) ∈ ℂ ∧ ( 𝐷 ↑ 2 ) ≠ 0 ) )
86		divass	⊢ ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) ∈ ℂ ∧ ( 𝑈 ↑ 2 ) ∈ ℂ ∧ ( ( 𝐷 ↑ 2 ) ∈ ℂ ∧ ( 𝐷 ↑ 2 ) ≠ 0 ) ) → ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( 𝑈 ↑ 2 ) ) / ( 𝐷 ↑ 2 ) ) = ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( ( 𝑈 ↑ 2 ) / ( 𝐷 ↑ 2 ) ) ) )
87		div23	⊢ ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) ∈ ℂ ∧ ( 𝑈 ↑ 2 ) ∈ ℂ ∧ ( ( 𝐷 ↑ 2 ) ∈ ℂ ∧ ( 𝐷 ↑ 2 ) ≠ 0 ) ) → ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( 𝑈 ↑ 2 ) ) / ( 𝐷 ↑ 2 ) ) = ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) · ( 𝑈 ↑ 2 ) ) )
88	86 87	eqtr3d	⊢ ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) ∈ ℂ ∧ ( 𝑈 ↑ 2 ) ∈ ℂ ∧ ( ( 𝐷 ↑ 2 ) ∈ ℂ ∧ ( 𝐷 ↑ 2 ) ≠ 0 ) ) → ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( ( 𝑈 ↑ 2 ) / ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) · ( 𝑈 ↑ 2 ) ) )
89	81 82 85 88	syl3anc	⊢ ( 𝜑 → ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) · ( ( 𝑈 ↑ 2 ) / ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) · ( 𝑈 ↑ 2 ) ) )
90	72 79 89	3eqtrd	⊢ ( 𝜑 → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) = ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) · ( 𝑈 ↑ 2 ) ) )
91	90	oveq2d	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) = ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) · ( 𝑈 ↑ 2 ) ) ) )
92		df-3	⊢ 3 = ( 2 + 1 )
93	92	oveq2i	⊢ ( 𝑈 ↑ 3 ) = ( 𝑈 ↑ ( 2 + 1 ) )
94		2nn0	⊢ 2 ∈ ℕ0
95		expp1	⊢ ( ( 𝑈 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝑈 ↑ ( 2 + 1 ) ) = ( ( 𝑈 ↑ 2 ) · 𝑈 ) )
96	64 94 95	sylancl	⊢ ( 𝜑 → ( 𝑈 ↑ ( 2 + 1 ) ) = ( ( 𝑈 ↑ 2 ) · 𝑈 ) )
97	93 96	eqtrid	⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) = ( ( 𝑈 ↑ 2 ) · 𝑈 ) )
98	82 64	mulcomd	⊢ ( 𝜑 → ( ( 𝑈 ↑ 2 ) · 𝑈 ) = ( 𝑈 · ( 𝑈 ↑ 2 ) ) )
99	97 98	eqtrd	⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) = ( 𝑈 · ( 𝑈 ↑ 2 ) ) )
100	99	oveq2d	⊢ ( 𝜑 → ( 𝐹 · ( 𝑈 ↑ 3 ) ) = ( 𝐹 · ( 𝑈 · ( 𝑈 ↑ 2 ) ) ) )
101	42	simp3d	⊢ ( 𝜑 → 𝐹 ∈ ℝ+ )
102	101	rpcnd	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
103	102 64 82	mulassd	⊢ ( 𝜑 → ( ( 𝐹 · 𝑈 ) · ( 𝑈 ↑ 2 ) ) = ( 𝐹 · ( 𝑈 · ( 𝑈 ↑ 2 ) ) ) )
104		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
105	74	rpreccld	⊢ ( 𝜑 → ( 1 / 𝐷 ) ∈ ℝ+ )
106	105	rpcnd	⊢ ( 𝜑 → ( 1 / 𝐷 ) ∈ ℂ )
107	104 106 64	subdird	⊢ ( 𝜑 → ( ( 1 − ( 1 / 𝐷 ) ) · 𝑈 ) = ( ( 1 · 𝑈 ) − ( ( 1 / 𝐷 ) · 𝑈 ) ) )
108	64	mullidd	⊢ ( 𝜑 → ( 1 · 𝑈 ) = 𝑈 )
109	64 75 76	divrec2d	⊢ ( 𝜑 → ( 𝑈 / 𝐷 ) = ( ( 1 / 𝐷 ) · 𝑈 ) )
110	9 109	eqtr2id	⊢ ( 𝜑 → ( ( 1 / 𝐷 ) · 𝑈 ) = 𝐸 )
111	108 110	oveq12d	⊢ ( 𝜑 → ( ( 1 · 𝑈 ) − ( ( 1 / 𝐷 ) · 𝑈 ) ) = ( 𝑈 − 𝐸 ) )
112	107 111	eqtr2d	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) = ( ( 1 − ( 1 / 𝐷 ) ) · 𝑈 ) )
113	112	oveq1d	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) = ( ( ( 1 − ( 1 / 𝐷 ) ) · 𝑈 ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) )
114	6	oveq1i	⊢ ( 𝐹 · 𝑈 ) = ( ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) · 𝑈 )
115	104 106	subcld	⊢ ( 𝜑 → ( 1 − ( 1 / 𝐷 ) ) ∈ ℂ )
116	80 84	rpdivcld	⊢ ( 𝜑 → ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ∈ ℝ+ )
117	116	rpcnd	⊢ ( 𝜑 → ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ∈ ℂ )
118	115 117 64	mul32d	⊢ ( 𝜑 → ( ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) · 𝑈 ) = ( ( ( 1 − ( 1 / 𝐷 ) ) · 𝑈 ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) )
119	114 118	eqtrid	⊢ ( 𝜑 → ( 𝐹 · 𝑈 ) = ( ( ( 1 − ( 1 / 𝐷 ) ) · 𝑈 ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) )
120	113 119	eqtr4d	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) = ( 𝐹 · 𝑈 ) )
121	120	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) · ( 𝑈 ↑ 2 ) ) = ( ( 𝐹 · 𝑈 ) · ( 𝑈 ↑ 2 ) ) )
122	40	rpcnd	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℂ )
123	122 117 82	mulassd	⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) · ( 𝑈 ↑ 2 ) ) = ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) · ( 𝑈 ↑ 2 ) ) ) )
124	121 123	eqtr3d	⊢ ( 𝜑 → ( ( 𝐹 · 𝑈 ) · ( 𝑈 ↑ 2 ) ) = ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) · ( 𝑈 ↑ 2 ) ) ) )
125	100 103 124	3eqtr2d	⊢ ( 𝜑 → ( 𝐹 · ( 𝑈 ↑ 3 ) ) = ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) · ( 𝑈 ↑ 2 ) ) ) )
126	91 125	eqtr4d	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) = ( 𝐹 · ( 𝑈 ↑ 3 ) ) )
127	126	oveq2d	⊢ ( 𝜑 → ( 𝑈 − ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) ) = ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )
128	127	oveq1d	⊢ ( 𝜑 → ( ( 𝑈 − ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) ) · ( log ‘ 𝑍 ) ) = ( ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) · ( log ‘ 𝑍 ) ) )
129	67 128	eqtr3d	⊢ ( 𝜑 → ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) = ( ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) · ( log ‘ 𝑍 ) ) )
130	31 29	remulcld	⊢ ( 𝜑 → ( 𝑈 · ( log ‘ 𝑍 ) ) ∈ ℝ )
131	130 59	resubcld	⊢ ( 𝜑 → ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ )
132	129 131	eqeltrrd	⊢ ( 𝜑 → ( ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
133	22	rpred	⊢ ( 𝜑 → 𝑍 ∈ ℝ )
134	21	simp2d	⊢ ( 𝜑 → ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) )
135	134	simp1d	⊢ ( 𝜑 → 1 < 𝑍 )
136	133 135	rplogcld	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ+ )
137	37 136	rerpdivcld	⊢ ( 𝜑 → ( 2 / ( log ‘ 𝑍 ) ) ∈ ℝ )
138		fzfid	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ∈ Fin )
139	22	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑍 ∈ ℝ+ )
140		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) → 𝑛 ∈ ℕ )
141	140	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ℕ )
142	141	nnrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ℝ+ )
143	139 142	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑍 / 𝑛 ) ∈ ℝ+ )
144	23	ffvelcdmi	⊢ ( ( 𝑍 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
145	143 144	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
146	145 139	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ∈ ℝ )
147	146	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ∈ ℂ )
148	147	abscld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ∈ ℝ )
149	142	relogcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
150	148 149	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
151	138 150	fsumrecl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
152	137 151	remulcld	⊢ ( 𝜑 → ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
153	152 62	readdcld	⊢ ( 𝜑 → ( ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) + 𝐶 ) ∈ ℝ )
154	25	recnd	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑍 ) ∈ ℂ )
155	154	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) ∈ ℝ )
156	155	recnd	⊢ ( 𝜑 → ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) ∈ ℂ )
157	156 66	mulcld	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) ∈ ℂ )
158	137	recnd	⊢ ( 𝜑 → ( 2 / ( log ‘ 𝑍 ) ) ∈ ℂ )
159	145	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℂ )
160	159	abscld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) ∈ ℝ )
161	160 149	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
162	138 161	fsumrecl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
163	162	recnd	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
164	158 163	mulcld	⊢ ( 𝜑 → ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
165	22	rpcnd	⊢ ( 𝜑 → 𝑍 ∈ ℂ )
166	22	rpne0d	⊢ ( 𝜑 → 𝑍 ≠ 0 )
167	157 164 165 166	divsubdird	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑍 ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) / 𝑍 ) − ( ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑍 ) ) )
168	156 66 165 166	div23d	⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) / 𝑍 ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) / 𝑍 ) · ( log ‘ 𝑍 ) ) )
169	154 165 166	absdivd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) / ( abs ‘ 𝑍 ) ) )
170	22	rprege0d	⊢ ( 𝜑 → ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) )
171		absid	⊢ ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( abs ‘ 𝑍 ) = 𝑍 )
172	170 171	syl	⊢ ( 𝜑 → ( abs ‘ 𝑍 ) = 𝑍 )
173	172	oveq2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) / ( abs ‘ 𝑍 ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) / 𝑍 ) )
174	169 173	eqtrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) / 𝑍 ) )
175	174	oveq1d	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) / 𝑍 ) · ( log ‘ 𝑍 ) ) )
176	168 175	eqtr4d	⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) / 𝑍 ) = ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) )
177	158 163 165 166	divassd	⊢ ( 𝜑 → ( ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑍 ) = ( ( 2 / ( log ‘ 𝑍 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) ) )
178	165	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑍 ∈ ℂ )
179	166	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑍 ≠ 0 )
180	159 178 179	absdivd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) / ( abs ‘ 𝑍 ) ) )
181	172	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ 𝑍 ) = 𝑍 )
182	181	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) / ( abs ‘ 𝑍 ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) / 𝑍 ) )
183	180 182	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) / 𝑍 ) )
184	183	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) / 𝑍 ) · ( log ‘ 𝑛 ) ) )
185	160	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) ∈ ℂ )
186	149	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
187	22	rpcnne0d	⊢ ( 𝜑 → ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) )
188	187	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) )
189		div23	⊢ ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) ∈ ℂ ∧ ( log ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) / 𝑍 ) · ( log ‘ 𝑛 ) ) )
190	185 186 188 189	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) / 𝑍 ) · ( log ‘ 𝑛 ) ) )
191	184 190	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) = ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) )
192	191	sumeq2dv	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) )
193	161	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
194	138 165 193 166	fsumdivc	⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) )
195	192 194	eqtr4d	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) )
196	195	oveq2d	⊢ ( 𝜑 → ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) = ( ( 2 / ( log ‘ 𝑍 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / 𝑍 ) ) )
197	177 196	eqtr4d	⊢ ( 𝜑 → ( ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑍 ) = ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) )
198	176 197	oveq12d	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) / 𝑍 ) − ( ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑍 ) ) = ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) )
199	167 198	eqtrd	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑍 ) = ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) )
200		2fveq3	⊢ ( 𝑧 = 𝑍 → ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) = ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) )
201		fveq2	⊢ ( 𝑧 = 𝑍 → ( log ‘ 𝑧 ) = ( log ‘ 𝑍 ) )
202	200 201	oveq12d	⊢ ( 𝑧 = 𝑍 → ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) )
203	201	oveq2d	⊢ ( 𝑧 = 𝑍 → ( 2 / ( log ‘ 𝑧 ) ) = ( 2 / ( log ‘ 𝑍 ) ) )
204		oveq2	⊢ ( 𝑖 = 𝑛 → ( 𝑧 / 𝑖 ) = ( 𝑧 / 𝑛 ) )
205	204	fveq2d	⊢ ( 𝑖 = 𝑛 → ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) = ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) )
206	205	fveq2d	⊢ ( 𝑖 = 𝑛 → ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) )
207		fveq2	⊢ ( 𝑖 = 𝑛 → ( log ‘ 𝑖 ) = ( log ‘ 𝑛 ) )
208	206 207	oveq12d	⊢ ( 𝑖 = 𝑛 → ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
209	208	cbvsumv	⊢ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) )
210		fvoveq1	⊢ ( 𝑧 = 𝑍 → ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) = ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) )
211	210	oveq2d	⊢ ( 𝑧 = 𝑍 → ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) = ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
212		simpl	⊢ ( ( 𝑧 = 𝑍 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑧 = 𝑍 )
213	212	fvoveq1d	⊢ ( ( 𝑧 = 𝑍 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) = ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) )
214	213	fveq2d	⊢ ( ( 𝑧 = 𝑍 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) = ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) )
215	214	oveq1d	⊢ ( ( 𝑧 = 𝑍 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
216	211 215	sumeq12rdv	⊢ ( 𝑧 = 𝑍 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
217	209 216	eqtrid	⊢ ( 𝑧 = 𝑍 → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
218	203 217	oveq12d	⊢ ( 𝑧 = 𝑍 → ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) = ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
219	202 218	oveq12d	⊢ ( 𝑧 = 𝑍 → ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
220		id	⊢ ( 𝑧 = 𝑍 → 𝑧 = 𝑍 )
221	219 220	oveq12d	⊢ ( 𝑧 = 𝑍 → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) ) / 𝑧 ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑍 ) )
222	221	breq1d	⊢ ( 𝑧 = 𝑍 → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) ) / 𝑧 ) ≤ 𝐶 ↔ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑍 ) ≤ 𝐶 ) )
223		1re	⊢ 1 ∈ ℝ
224		rexr	⊢ ( 1 ∈ ℝ → 1 ∈ ℝ* )
225		elioopnf	⊢ ( 1 ∈ ℝ* → ( 𝑍 ∈ ( 1 (,) +∞ ) ↔ ( 𝑍 ∈ ℝ ∧ 1 < 𝑍 ) ) )
226	223 224 225	mp2b	⊢ ( 𝑍 ∈ ( 1 (,) +∞ ) ↔ ( 𝑍 ∈ ℝ ∧ 1 < 𝑍 ) )
227	133 135 226	sylanbrc	⊢ ( 𝜑 → 𝑍 ∈ ( 1 (,) +∞ ) )
228	222 20 227	rspcdva	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑍 ) ≤ 𝐶 )
229	199 228	eqbrtrrd	⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) ≤ 𝐶 )
230	30 152 62	lesubadd2d	⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) ≤ 𝐶 ↔ ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) ≤ ( ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) + 𝐶 ) ) )
231	229 230	mpbid	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) ≤ ( ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) + 𝐶 ) )
232		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
233	148	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ∈ ℂ )
234	233 186	mulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
235	138 234	fsumcl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
236	136	rpne0d	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ≠ 0 )
237	232 235 66 236	div23d	⊢ ( 𝜑 → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑍 ) ) = ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) )
238	29	resqcld	⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) ↑ 2 ) ∈ ℝ )
239	57 238	remulcld	⊢ ( 𝜑 → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ∈ ℝ )
240	41 239	remulcld	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ∈ ℝ )
241		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ∈ ℝ ) → ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ∈ ℝ )
242	36 240 241	sylancr	⊢ ( 𝜑 → ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ∈ ℝ )
243	35 29	remulcld	⊢ ( 𝜑 → ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
244		remulcl	⊢ ( ( 2 ∈ ℝ ∧ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
245	36 151 244	sylancr	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
246	31	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑈 ∈ ℝ )
247	246 141	nndivred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑈 / 𝑛 ) ∈ ℝ )
248	247 148	resubcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) ∈ ℝ )
249	248 149	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
250	138 249	fsumrecl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
251	37 250	remulcld	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
252	243 245	resubcld	⊢ ( 𝜑 → ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
253	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	pntlemf	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
254		2pos	⊢ 0 < 2
255	254	a1i	⊢ ( 𝜑 → 0 < 2 )
256		lemul2	⊢ ( ( ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ∈ ℝ ∧ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ≤ ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
257	240 250 37 255 256	syl112anc	⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ≤ ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
258	253 257	mpbid	⊢ ( 𝜑 → ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ≤ ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
259	247	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑈 / 𝑛 ) ∈ ℂ )
260	259 233 186	subdird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) = ( ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) )
261	260	sumeq2dv	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) )
262	247 149	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
263	262	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
264	138 263 234	fsumsub	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) )
265	261 264	eqtrd	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) )
266	265	oveq2d	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) )
267	138 262	fsumrecl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
268	267	recnd	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
269	232 268 235	subdid	⊢ ( 𝜑 → ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) )
270	266 269	eqtrd	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) )
271		remulcl	⊢ ( ( 2 ∈ ℝ ∧ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℝ ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
272	36 267 271	sylancr	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
273	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	pntlemk	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) ≤ ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) )
274	272 243 245 273	lesub1dd	⊢ ( 𝜑 → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) ≤ ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) )
275	270 274	eqbrtrd	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ≤ ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) )
276	242 251 252 258 275	letrd	⊢ ( 𝜑 → ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ≤ ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ) )
277	242 243 245 276	lesubd	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ≤ ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ) )
278	35	recnd	⊢ ( 𝜑 → ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) ∈ ℂ )
279	60	recnd	⊢ ( 𝜑 → ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ∈ ℂ )
280	278 279 66	subdird	⊢ ( 𝜑 → ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) · ( log ‘ 𝑍 ) ) = ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) · ( log ‘ 𝑍 ) ) ) )
281	59	recnd	⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ∈ ℂ )
282	232 281 66	mulassd	⊢ ( 𝜑 → ( ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) · ( log ‘ 𝑍 ) ) = ( 2 · ( ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) ) )
283	65 66 66	mulassd	⊢ ( 𝜑 → ( ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) = ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) ) )
284	66	sqvald	⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) ↑ 2 ) = ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) )
285	284	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) = ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) ) )
286	56	rpcnd	⊢ ( 𝜑 → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ∈ ℂ )
287	238	recnd	⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) ↑ 2 ) ∈ ℂ )
288	122 286 287	mulassd	⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) = ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) )
289	283 285 288	3eqtr2d	⊢ ( 𝜑 → ( ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) = ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) )
290	289	oveq2d	⊢ ( 𝜑 → ( 2 · ( ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) ) = ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) )
291	282 290	eqtrd	⊢ ( 𝜑 → ( ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) · ( log ‘ 𝑍 ) ) = ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) )
292	291	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) · ( log ‘ 𝑍 ) ) ) = ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ) )
293	280 292	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) · ( log ‘ 𝑍 ) ) = ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) − ( 2 · ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ) ) )
294	277 293	breqtrrd	⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ≤ ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) · ( log ‘ 𝑍 ) ) )
295	245 61 136	ledivmul2d	⊢ ( 𝜑 → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑍 ) ) ≤ ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) ↔ ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ≤ ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) · ( log ‘ 𝑍 ) ) ) )
296	294 295	mpbird	⊢ ( 𝜑 → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑍 ) ) ≤ ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
297	237 296	eqbrtrrd	⊢ ( 𝜑 → ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) ≤ ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
298	152 61 62 297	leadd1dd	⊢ ( 𝜑 → ( ( ( 2 / ( log ‘ 𝑍 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( log ‘ 𝑛 ) ) ) + 𝐶 ) ≤ ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) + 𝐶 ) )
299	30 153 63 231 298	letrd	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) ≤ ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) + 𝐶 ) )
300		remulcl	⊢ ( ( 𝑈 ∈ ℝ ∧ 3 ∈ ℝ ) → ( 𝑈 · 3 ) ∈ ℝ )
301	31 32 300	sylancl	⊢ ( 𝜑 → ( 𝑈 · 3 ) ∈ ℝ )
302	301 62	readdcld	⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) ∈ ℝ )
303	21	simp3d	⊢ ( 𝜑 → ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
304	303	simp3d	⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) )
305	302 59 130 304	leadd2dd	⊢ ( 𝜑 → ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( ( 𝑈 · 3 ) + 𝐶 ) ) ≤ ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
306	33	recnd	⊢ ( 𝜑 → 3 ∈ ℂ )
307	64 66 306	adddid	⊢ ( 𝜑 → ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) = ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( 𝑈 · 3 ) ) )
308	307	oveq1d	⊢ ( 𝜑 → ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) + 𝐶 ) = ( ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( 𝑈 · 3 ) ) + 𝐶 ) )
309	130	recnd	⊢ ( 𝜑 → ( 𝑈 · ( log ‘ 𝑍 ) ) ∈ ℂ )
310	64 306	mulcld	⊢ ( 𝜑 → ( 𝑈 · 3 ) ∈ ℂ )
311	13	rpcnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
312	309 310 311	addassd	⊢ ( 𝜑 → ( ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( 𝑈 · 3 ) ) + 𝐶 ) = ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( ( 𝑈 · 3 ) + 𝐶 ) ) )
313	308 312	eqtrd	⊢ ( 𝜑 → ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) + 𝐶 ) = ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( ( 𝑈 · 3 ) + 𝐶 ) ) )
314	281	2timesd	⊢ ( 𝜑 → ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) = ( ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) + ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
315	314	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) + ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) = ( ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) + ( ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) + ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
316	309 281 281	nppcan3d	⊢ ( 𝜑 → ( ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) + ( ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) + ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) = ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
317	315 316	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) + ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) = ( ( 𝑈 · ( log ‘ 𝑍 ) ) + ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
318	305 313 317	3brtr4d	⊢ ( 𝜑 → ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) + 𝐶 ) ≤ ( ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) + ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
319	35 62	readdcld	⊢ ( 𝜑 → ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) + 𝐶 ) ∈ ℝ )
320	319 60 131	lesubaddd	⊢ ( 𝜑 → ( ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) + 𝐶 ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) ≤ ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ↔ ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) + 𝐶 ) ≤ ( ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) + ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) ) )
321	318 320	mpbird	⊢ ( 𝜑 → ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) + 𝐶 ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) ≤ ( ( 𝑈 · ( log ‘ 𝑍 ) ) − ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
322	278 311 279	addsubd	⊢ ( 𝜑 → ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) + 𝐶 ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) = ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) + 𝐶 ) )
323	321 322 129	3brtr3d	⊢ ( 𝜑 → ( ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) − ( 2 · ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) + 𝐶 ) ≤ ( ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) · ( log ‘ 𝑍 ) ) )
324	30 63 132 299 323	letrd	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) ≤ ( ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) · ( log ‘ 𝑍 ) ) )
325		3z	⊢ 3 ∈ ℤ
326		rpexpcl	⊢ ( ( 𝑈 ∈ ℝ+ ∧ 3 ∈ ℤ ) → ( 𝑈 ↑ 3 ) ∈ ℝ+ )
327	7 325 326	sylancl	⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) ∈ ℝ+ )
328	101 327	rpmulcld	⊢ ( 𝜑 → ( 𝐹 · ( 𝑈 ↑ 3 ) ) ∈ ℝ+ )
329	328	rpred	⊢ ( 𝜑 → ( 𝐹 · ( 𝑈 ↑ 3 ) ) ∈ ℝ )
330	31 329	resubcld	⊢ ( 𝜑 → ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ∈ ℝ )
331	28 330 136	lemul1d	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ↔ ( ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) · ( log ‘ 𝑍 ) ) ≤ ( ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) · ( log ‘ 𝑍 ) ) ) )
332	324 331	mpbird	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑍 ) / 𝑍 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )