Metamath Proof Explorer


Theorem pntlemf

Description: Lemma for pnt . Add up the pieces in pntlemi to get an estimate slightly better than the naive lower bound 0 . (Contributed by Mario Carneiro, 13-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 ‘ ( ( 𝑅𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
Assertion pntlemf ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )

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 1 2 3 4 5 6 7 8 9 10 pntlemc ( 𝜑 → ( 𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈𝐸 ) ∈ ℝ+ ) ) )
21 20 simp3d ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈𝐸 ) ∈ ℝ+ ) )
22 21 simp3d ( 𝜑 → ( 𝑈𝐸 ) ∈ ℝ+ )
23 1 2 3 4 5 6 pntlemd ( 𝜑 → ( 𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+ ) )
24 23 simp1d ( 𝜑𝐿 ∈ ℝ+ )
25 20 simp1d ( 𝜑𝐸 ∈ ℝ+ )
26 2z 2 ∈ ℤ
27 rpexpcl ( ( 𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
28 25 26 27 sylancl ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
29 24 28 rpmulcld ( 𝜑 → ( 𝐿 · ( 𝐸 ↑ 2 ) ) ∈ ℝ+ )
30 3nn0 3 ∈ ℕ0
31 2nn 2 ∈ ℕ
32 30 31 decnncl 3 2 ∈ ℕ
33 nnrp ( 3 2 ∈ ℕ → 3 2 ∈ ℝ+ )
34 32 33 ax-mp 3 2 ∈ ℝ+
35 rpmulcl ( ( 3 2 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 3 2 · 𝐵 ) ∈ ℝ+ )
36 34 3 35 sylancr ( 𝜑 → ( 3 2 · 𝐵 ) ∈ ℝ+ )
37 29 36 rpdivcld ( 𝜑 → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ∈ ℝ+ )
38 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 ‘ 𝑍 ) ) ) ) )
39 38 simp1d ( 𝜑𝑍 ∈ ℝ+ )
40 39 rpred ( 𝜑𝑍 ∈ ℝ )
41 38 simp2d ( 𝜑 → ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) )
42 41 simp1d ( 𝜑 → 1 < 𝑍 )
43 40 42 rplogcld ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ+ )
44 rpexpcl ( ( ( log ‘ 𝑍 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( log ‘ 𝑍 ) ↑ 2 ) ∈ ℝ+ )
45 43 26 44 sylancl ( 𝜑 → ( ( log ‘ 𝑍 ) ↑ 2 ) ∈ ℝ+ )
46 37 45 rpmulcld ( 𝜑 → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ∈ ℝ+ )
47 22 46 rpmulcld ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ∈ ℝ+ )
48 47 rpred ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ∈ ℝ )
49 24 25 rpmulcld ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ+ )
50 8re 8 ∈ ℝ
51 8pos 0 < 8
52 50 51 elrpii 8 ∈ ℝ+
53 rpdivcl ( ( ( 𝐿 · 𝐸 ) ∈ ℝ+ ∧ 8 ∈ ℝ+ ) → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℝ+ )
54 49 52 53 sylancl ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℝ+ )
55 54 43 rpmulcld ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ∈ ℝ+ )
56 22 55 rpmulcld ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ+ )
57 56 rpred ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ )
58 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemg ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ𝑀 ) ∧ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁𝑀 ) ) )
59 58 simp1d ( 𝜑𝑀 ∈ ℕ )
60 58 simp2d ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
61 eluznn ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ𝑀 ) ) → 𝑁 ∈ ℕ )
62 59 60 61 syl2anc ( 𝜑𝑁 ∈ ℕ )
63 62 nnred ( 𝜑𝑁 ∈ ℝ )
64 59 nnred ( 𝜑𝑀 ∈ ℝ )
65 63 64 resubcld ( 𝜑 → ( 𝑁𝑀 ) ∈ ℝ )
66 57 65 remulcld ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) ∈ ℝ )
67 fzfid ( 𝜑 → ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ∈ Fin )
68 7 rpred ( 𝜑𝑈 ∈ ℝ )
69 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) → 𝑛 ∈ ℕ )
70 nndivre ( ( 𝑈 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑈 / 𝑛 ) ∈ ℝ )
71 68 69 70 syl2an ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑈 / 𝑛 ) ∈ ℝ )
72 39 adantr ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑍 ∈ ℝ+ )
73 69 adantl ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ℕ )
74 73 nnrpd ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ℝ+ )
75 72 74 rpdivcld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑍 / 𝑛 ) ∈ ℝ+ )
76 1 pntrf 𝑅 : ℝ+ ⟶ ℝ
77 76 ffvelrni ( ( 𝑍 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
78 75 77 syl ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
79 78 72 rerpdivcld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ∈ ℝ )
80 79 recnd ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ∈ ℂ )
81 80 abscld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ∈ ℝ )
82 71 81 resubcld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) ∈ ℝ )
83 74 relogcld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
84 82 83 remulcld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
85 67 84 fsumrecl ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
86 49 rpcnd ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℂ )
87 20 simp2d ( 𝜑𝐾 ∈ ℝ+ )
88 87 rpred ( 𝜑𝐾 ∈ ℝ )
89 21 simp2d ( 𝜑 → 1 < 𝐾 )
90 88 89 rplogcld ( 𝜑 → ( log ‘ 𝐾 ) ∈ ℝ+ )
91 43 90 rpdivcld ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ+ )
92 91 rpcnd ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℂ )
93 rpcnne0 ( 8 ∈ ℝ+ → ( 8 ∈ ℂ ∧ 8 ≠ 0 ) )
94 52 93 mp1i ( 𝜑 → ( 8 ∈ ℂ ∧ 8 ≠ 0 ) )
95 4re 4 ∈ ℝ
96 4pos 0 < 4
97 95 96 elrpii 4 ∈ ℝ+
98 rpcnne0 ( 4 ∈ ℝ+ → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
99 97 98 mp1i ( 𝜑 → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
100 divmuldiv ( ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℂ ) ∧ ( ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) ) → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) = ( ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ) / ( 8 · 4 ) ) )
101 86 92 94 99 100 syl22anc ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) = ( ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ) / ( 8 · 4 ) ) )
102 10 fveq2i ( log ‘ 𝐾 ) = ( log ‘ ( exp ‘ ( 𝐵 / 𝐸 ) ) )
103 3 25 rpdivcld ( 𝜑 → ( 𝐵 / 𝐸 ) ∈ ℝ+ )
104 103 rpred ( 𝜑 → ( 𝐵 / 𝐸 ) ∈ ℝ )
105 104 relogefd ( 𝜑 → ( log ‘ ( exp ‘ ( 𝐵 / 𝐸 ) ) ) = ( 𝐵 / 𝐸 ) )
106 102 105 syl5eq ( 𝜑 → ( log ‘ 𝐾 ) = ( 𝐵 / 𝐸 ) )
107 106 oveq2d ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) = ( ( log ‘ 𝑍 ) / ( 𝐵 / 𝐸 ) ) )
108 43 rpcnd ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℂ )
109 3 rpcnne0d ( 𝜑 → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
110 25 rpcnne0d ( 𝜑 → ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) )
111 divdiv2 ( ( ( log ‘ 𝑍 ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) ) → ( ( log ‘ 𝑍 ) / ( 𝐵 / 𝐸 ) ) = ( ( ( log ‘ 𝑍 ) · 𝐸 ) / 𝐵 ) )
112 108 109 110 111 syl3anc ( 𝜑 → ( ( log ‘ 𝑍 ) / ( 𝐵 / 𝐸 ) ) = ( ( ( log ‘ 𝑍 ) · 𝐸 ) / 𝐵 ) )
113 107 112 eqtrd ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) = ( ( ( log ‘ 𝑍 ) · 𝐸 ) / 𝐵 ) )
114 113 oveq2d ( 𝜑 → ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ) = ( ( 𝐿 · 𝐸 ) · ( ( ( log ‘ 𝑍 ) · 𝐸 ) / 𝐵 ) ) )
115 25 rpcnd ( 𝜑𝐸 ∈ ℂ )
116 108 115 mulcld ( 𝜑 → ( ( log ‘ 𝑍 ) · 𝐸 ) ∈ ℂ )
117 divass ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( ( log ‘ 𝑍 ) · 𝐸 ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) · 𝐸 ) ) / 𝐵 ) = ( ( 𝐿 · 𝐸 ) · ( ( ( log ‘ 𝑍 ) · 𝐸 ) / 𝐵 ) ) )
118 86 116 109 117 syl3anc ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) · 𝐸 ) ) / 𝐵 ) = ( ( 𝐿 · 𝐸 ) · ( ( ( log ‘ 𝑍 ) · 𝐸 ) / 𝐵 ) ) )
119 24 rpcnd ( 𝜑𝐿 ∈ ℂ )
120 119 115 108 115 mul4d ( 𝜑 → ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) · 𝐸 ) ) = ( ( 𝐿 · ( log ‘ 𝑍 ) ) · ( 𝐸 · 𝐸 ) ) )
121 115 sqvald ( 𝜑 → ( 𝐸 ↑ 2 ) = ( 𝐸 · 𝐸 ) )
122 121 oveq2d ( 𝜑 → ( ( 𝐿 · ( log ‘ 𝑍 ) ) · ( 𝐸 ↑ 2 ) ) = ( ( 𝐿 · ( log ‘ 𝑍 ) ) · ( 𝐸 · 𝐸 ) ) )
123 115 sqcld ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
124 119 108 123 mul32d ( 𝜑 → ( ( 𝐿 · ( log ‘ 𝑍 ) ) · ( 𝐸 ↑ 2 ) ) = ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) )
125 120 122 124 3eqtr2d ( 𝜑 → ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) · 𝐸 ) ) = ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) )
126 125 oveq1d ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) · 𝐸 ) ) / 𝐵 ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / 𝐵 ) )
127 114 118 126 3eqtr2d ( 𝜑 → ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / 𝐵 ) )
128 8t4e32 ( 8 · 4 ) = 3 2
129 128 a1i ( 𝜑 → ( 8 · 4 ) = 3 2 )
130 127 129 oveq12d ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) · ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ) / ( 8 · 4 ) ) = ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / 𝐵 ) / 3 2 ) )
131 29 rpcnd ( 𝜑 → ( 𝐿 · ( 𝐸 ↑ 2 ) ) ∈ ℂ )
132 131 108 mulcld ( 𝜑 → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) ∈ ℂ )
133 rpcnne0 ( 3 2 ∈ ℝ+ → ( 3 2 ∈ ℂ ∧ 3 2 ≠ 0 ) )
134 34 133 mp1i ( 𝜑 → ( 3 2 ∈ ℂ ∧ 3 2 ≠ 0 ) )
135 divdiv1 ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 3 2 ∈ ℂ ∧ 3 2 ≠ 0 ) ) → ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / 𝐵 ) / 3 2 ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / ( 𝐵 · 3 2 ) ) )
136 132 109 134 135 syl3anc ( 𝜑 → ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / 𝐵 ) / 3 2 ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / ( 𝐵 · 3 2 ) ) )
137 32 nncni 3 2 ∈ ℂ
138 3 rpcnd ( 𝜑𝐵 ∈ ℂ )
139 mulcom ( ( 3 2 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 3 2 · 𝐵 ) = ( 𝐵 · 3 2 ) )
140 137 138 139 sylancr ( 𝜑 → ( 3 2 · 𝐵 ) = ( 𝐵 · 3 2 ) )
141 140 oveq2d ( 𝜑 → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / ( 3 2 · 𝐵 ) ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / ( 𝐵 · 3 2 ) ) )
142 36 rpcnne0d ( 𝜑 → ( ( 3 2 · 𝐵 ) ∈ ℂ ∧ ( 3 2 · 𝐵 ) ≠ 0 ) )
143 div23 ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) ∈ ℂ ∧ ( log ‘ 𝑍 ) ∈ ℂ ∧ ( ( 3 2 · 𝐵 ) ∈ ℂ ∧ ( 3 2 · 𝐵 ) ≠ 0 ) ) → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / ( 3 2 · 𝐵 ) ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) )
144 131 108 142 143 syl3anc ( 𝜑 → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / ( 3 2 · 𝐵 ) ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) )
145 136 141 144 3eqtr2d ( 𝜑 → ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) · ( log ‘ 𝑍 ) ) / 𝐵 ) / 3 2 ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) )
146 101 130 145 3eqtrd ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) )
147 146 oveq1d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) · ( log ‘ 𝑍 ) ) = ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) )
148 54 rpcnd ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℂ )
149 91 rpred ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ )
150 4nn 4 ∈ ℕ
151 nndivre ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ ∧ 4 ∈ ℕ ) → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ )
152 149 150 151 sylancl ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ )
153 152 recnd ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℂ )
154 148 108 153 mul32d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) · ( log ‘ 𝑍 ) ) )
155 108 sqvald ( 𝜑 → ( ( log ‘ 𝑍 ) ↑ 2 ) = ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) )
156 155 oveq2d ( 𝜑 → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) ) )
157 37 rpcnd ( 𝜑 → ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ∈ ℂ )
158 157 108 108 mulassd ( 𝜑 → ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) ) )
159 156 158 eqtr4d ( 𝜑 → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) = ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) · ( log ‘ 𝑍 ) ) )
160 147 154 159 3eqtr4d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) = ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) )
161 58 simp3d ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁𝑀 ) )
162 152 65 55 lemul2d ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁𝑀 ) ↔ ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) ≤ ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( 𝑁𝑀 ) ) ) )
163 161 162 mpbid ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) ≤ ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( 𝑁𝑀 ) ) )
164 160 163 eqbrtrrd ( 𝜑 → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ≤ ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( 𝑁𝑀 ) ) )
165 46 rpred ( 𝜑 → ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ∈ ℝ )
166 55 rpred ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
167 166 65 remulcld ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( 𝑁𝑀 ) ) ∈ ℝ )
168 165 167 22 lemul2d ( 𝜑 → ( ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ≤ ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( 𝑁𝑀 ) ) ↔ ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ≤ ( ( 𝑈𝐸 ) · ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( 𝑁𝑀 ) ) ) ) )
169 164 168 mpbid ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ≤ ( ( 𝑈𝐸 ) · ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( 𝑁𝑀 ) ) ) )
170 22 rpcnd ( 𝜑 → ( 𝑈𝐸 ) ∈ ℂ )
171 55 rpcnd ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ∈ ℂ )
172 65 recnd ( 𝜑 → ( 𝑁𝑀 ) ∈ ℂ )
173 170 171 172 mulassd ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) = ( ( 𝑈𝐸 ) · ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) · ( 𝑁𝑀 ) ) ) )
174 169 173 breqtrrd ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ≤ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) )
175 fzfid ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ∈ Fin )
176 62 nnzd ( 𝜑𝑁 ∈ ℤ )
177 87 176 rpexpcld ( 𝜑 → ( 𝐾𝑁 ) ∈ ℝ+ )
178 39 177 rpdivcld ( 𝜑 → ( 𝑍 / ( 𝐾𝑁 ) ) ∈ ℝ+ )
179 178 rprege0d ( 𝜑 → ( ( 𝑍 / ( 𝐾𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( 𝐾𝑁 ) ) ) )
180 flge0nn0 ( ( ( 𝑍 / ( 𝐾𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( 𝐾𝑁 ) ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) ∈ ℕ0 )
181 nn0p1nn ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ∈ ℕ )
182 179 180 181 3syl ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ∈ ℕ )
183 nnuz ℕ = ( ℤ ‘ 1 )
184 182 183 eleqtrdi ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ∈ ( ℤ ‘ 1 ) )
185 fzss1 ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ∈ ( ℤ ‘ 1 ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
186 184 185 syl ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
187 186 sselda ( ( 𝜑𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
188 187 84 syldan ( ( 𝜑𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
189 175 188 fsumrecl ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
190 eluzfz2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
191 60 190 syl ( 𝜑𝑁 ∈ ( 𝑀 ... 𝑁 ) )
192 oveq1 ( 𝑚 = 𝑀 → ( 𝑚𝑀 ) = ( 𝑀𝑀 ) )
193 192 oveq2d ( 𝑚 = 𝑀 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) = ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑀𝑀 ) ) )
194 oveq2 ( 𝑚 = 𝑀 → ( 𝐾𝑚 ) = ( 𝐾𝑀 ) )
195 194 oveq2d ( 𝑚 = 𝑀 → ( 𝑍 / ( 𝐾𝑚 ) ) = ( 𝑍 / ( 𝐾𝑀 ) ) )
196 195 fveq2d ( 𝑚 = 𝑀 → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) = ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) )
197 196 oveq1d ( 𝑚 = 𝑀 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) = ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) )
198 197 oveq1d ( 𝑚 = 𝑀 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
199 198 sumeq1d ( 𝑚 = 𝑀 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
200 193 199 breq12d ( 𝑚 = 𝑀 → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑀𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
201 200 imbi2d ( 𝑚 = 𝑀 → ( ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ↔ ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑀𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
202 oveq1 ( 𝑚 = 𝑗 → ( 𝑚𝑀 ) = ( 𝑗𝑀 ) )
203 202 oveq2d ( 𝑚 = 𝑗 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) = ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) )
204 oveq2 ( 𝑚 = 𝑗 → ( 𝐾𝑚 ) = ( 𝐾𝑗 ) )
205 204 oveq2d ( 𝑚 = 𝑗 → ( 𝑍 / ( 𝐾𝑚 ) ) = ( 𝑍 / ( 𝐾𝑗 ) ) )
206 205 fveq2d ( 𝑚 = 𝑗 → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) = ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) )
207 206 oveq1d ( 𝑚 = 𝑗 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) = ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) )
208 207 oveq1d ( 𝑚 = 𝑗 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
209 208 sumeq1d ( 𝑚 = 𝑗 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
210 203 209 breq12d ( 𝑚 = 𝑗 → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
211 210 imbi2d ( 𝑚 = 𝑗 → ( ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ↔ ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
212 oveq1 ( 𝑚 = ( 𝑗 + 1 ) → ( 𝑚𝑀 ) = ( ( 𝑗 + 1 ) − 𝑀 ) )
213 212 oveq2d ( 𝑚 = ( 𝑗 + 1 ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) = ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) )
214 oveq2 ( 𝑚 = ( 𝑗 + 1 ) → ( 𝐾𝑚 ) = ( 𝐾 ↑ ( 𝑗 + 1 ) ) )
215 214 oveq2d ( 𝑚 = ( 𝑗 + 1 ) → ( 𝑍 / ( 𝐾𝑚 ) ) = ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) )
216 215 fveq2d ( 𝑚 = ( 𝑗 + 1 ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) = ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) )
217 216 oveq1d ( 𝑚 = ( 𝑗 + 1 ) → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) = ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) )
218 217 oveq1d ( 𝑚 = ( 𝑗 + 1 ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
219 218 sumeq1d ( 𝑚 = ( 𝑗 + 1 ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
220 213 219 breq12d ( 𝑚 = ( 𝑗 + 1 ) → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
221 220 imbi2d ( 𝑚 = ( 𝑗 + 1 ) → ( ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ↔ ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
222 oveq1 ( 𝑚 = 𝑁 → ( 𝑚𝑀 ) = ( 𝑁𝑀 ) )
223 222 oveq2d ( 𝑚 = 𝑁 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) = ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) )
224 oveq2 ( 𝑚 = 𝑁 → ( 𝐾𝑚 ) = ( 𝐾𝑁 ) )
225 224 oveq2d ( 𝑚 = 𝑁 → ( 𝑍 / ( 𝐾𝑚 ) ) = ( 𝑍 / ( 𝐾𝑁 ) ) )
226 225 fveq2d ( 𝑚 = 𝑁 → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) = ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) )
227 226 oveq1d ( 𝑚 = 𝑁 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) = ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) )
228 227 oveq1d ( 𝑚 = 𝑁 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
229 228 sumeq1d ( 𝑚 = 𝑁 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
230 223 229 breq12d ( 𝑚 = 𝑁 → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
231 230 imbi2d ( 𝑚 = 𝑁 → ( ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑚𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑚 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ↔ ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
232 59 nncnd ( 𝜑𝑀 ∈ ℂ )
233 232 subidd ( 𝜑 → ( 𝑀𝑀 ) = 0 )
234 233 oveq2d ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑀𝑀 ) ) = ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · 0 ) )
235 56 rpcnd ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℂ )
236 235 mul01d ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · 0 ) = 0 )
237 234 236 eqtrd ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑀𝑀 ) ) = 0 )
238 fzfid ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ∈ Fin )
239 59 nnzd ( 𝜑𝑀 ∈ ℤ )
240 87 239 rpexpcld ( 𝜑 → ( 𝐾𝑀 ) ∈ ℝ+ )
241 39 240 rpdivcld ( 𝜑 → ( 𝑍 / ( 𝐾𝑀 ) ) ∈ ℝ+ )
242 241 rprege0d ( 𝜑 → ( ( 𝑍 / ( 𝐾𝑀 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( 𝐾𝑀 ) ) ) )
243 flge0nn0 ( ( ( 𝑍 / ( 𝐾𝑀 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( 𝐾𝑀 ) ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) ∈ ℕ0 )
244 nn0p1nn ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ∈ ℕ )
245 242 243 244 3syl ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ∈ ℕ )
246 245 183 eleqtrdi ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ∈ ( ℤ ‘ 1 ) )
247 fzss1 ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ∈ ( ℤ ‘ 1 ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
248 246 247 syl ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
249 248 sselda ( ( 𝜑𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
250 249 84 syldan ( ( 𝜑𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
251 elfzle2 ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) → 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) )
252 251 adantl ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) )
253 11 simpld ( 𝜑𝑌 ∈ ℝ+ )
254 39 253 rpdivcld ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℝ+ )
255 254 rpred ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℝ )
256 elfzelz ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) → 𝑛 ∈ ℤ )
257 flge ( ( ( 𝑍 / 𝑌 ) ∈ ℝ ∧ 𝑛 ∈ ℤ ) → ( 𝑛 ≤ ( 𝑍 / 𝑌 ) ↔ 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
258 255 256 257 syl2an ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑛 ≤ ( 𝑍 / 𝑌 ) ↔ 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
259 252 258 mpbird ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ≤ ( 𝑍 / 𝑌 ) )
260 73 259 jca ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝑍 / 𝑌 ) ) )
261 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 pntlemn ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝑍 / 𝑌 ) ) ) → 0 ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
262 260 261 syldan ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 0 ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
263 249 262 syldan ( ( 𝜑𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 0 ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
264 238 250 263 fsumge0 ( 𝜑 → 0 ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
265 237 264 eqbrtrd ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑀𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
266 265 a1i ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑀𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑀 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
267 eqid ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) )
268 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 267 pntlemi ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
269 56 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ+ )
270 269 rpred ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ )
271 elfzoelz ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑗 ∈ ℤ )
272 271 adantl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 ∈ ℤ )
273 272 zred ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 ∈ ℝ )
274 59 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℕ )
275 274 nnred ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
276 273 275 resubcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑗𝑀 ) ∈ ℝ )
277 270 276 remulcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ∈ ℝ )
278 fzfid ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ∈ Fin )
279 ssun1 ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ⊆ ( ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
280 40 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑍 ∈ ℝ )
281 87 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐾 ∈ ℝ+ )
282 272 peano2zd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ℤ )
283 281 282 rpexpcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾 ↑ ( 𝑗 + 1 ) ) ∈ ℝ+ )
284 280 283 rerpdivcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ )
285 281 272 rpexpcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾𝑗 ) ∈ ℝ+ )
286 280 285 rerpdivcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑍 / ( 𝐾𝑗 ) ) ∈ ℝ )
287 88 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐾 ∈ ℝ )
288 1re 1 ∈ ℝ
289 ltle ( ( 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 1 < 𝐾 → 1 ≤ 𝐾 ) )
290 288 88 289 sylancr ( 𝜑 → ( 1 < 𝐾 → 1 ≤ 𝐾 ) )
291 89 290 mpd ( 𝜑 → 1 ≤ 𝐾 )
292 291 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 1 ≤ 𝐾 )
293 uzid ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ𝑗 ) )
294 peano2uz ( 𝑗 ∈ ( ℤ𝑗 ) → ( 𝑗 + 1 ) ∈ ( ℤ𝑗 ) )
295 272 293 294 3syl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ( ℤ𝑗 ) )
296 287 292 295 leexp2ad ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾𝑗 ) ≤ ( 𝐾 ↑ ( 𝑗 + 1 ) ) )
297 39 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑍 ∈ ℝ+ )
298 285 283 297 lediv2d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐾𝑗 ) ≤ ( 𝐾 ↑ ( 𝑗 + 1 ) ) ↔ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝑍 / ( 𝐾𝑗 ) ) ) )
299 296 298 mpbid ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝑍 / ( 𝐾𝑗 ) ) )
300 flword2 ( ( ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ ∧ ( 𝑍 / ( 𝐾𝑗 ) ) ∈ ℝ ∧ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝑍 / ( 𝐾𝑗 ) ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) ) )
301 284 286 299 300 syl3anc ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) ) )
302 eluzp1p1 ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) ) → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ∈ ( ℤ ‘ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ) )
303 301 302 syl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ∈ ( ℤ ‘ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ) )
304 286 flcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ∈ ℤ )
305 254 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑍 / 𝑌 ) ∈ ℝ+ )
306 305 rpred ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑍 / 𝑌 ) ∈ ℝ )
307 306 flcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℤ )
308 253 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 ∈ ℝ+ )
309 308 rpred ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 ∈ ℝ )
310 285 rpred ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾𝑗 ) ∈ ℝ )
311 12 simpld ( 𝜑𝑋 ∈ ℝ+ )
312 311 rpred ( 𝜑𝑋 ∈ ℝ )
313 312 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℝ )
314 12 simprd ( 𝜑𝑌 < 𝑋 )
315 314 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 < 𝑋 )
316 elfzofz ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
317 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemh ( ( 𝜑𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾𝑗 ) ∧ ( 𝐾𝑗 ) ≤ ( √ ‘ 𝑍 ) ) )
318 316 317 sylan2 ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 < ( 𝐾𝑗 ) ∧ ( 𝐾𝑗 ) ≤ ( √ ‘ 𝑍 ) ) )
319 318 simpld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 < ( 𝐾𝑗 ) )
320 309 313 310 315 319 lttrd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 < ( 𝐾𝑗 ) )
321 309 310 320 ltled ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 ≤ ( 𝐾𝑗 ) )
322 308 285 297 lediv2d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑌 ≤ ( 𝐾𝑗 ) ↔ ( 𝑍 / ( 𝐾𝑗 ) ) ≤ ( 𝑍 / 𝑌 ) ) )
323 321 322 mpbid ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑍 / ( 𝐾𝑗 ) ) ≤ ( 𝑍 / 𝑌 ) )
324 flwordi ( ( ( 𝑍 / ( 𝐾𝑗 ) ) ∈ ℝ ∧ ( 𝑍 / 𝑌 ) ∈ ℝ ∧ ( 𝑍 / ( 𝐾𝑗 ) ) ≤ ( 𝑍 / 𝑌 ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) )
325 286 306 323 324 syl3anc ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) )
326 eluz2 ( ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ↔ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
327 304 307 325 326 syl3anbrc ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) )
328 fzsplit2 ( ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ∈ ( ℤ ‘ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ) ∧ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) = ( ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) )
329 303 327 328 syl2anc ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) = ( ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) )
330 279 329 sseqtrrid ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ⊆ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
331 297 283 rpdivcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ+ )
332 331 rprege0d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) )
333 flge0nn0 ( ( ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℕ0 )
334 nn0p1nn ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ∈ ℕ )
335 332 333 334 3syl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ∈ ℕ )
336 335 183 eleqtrdi ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ∈ ( ℤ ‘ 1 ) )
337 fzss1 ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ∈ ( ℤ ‘ 1 ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
338 336 337 syl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
339 330 338 sstrd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
340 339 sselda ( ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
341 84 adantlr ( ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
342 340 341 syldan ( ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
343 278 342 fsumrecl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
344 fzfid ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ∈ Fin )
345 ssun2 ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
346 345 329 sseqtrrid ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
347 346 338 sstrd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
348 347 sselda ( ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
349 348 341 syldan ( ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
350 344 349 fsumrecl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
351 le2add ( ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ ∧ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ∈ ℝ ) ∧ ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ ∧ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ ) ) → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∧ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) + ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ) ≤ ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
352 270 277 343 350 351 syl22anc ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∧ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) + ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ) ≤ ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
353 268 352 mpand ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) + ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ) ≤ ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
354 235 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℂ )
355 1cnd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 1 ∈ ℂ )
356 272 zcnd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 ∈ ℂ )
357 232 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℂ )
358 356 357 subcld ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑗𝑀 ) ∈ ℂ )
359 354 355 358 adddid ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 1 + ( 𝑗𝑀 ) ) ) = ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · 1 ) + ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ) )
360 355 358 addcomd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 1 + ( 𝑗𝑀 ) ) = ( ( 𝑗𝑀 ) + 1 ) )
361 356 355 357 addsubd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑗 + 1 ) − 𝑀 ) = ( ( 𝑗𝑀 ) + 1 ) )
362 360 361 eqtr4d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 1 + ( 𝑗𝑀 ) ) = ( ( 𝑗 + 1 ) − 𝑀 ) )
363 362 oveq2d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 1 + ( 𝑗𝑀 ) ) ) = ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) )
364 354 mulid1d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · 1 ) = ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) )
365 364 oveq1d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · 1 ) + ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ) = ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) + ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ) )
366 359 363 365 3eqtr3d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) = ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) + ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ) )
367 reflcl ( ( 𝑍 / ( 𝐾𝑗 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ∈ ℝ )
368 286 367 syl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ∈ ℝ )
369 368 ltp1d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) < ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) )
370 fzdisj ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) < ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) → ( ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) = ∅ )
371 369 370 syl ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) = ∅ )
372 fzfid ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ∈ Fin )
373 338 sselda ( ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
374 373 341 syldan ( ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
375 374 recnd ( ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
376 371 329 372 375 fsumsplit ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
377 366 376 breq12d ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) + ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ) ≤ ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
378 353 377 sylibrd ( ( 𝜑𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
379 378 expcom ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜑 → ( ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
380 379 a2d ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑗𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑗 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) → ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( ( 𝑗 + 1 ) − 𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝑗 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
381 201 211 221 231 266 380 fzind2 ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
382 191 381 mpcom ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
383 67 84 262 186 fsumless ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾𝑁 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
384 66 189 85 382 383 letrd ( 𝜑 → ( ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) · ( 𝑁𝑀 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
385 48 66 85 174 384 letrd ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) · ( ( log ‘ 𝑍 ) ↑ 2 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )