Metamath Proof Explorer

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 ffvelrni ⊢ ( 𝑍 ∈ ℝ+ → ( 𝑅 ‘ 𝑍 ) ∈ ℝ )
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 syl5eq ⊢ ( 𝜑 → ( 𝐸 ↑ 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 syl5eq ⊢ ( 𝜑 → ( 𝑈 ↑ 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 mulid2d ⊢ ( 𝜑 → ( 1 · 𝑈 ) = 𝑈 )
109 64 75 76 divrec2d ⊢ ( 𝜑 → ( 𝑈 / 𝐷 ) = ( ( 1 / 𝐷 ) · 𝑈 ) )
110 9 109 syl5req ⊢ ( 𝜑 → ( ( 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 syl5eq ⊢ ( 𝜑 → ( 𝐹 · 𝑈 ) = ( ( ( 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 ffvelrni ⊢ ( ( 𝑍 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
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 syl5eq ⊢ ( 𝑧 = 𝑍 → Σ 𝑖 ∈ ( 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 ) ) ) )