This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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