Theorem dchrvmasumiflem1

Description: Lemma for dchrvmasumif . (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrvmasumif.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
	dchrvmasumif.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
	dchrvmasumif.s	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
	dchrvmasumif.1	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
	dchrvmasumif.g	⊢ 𝐾 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) )
	dchrvmasumif.e	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
	dchrvmasumif.t	⊢ ( 𝜑 → seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
	dchrvmasumif.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
Assertion	dchrvmasumiflem1	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrvmasumif.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10		dchrvmasumif.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11		dchrvmasumif.s	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
12		dchrvmasumif.1	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
13		dchrvmasumif.g	⊢ 𝐾 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) )
14		dchrvmasumif.e	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
15		dchrvmasumif.t	⊢ ( 𝜑 → seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
16		dchrvmasumif.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
17		fzfid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑚 ) ) ∈ Fin )
18		simpl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝜑 )
19		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) → 𝑘 ∈ ℕ )
20	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
21		nnz	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
22	21	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
23	4 1 5 2 20 22	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ )
24	18 19 23	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝑚 ∈ ℝ+ )
26	19	nnrpd	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) → 𝑘 ∈ ℝ+ )
27		ifcl	⊢ ( ( 𝑚 ∈ ℝ+ ∧ 𝑘 ∈ ℝ+ ) → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ∈ ℝ+ )
28	25 26 27	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ∈ ℝ+ )
29	28	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ∈ ℝ )
30	19	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → 𝑘 ∈ ℕ )
31	29 30	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ∈ ℝ )
32	31	recnd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ∈ ℂ )
33	24 32	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ∈ ℂ )
34	17 33	fsumcl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ∈ ℂ )
35		fveq2	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( ⌊ ‘ 𝑚 ) = ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) )
36	35	oveq2d	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( 1 ... ( ⌊ ‘ 𝑚 ) ) = ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) )
37		ifeq1	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) = if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) )
38	37	fveq2d	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) = ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) )
39	38	oveq1d	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) = ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) )
40	39	oveq2d	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) )
41	40	adantr	⊢ ( ( 𝑚 = ( 𝑥 / 𝑑 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) )
42	36 41	sumeq12rdv	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) )
43	10 14	ifcld	⊢ ( 𝜑 → if ( 𝑆 = 0 , 𝐶 , 𝐸 ) ∈ ( 0 [,) +∞ ) )
44		0cn	⊢ 0 ∈ ℂ
45		climcl	⊢ ( seq 1 ( + , 𝐾 ) ⇝ 𝑇 → 𝑇 ∈ ℂ )
46	15 45	syl	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
47		ifcl	⊢ ( ( 0 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ ℂ )
48	44 46 47	sylancr	⊢ ( 𝜑 → if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ ℂ )
49		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
50		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
51		nncn	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
52	51	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
53		nnne0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
54	53	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ≠ 0 )
55	23 52 54	divcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ∈ ℂ )
56		2fveq3	⊢ ( 𝑎 = 𝑘 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) )
57		id	⊢ ( 𝑎 = 𝑘 → 𝑎 = 𝑘 )
58	56 57	oveq12d	⊢ ( 𝑎 = 𝑘 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) )
59	58	cbvmptv	⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) )
60	9 59	eqtri	⊢ 𝐹 = ( 𝑘 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) )
61	55 60	fmptd	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℂ )
62		ffvelcdm	⊢ ( ( 𝐹 : ℕ ⟶ ℂ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
63	61 62	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
64	49 50 63	serf	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
65	64	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
66		3re	⊢ 3 ∈ ℝ
67		elicopnf	⊢ ( 3 ∈ ℝ → ( 𝑚 ∈ ( 3 [,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 3 ≤ 𝑚 ) ) )
68	66 67	mp1i	⊢ ( 𝜑 → ( 𝑚 ∈ ( 3 [,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 3 ≤ 𝑚 ) ) )
69	68	simprbda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 𝑚 ∈ ℝ )
70		1red	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 1 ∈ ℝ )
71	66	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 3 ∈ ℝ )
72		1le3	⊢ 1 ≤ 3
73	72	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 1 ≤ 3 )
74	68	simplbda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 3 ≤ 𝑚 )
75	70 71 69 73 74	letrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 1 ≤ 𝑚 )
76		flge1nn	⊢ ( ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
77	69 75 76	syl2anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
78	77	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
79	65 78	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ∈ ℂ )
80	79	abscld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ∈ ℝ )
81		simpl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 𝜑 )
82		0red	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 0 ∈ ℝ )
83		3pos	⊢ 0 < 3
84	83	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 0 < 3 )
85	82 71 69 84 74	ltletrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 0 < 𝑚 )
86	69 85	elrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 𝑚 ∈ ℝ+ )
87	81 86	jca	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) )
88		elrege0	⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
89	88	simplbi	⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) → 𝐶 ∈ ℝ )
90	10 89	syl	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
91		rerpdivcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑚 ∈ ℝ+ ) → ( 𝐶 / 𝑚 ) ∈ ℝ )
92	90 91	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( 𝐶 / 𝑚 ) ∈ ℝ )
93	87 92	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( 𝐶 / 𝑚 ) ∈ ℝ )
94	93	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( 𝐶 / 𝑚 ) ∈ ℝ )
95	86	relogcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
96	69 75	logge0d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 0 ≤ ( log ‘ 𝑚 ) )
97	95 96	jca	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( ( log ‘ 𝑚 ) ∈ ℝ ∧ 0 ≤ ( log ‘ 𝑚 ) ) )
98	97	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( ( log ‘ 𝑚 ) ∈ ℝ ∧ 0 ≤ ( log ‘ 𝑚 ) ) )
99		oveq2	⊢ ( 𝑆 = 0 → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑆 ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 0 ) )
100	64	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
101	100 77	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ∈ ℂ )
102	101	subid1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 0 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
103	99 102	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑆 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
104	103	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑆 ) ) = ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) )
105		2fveq3	⊢ ( 𝑦 = 𝑚 → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
106	105	fvoveq1d	⊢ ( 𝑦 = 𝑚 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑆 ) ) )
107		oveq2	⊢ ( 𝑦 = 𝑚 → ( 𝐶 / 𝑦 ) = ( 𝐶 / 𝑚 ) )
108	106 107	breq12d	⊢ ( 𝑦 = 𝑚 → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑚 ) ) )
109	12	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
110		1re	⊢ 1 ∈ ℝ
111		elicopnf	⊢ ( 1 ∈ ℝ → ( 𝑚 ∈ ( 1 [,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ) ) )
112	110 111	ax-mp	⊢ ( 𝑚 ∈ ( 1 [,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ) )
113	69 75 112	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → 𝑚 ∈ ( 1 [,) +∞ ) )
114	108 109 113	rspcdva	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑚 ) )
115	114	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑚 ) )
116	104 115	eqbrtrrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ≤ ( 𝐶 / 𝑚 ) )
117		lemul2a	⊢ ( ( ( ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ∈ ℝ ∧ ( 𝐶 / 𝑚 ) ∈ ℝ ∧ ( ( log ‘ 𝑚 ) ∈ ℝ ∧ 0 ≤ ( log ‘ 𝑚 ) ) ) ∧ ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ≤ ( 𝐶 / 𝑚 ) ) → ( ( log ‘ 𝑚 ) · ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) ≤ ( ( log ‘ 𝑚 ) · ( 𝐶 / 𝑚 ) ) )
118	80 94 98 116 117	syl31anc	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( ( log ‘ 𝑚 ) · ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) ≤ ( ( log ‘ 𝑚 ) · ( 𝐶 / 𝑚 ) ) )
119		iftrue	⊢ ( 𝑆 = 0 → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) = 𝑚 )
120	119	fveq2d	⊢ ( 𝑆 = 0 → ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) = ( log ‘ 𝑚 ) )
121	120	oveq1d	⊢ ( 𝑆 = 0 → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) = ( ( log ‘ 𝑚 ) / 𝑘 ) )
122	121	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) = ( ( log ‘ 𝑚 ) / 𝑘 ) )
123	122	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑚 ) / 𝑘 ) ) )
124	24	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ )
125		relogcl	⊢ ( 𝑚 ∈ ℝ+ → ( log ‘ 𝑚 ) ∈ ℝ )
126	125	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( log ‘ 𝑚 ) ∈ ℝ )
127	126	recnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( log ‘ 𝑚 ) ∈ ℂ )
128	127	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ )
129	19	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → 𝑘 ∈ ℕ )
130	129	nncnd	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → 𝑘 ∈ ℂ )
131	129	nnne0d	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → 𝑘 ≠ 0 )
132	124 128 130 131	div12d	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑚 ) / 𝑘 ) ) = ( ( log ‘ 𝑚 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) )
133	123 132	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = ( ( log ‘ 𝑚 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) )
134	133	sumeq2dv	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( log ‘ 𝑚 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) )
135		iftrue	⊢ ( 𝑆 = 0 → if ( 𝑆 = 0 , 0 , 𝑇 ) = 0 )
136	135	oveq2d	⊢ ( 𝑆 = 0 → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) = ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − 0 ) )
137	34	subid1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − 0 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) )
138	136 137	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) )
139		ovex	⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ∈ V
140	58 9 139	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) )
141	30 140	syl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) )
142	61	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝐹 : ℕ ⟶ ℂ )
143	142 19 62	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
144	141 143	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ∈ ℂ )
145	17 127 144	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( ( log ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( log ‘ 𝑚 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) )
146	145	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( ( log ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( log ‘ 𝑚 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) )
147	134 138 146	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) = ( ( log ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) )
148	87 147	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) = ( ( log ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) )
149	87 141	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) )
150	77 49	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( ⌊ ‘ 𝑚 ) ∈ ( ℤ≥ ‘ 1 ) )
151	81 19 55	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ∈ ℂ )
152	149 150 151	fsumser	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
153	152	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
154	153	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( ( log ‘ 𝑚 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) / 𝑘 ) ) = ( ( log ‘ 𝑚 ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) )
155	148 154	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) = ( ( log ‘ 𝑚 ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) )
156	155	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( abs ‘ ( ( log ‘ 𝑚 ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
157	125	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( log ‘ 𝑚 ) ∈ ℝ )
158	157	recnd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( log ‘ 𝑚 ) ∈ ℂ )
159	87 158	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( log ‘ 𝑚 ) ∈ ℂ )
160	159 79	absmuld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( abs ‘ ( ( log ‘ 𝑚 ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) = ( ( abs ‘ ( log ‘ 𝑚 ) ) · ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
161	95 96	absidd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( log ‘ 𝑚 ) ) = ( log ‘ 𝑚 ) )
162	161	oveq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( ( abs ‘ ( log ‘ 𝑚 ) ) · ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) = ( ( log ‘ 𝑚 ) · ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
163	162	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( ( abs ‘ ( log ‘ 𝑚 ) ) · ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) = ( ( log ‘ 𝑚 ) · ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
164	156 160 163	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( ( log ‘ 𝑚 ) · ( abs ‘ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
165		iftrue	⊢ ( 𝑆 = 0 → if ( 𝑆 = 0 , 𝐶 , 𝐸 ) = 𝐶 )
166	165	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → if ( 𝑆 = 0 , 𝐶 , 𝐸 ) = 𝐶 )
167	166	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( if ( 𝑆 = 0 , 𝐶 , 𝐸 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
168	90	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
169	168	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → 𝐶 ∈ ℂ )
170		rpcnne0	⊢ ( 𝑚 ∈ ℝ+ → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
171	170	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
172		div12	⊢ ( ( 𝐶 ∈ ℂ ∧ ( log ‘ 𝑚 ) ∈ ℂ ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( ( log ‘ 𝑚 ) · ( 𝐶 / 𝑚 ) ) )
173	169 158 171 172	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( ( log ‘ 𝑚 ) · ( 𝐶 / 𝑚 ) ) )
174	167 173	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑆 = 0 ) → ( if ( 𝑆 = 0 , 𝐶 , 𝐸 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( ( log ‘ 𝑚 ) · ( 𝐶 / 𝑚 ) ) )
175	87 174	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( if ( 𝑆 = 0 , 𝐶 , 𝐸 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( ( log ‘ 𝑚 ) · ( 𝐶 / 𝑚 ) ) )
176	118 164 175	3brtr4d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 = 0 ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( if ( 𝑆 = 0 , 𝐶 , 𝐸 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
177		2fveq3	⊢ ( 𝑦 = 𝑚 → ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
178	177	fvoveq1d	⊢ ( 𝑦 = 𝑚 → ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑇 ) ) )
179		fveq2	⊢ ( 𝑦 = 𝑚 → ( log ‘ 𝑦 ) = ( log ‘ 𝑚 ) )
180		id	⊢ ( 𝑦 = 𝑚 → 𝑦 = 𝑚 )
181	179 180	oveq12d	⊢ ( 𝑦 = 𝑚 → ( ( log ‘ 𝑦 ) / 𝑦 ) = ( ( log ‘ 𝑚 ) / 𝑚 ) )
182	181	oveq2d	⊢ ( 𝑦 = 𝑚 → ( 𝐸 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) = ( 𝐸 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
183	178 182	breq12d	⊢ ( 𝑦 = 𝑚 → ( ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )
184	183	rspccva	⊢ ( ( ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
185	16 184	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
186	185	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑇 ) ) ≤ ( 𝐸 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
187		fveq2	⊢ ( 𝑎 = 𝑘 → ( log ‘ 𝑎 ) = ( log ‘ 𝑘 ) )
188	187 57	oveq12d	⊢ ( 𝑎 = 𝑘 → ( ( log ‘ 𝑎 ) / 𝑎 ) = ( ( log ‘ 𝑘 ) / 𝑘 ) )
189	56 188	oveq12d	⊢ ( 𝑎 = 𝑘 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) )
190		ovex	⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) ∈ V
191	189 13 190	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( 𝐾 ‘ 𝑘 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) )
192	19 191	syl	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) → ( 𝐾 ‘ 𝑘 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) )
193		ifnefalse	⊢ ( 𝑆 ≠ 0 → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) = 𝑘 )
194	193	fveq2d	⊢ ( 𝑆 ≠ 0 → ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) = ( log ‘ 𝑘 ) )
195	194	oveq1d	⊢ ( 𝑆 ≠ 0 → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) = ( ( log ‘ 𝑘 ) / 𝑘 ) )
196	195	oveq2d	⊢ ( 𝑆 ≠ 0 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) )
197	196	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) )
198	197	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) )
199	192 198	sylan9eqr	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( 𝐾 ‘ 𝑘 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) )
200	150	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → ( ⌊ ‘ 𝑚 ) ∈ ( ℤ≥ ‘ 1 ) )
201		nnrp	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
202	201	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ+ )
203	202	relogcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑘 ) ∈ ℝ )
204	203	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑘 ) ∈ ℂ )
205	204 52 54	divcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑘 ) / 𝑘 ) ∈ ℂ )
206	23 205	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) ∈ ℂ )
207	189	cbvmptv	⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) )
208	13 207	eqtri	⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ 𝑘 ) / 𝑘 ) ) )
209	206 208	fmptd	⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ℂ )
210	209	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → 𝐾 : ℕ ⟶ ℂ )
211		ffvelcdm	⊢ ( ( 𝐾 : ℕ ⟶ ℂ ∧ 𝑘 ∈ ℕ ) → ( 𝐾 ‘ 𝑘 ) ∈ ℂ )
212	210 19 211	syl2an	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( 𝐾 ‘ 𝑘 ) ∈ ℂ )
213	199 212	eqeltrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ∈ ℂ )
214	199 200 213	fsumser	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
215		ifnefalse	⊢ ( 𝑆 ≠ 0 → if ( 𝑆 = 0 , 0 , 𝑇 ) = 𝑇 )
216	215	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → if ( 𝑆 = 0 , 0 , 𝑇 ) = 𝑇 )
217	214 216	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) = ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑇 ) )
218	217	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑇 ) ) )
219		ifnefalse	⊢ ( 𝑆 ≠ 0 → if ( 𝑆 = 0 , 𝐶 , 𝐸 ) = 𝐸 )
220	219	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → if ( 𝑆 = 0 , 𝐶 , 𝐸 ) = 𝐸 )
221	220	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → ( if ( 𝑆 = 0 , 𝐶 , 𝐸 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( 𝐸 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
222	186 218 221	3brtr4d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) ∧ 𝑆 ≠ 0 ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( if ( 𝑆 = 0 , 𝐶 , 𝐸 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
223	176 222	pm2.61dane	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( if ( 𝑆 = 0 , 𝐶 , 𝐸 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
224		fzfid	⊢ ( 𝜑 → ( 1 ... 2 ) ∈ Fin )
225	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑋 ∈ 𝐷 )
226		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... 2 ) → 𝑘 ∈ ℤ )
227	226	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑘 ∈ ℤ )
228	4 1 5 2 225 227	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ )
229	228	abscld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) ∈ ℝ )
230		3rp	⊢ 3 ∈ ℝ+
231		relogcl	⊢ ( 3 ∈ ℝ+ → ( log ‘ 3 ) ∈ ℝ )
232	230 231	ax-mp	⊢ ( log ‘ 3 ) ∈ ℝ
233		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 2 ) → 𝑘 ∈ ℕ )
234	233	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑘 ∈ ℕ )
235		nndivre	⊢ ( ( ( log ‘ 3 ) ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 3 ) / 𝑘 ) ∈ ℝ )
236	232 234 235	sylancr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( log ‘ 3 ) / 𝑘 ) ∈ ℝ )
237	229 236	remulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) ∈ ℝ )
238	224 237	fsumrecl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) ∈ ℝ )
239	48	abscld	⊢ ( 𝜑 → ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ∈ ℝ )
240	238 239	readdcld	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ∈ ℝ )
241		simpl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 𝜑 )
242	66	rexri	⊢ 3 ∈ ℝ*
243		elico2	⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℝ* ) → ( 𝑚 ∈ ( 1 [,) 3 ) ↔ ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3 ) ) )
244	110 242 243	mp2an	⊢ ( 𝑚 ∈ ( 1 [,) 3 ) ↔ ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3 ) )
245	244	simp1bi	⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 𝑚 ∈ ℝ )
246	245	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 𝑚 ∈ ℝ )
247		0red	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 0 ∈ ℝ )
248		1red	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 1 ∈ ℝ )
249		0lt1	⊢ 0 < 1
250	249	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 0 < 1 )
251	244	simp2bi	⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 1 ≤ 𝑚 )
252	251	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 1 ≤ 𝑚 )
253	247 248 246 250 252	ltletrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 0 < 𝑚 )
254	246 253	elrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 𝑚 ∈ ℝ+ )
255	241 254	jca	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) )
256	48	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ ℂ )
257	34 256	subcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ∈ ℂ )
258	255 257	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ∈ ℂ )
259	258	abscld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ∈ ℝ )
260	255 34	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ∈ ℂ )
261	260	abscld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
262	239	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ∈ ℝ )
263	261 262	readdcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ∈ ℝ )
264	238	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) ∈ ℝ )
265	264 262	readdcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ∈ ℝ )
266	34 256	abs2dif2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
267	255 266	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
268	33	abscld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
269	17 268	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
270	255 269	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
271	17 33	fsumabs	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) )
272	255 271	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) )
273		fzfid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( 1 ... 2 ) ∈ Fin )
274	228	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ )
275	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑚 ∈ ℝ+ )
276	233	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑘 ∈ ℕ )
277	276	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑘 ∈ ℝ+ )
278	275 277	ifcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ∈ ℝ+ )
279	278	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ∈ ℝ )
280	279 276	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ∈ ℝ )
281	280	recnd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ∈ ℂ )
282	274 281	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ∈ ℂ )
283	282	abscld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
284	273 283	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... 2 ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
285	255 284	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → Σ 𝑘 ∈ ( 1 ... 2 ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
286		fzfid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( 1 ... 2 ) ∈ Fin )
287	255 282	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ∈ ℂ )
288	287	abscld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
289	287	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 0 ≤ ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) )
290	246	flcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( ⌊ ‘ 𝑚 ) ∈ ℤ )
291		2z	⊢ 2 ∈ ℤ
292	291	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 2 ∈ ℤ )
293	244	simp3bi	⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 𝑚 < 3 )
294	293	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 𝑚 < 3 )
295		3z	⊢ 3 ∈ ℤ
296		fllt	⊢ ( ( 𝑚 ∈ ℝ ∧ 3 ∈ ℤ ) → ( 𝑚 < 3 ↔ ( ⌊ ‘ 𝑚 ) < 3 ) )
297	246 295 296	sylancl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( 𝑚 < 3 ↔ ( ⌊ ‘ 𝑚 ) < 3 ) )
298	294 297	mpbid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( ⌊ ‘ 𝑚 ) < 3 )
299		df-3	⊢ 3 = ( 2 + 1 )
300	298 299	breqtrdi	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( ⌊ ‘ 𝑚 ) < ( 2 + 1 ) )
301		rpre	⊢ ( 𝑚 ∈ ℝ+ → 𝑚 ∈ ℝ )
302	301	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝑚 ∈ ℝ )
303	302	flcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( ⌊ ‘ 𝑚 ) ∈ ℤ )
304		zleltp1	⊢ ( ( ( ⌊ ‘ 𝑚 ) ∈ ℤ ∧ 2 ∈ ℤ ) → ( ( ⌊ ‘ 𝑚 ) ≤ 2 ↔ ( ⌊ ‘ 𝑚 ) < ( 2 + 1 ) ) )
305	303 291 304	sylancl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑚 ) ≤ 2 ↔ ( ⌊ ‘ 𝑚 ) < ( 2 + 1 ) ) )
306	255 305	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( ( ⌊ ‘ 𝑚 ) ≤ 2 ↔ ( ⌊ ‘ 𝑚 ) < ( 2 + 1 ) ) )
307	300 306	mpbird	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( ⌊ ‘ 𝑚 ) ≤ 2 )
308		eluz2	⊢ ( 2 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ↔ ( ( ⌊ ‘ 𝑚 ) ∈ ℤ ∧ 2 ∈ ℤ ∧ ( ⌊ ‘ 𝑚 ) ≤ 2 ) )
309	290 292 307 308	syl3anbrc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 2 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) )
310		fzss2	⊢ ( 2 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) → ( 1 ... ( ⌊ ‘ 𝑚 ) ) ⊆ ( 1 ... 2 ) )
311	309 310	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( 1 ... ( ⌊ ‘ 𝑚 ) ) ⊆ ( 1 ... 2 ) )
312	286 288 289 311	fsumless	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... 2 ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) )
313	237	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) ∈ ℝ )
314	274 281	absmuld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) )
315	255 314	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) )
316	255 280	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ∈ ℝ )
317	255 279	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ∈ ℝ )
318		log1	⊢ ( log ‘ 1 ) = 0
319		elfzle1	⊢ ( 𝑘 ∈ ( 1 ... 2 ) → 1 ≤ 𝑘 )
320		breq2	⊢ ( 𝑚 = if ( 𝑆 = 0 , 𝑚 , 𝑘 ) → ( 1 ≤ 𝑚 ↔ 1 ≤ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) )
321		breq2	⊢ ( 𝑘 = if ( 𝑆 = 0 , 𝑚 , 𝑘 ) → ( 1 ≤ 𝑘 ↔ 1 ≤ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) )
322	320 321	ifboth	⊢ ( ( 1 ≤ 𝑚 ∧ 1 ≤ 𝑘 ) → 1 ≤ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) )
323	252 319 322	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 1 ≤ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) )
324		1rp	⊢ 1 ∈ ℝ+
325		logleb	⊢ ( ( 1 ∈ ℝ+ ∧ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ∈ ℝ+ ) → ( 1 ≤ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ) )
326	324 278 325	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( 1 ≤ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ) )
327	255 326	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( 1 ≤ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ) )
328	323 327	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( log ‘ 1 ) ≤ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) )
329	318 328	eqbrtrrid	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 0 ≤ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) )
330	277	rpregt0d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
331	255 330	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
332		divge0	⊢ ( ( ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ∈ ℝ ∧ 0 ≤ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → 0 ≤ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) )
333	317 329 331 332	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 0 ≤ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) )
334	316 333	absidd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) = ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) )
335	334 316	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ∈ ℝ )
336	236	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( log ‘ 3 ) / 𝑘 ) ∈ ℝ )
337	229	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) ∈ ℝ )
338	274	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) )
339	337 338	jca	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) ) )
340	255 339	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) ) )
341	293	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑚 < 3 )
342	276	nnred	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑘 ∈ ℝ )
343		2re	⊢ 2 ∈ ℝ
344	343	a1i	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 2 ∈ ℝ )
345	66	a1i	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 3 ∈ ℝ )
346		elfzle2	⊢ ( 𝑘 ∈ ( 1 ... 2 ) → 𝑘 ≤ 2 )
347	346	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑘 ≤ 2 )
348		2lt3	⊢ 2 < 3
349	348	a1i	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 2 < 3 )
350	342 344 345 347 349	lelttrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑘 < 3 )
351	255 350	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → 𝑘 < 3 )
352		breq1	⊢ ( 𝑚 = if ( 𝑆 = 0 , 𝑚 , 𝑘 ) → ( 𝑚 < 3 ↔ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) < 3 ) )
353		breq1	⊢ ( 𝑘 = if ( 𝑆 = 0 , 𝑚 , 𝑘 ) → ( 𝑘 < 3 ↔ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) < 3 ) )
354	352 353	ifboth	⊢ ( ( 𝑚 < 3 ∧ 𝑘 < 3 ) → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) < 3 )
355	341 351 354	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) < 3 )
356	278	rpred	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ∈ ℝ )
357		ltle	⊢ ( ( if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ∈ ℝ ∧ 3 ∈ ℝ ) → ( if ( 𝑆 = 0 , 𝑚 , 𝑘 ) < 3 → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ≤ 3 ) )
358	356 66 357	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( if ( 𝑆 = 0 , 𝑚 , 𝑘 ) < 3 → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ≤ 3 ) )
359	255 358	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( if ( 𝑆 = 0 , 𝑚 , 𝑘 ) < 3 → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ≤ 3 ) )
360	355 359	mpd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ≤ 3 )
361		logleb	⊢ ( ( if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ≤ 3 ↔ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ≤ ( log ‘ 3 ) ) )
362	278 230 361	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ≤ 3 ↔ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ≤ ( log ‘ 3 ) ) )
363	255 362	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ≤ 3 ↔ ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ≤ ( log ‘ 3 ) ) )
364	360 363	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ≤ ( log ‘ 3 ) )
365	232	a1i	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( log ‘ 3 ) ∈ ℝ )
366	279 365 277	lediv1d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ≤ ( log ‘ 3 ) ↔ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ≤ ( ( log ‘ 3 ) / 𝑘 ) ) )
367	255 366	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) ≤ ( log ‘ 3 ) ↔ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ≤ ( ( log ‘ 3 ) / 𝑘 ) ) )
368	364 367	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ≤ ( ( log ‘ 3 ) / 𝑘 ) )
369	334 368	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ≤ ( ( log ‘ 3 ) / 𝑘 ) )
370		lemul2a	⊢ ( ( ( ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ∈ ℝ ∧ ( ( log ‘ 3 ) / 𝑘 ) ∈ ℝ ∧ ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) ) ) ∧ ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ≤ ( ( log ‘ 3 ) / 𝑘 ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) )
371	335 336 340 369 370	syl31anc	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( abs ‘ ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) )
372	315 371	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) ∧ 𝑘 ∈ ( 1 ... 2 ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) )
373	286 288 313 372	fsumle	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → Σ 𝑘 ∈ ( 1 ... 2 ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) )
374	270 285 264 312 373	letrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) )
375	261 270 264 272 374	letrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) )
376	34	abscld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ∈ ℝ )
377	238	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) ∈ ℝ )
378	256	abscld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ∈ ℝ )
379	376 377 378	leadd1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) ↔ ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ) )
380	255 379	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) ↔ ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ) )
381	375 380	mpbid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
382	259 263 265 267 381	letrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
383	382	ralrimiva	⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 1 [,) 3 ) ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , 𝑚 , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ≤ ( Σ 𝑘 ∈ ( 1 ... 2 ) ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) · ( ( log ‘ 3 ) / 𝑘 ) ) + ( abs ‘ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
384	1 2 3 4 5 6 7 8 34 42 43 48 223 240 383	dchrvmasumlem3	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) · ( ( log ‘ if ( 𝑆 = 0 , ( 𝑥 / 𝑑 ) , 𝑘 ) ) / 𝑘 ) ) − if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ) ∈ 𝑂(1) )