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 ffvelcdmi ⊢ ( ( 𝑍 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
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 eqtrid ⊢ ( 𝜑 → ( 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 mulridd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 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 ‘ 𝑛 ) ) )