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 ‘ 𝑛 ) ) )