MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrvmasumiflem1 Structured version   Visualization version   GIF version

Theorem dchrvmasumiflem1 26849
Description: Lemma for dchrvmasumif 26851. (Contributed by Mario Carneiro, 5-May-2016.)
Hypotheses
Ref Expression
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 (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)
dchrvmasumif.1 (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))
dchrvmasumif.g 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) · ((log‘𝑎) / 𝑎)))
dchrvmasumif.e (𝜑𝐸 ∈ (0[,)+∞))
dchrvmasumif.t (𝜑 → seq1( + , 𝐾) ⇝ 𝑇)
dchrvmasumif.2 (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)))
Assertion
Ref Expression
dchrvmasumiflem1 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · (Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1))
Distinct variable groups:   𝑥,𝑘,𝑦, 1   𝑥,𝑑,𝑦,𝐶   𝑘,𝑑,𝐹,𝑥,𝑦   𝑎,𝑑,𝑘,𝑥,𝑦   𝐸,𝑑,𝑥,𝑦   𝑘,𝐾,𝑦   𝑘,𝑁,𝑥,𝑦   𝜑,𝑑,𝑘,𝑥   𝑇,𝑑,𝑥,𝑦   𝑆,𝑑,𝑘,𝑥,𝑦   𝑘,𝑍,𝑥,𝑦   𝐷,𝑘,𝑥,𝑦   𝐿,𝑎,𝑑,𝑘,𝑥,𝑦   𝑋,𝑎,𝑑,𝑘,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑦,𝑎)   𝐶(𝑘,𝑎)   𝐷(𝑎,𝑑)   𝑆(𝑎)   𝑇(𝑘,𝑎)   1 (𝑎,𝑑)   𝐸(𝑘,𝑎)   𝐹(𝑎)   𝐺(𝑥,𝑦,𝑘,𝑎,𝑑)   𝐾(𝑥,𝑎,𝑑)   𝑁(𝑎,𝑑)   𝑍(𝑎,𝑑)

Proof of Theorem dchrvmasumiflem1
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 rpvmasum.z . 2 𝑍 = (ℤ/nℤ‘𝑁)
2 rpvmasum.l . 2 𝐿 = (ℤRHom‘𝑍)
3 rpvmasum.a . 2 (𝜑𝑁 ∈ ℕ)
4 rpvmasum.g . 2 𝐺 = (DChr‘𝑁)
5 rpvmasum.d . 2 𝐷 = (Base‘𝐺)
6 rpvmasum.1 . 2 1 = (0g𝐺)
7 dchrisum.b . 2 (𝜑𝑋𝐷)
8 dchrisum.n1 . 2 (𝜑𝑋1 )
9 fzfid 13878 . . 3 ((𝜑𝑚 ∈ ℝ+) → (1...(⌊‘𝑚)) ∈ Fin)
10 simpl 483 . . . . 5 ((𝜑𝑚 ∈ ℝ+) → 𝜑)
11 elfznn 13470 . . . . 5 (𝑘 ∈ (1...(⌊‘𝑚)) → 𝑘 ∈ ℕ)
127adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑋𝐷)
13 nnz 12520 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
1413adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
154, 1, 5, 2, 12, 14dchrzrhcl 26593 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
1610, 11, 15syl2an 596 . . . 4 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
17 simpr 485 . . . . . . . 8 ((𝜑𝑚 ∈ ℝ+) → 𝑚 ∈ ℝ+)
1811nnrpd 12955 . . . . . . . 8 (𝑘 ∈ (1...(⌊‘𝑚)) → 𝑘 ∈ ℝ+)
19 ifcl 4531 . . . . . . . 8 ((𝑚 ∈ ℝ+𝑘 ∈ ℝ+) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+)
2017, 18, 19syl2an 596 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+)
2120relogcld 25978 . . . . . 6 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ)
2211adantl 482 . . . . . 6 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℕ)
2321, 22nndivred 12207 . . . . 5 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ)
2423recnd 11183 . . . 4 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℂ)
2516, 24mulcld 11175 . . 3 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
269, 25fsumcl 15618 . 2 ((𝜑𝑚 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
27 fveq2 6842 . . . 4 (𝑚 = (𝑥 / 𝑑) → (⌊‘𝑚) = (⌊‘(𝑥 / 𝑑)))
2827oveq2d 7373 . . 3 (𝑚 = (𝑥 / 𝑑) → (1...(⌊‘𝑚)) = (1...(⌊‘(𝑥 / 𝑑))))
29 ifeq1 4490 . . . . . . 7 (𝑚 = (𝑥 / 𝑑) → if(𝑆 = 0, 𝑚, 𝑘) = if(𝑆 = 0, (𝑥 / 𝑑), 𝑘))
3029fveq2d 6846 . . . . . 6 (𝑚 = (𝑥 / 𝑑) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)))
3130oveq1d 7372 . . . . 5 (𝑚 = (𝑥 / 𝑑) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘))
3231oveq2d 7373 . . . 4 (𝑚 = (𝑥 / 𝑑) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)))
3332adantr 481 . . 3 ((𝑚 = (𝑥 / 𝑑) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)))
3428, 33sumeq12rdv 15592 . 2 (𝑚 = (𝑥 / 𝑑) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)))
35 dchrvmasumif.c . . 3 (𝜑𝐶 ∈ (0[,)+∞))
36 dchrvmasumif.e . . 3 (𝜑𝐸 ∈ (0[,)+∞))
3735, 36ifcld 4532 . 2 (𝜑 → if(𝑆 = 0, 𝐶, 𝐸) ∈ (0[,)+∞))
38 0cn 11147 . . 3 0 ∈ ℂ
39 dchrvmasumif.t . . . 4 (𝜑 → seq1( + , 𝐾) ⇝ 𝑇)
40 climcl 15381 . . . 4 (seq1( + , 𝐾) ⇝ 𝑇𝑇 ∈ ℂ)
4139, 40syl 17 . . 3 (𝜑𝑇 ∈ ℂ)
42 ifcl 4531 . . 3 ((0 ∈ ℂ ∧ 𝑇 ∈ ℂ) → if(𝑆 = 0, 0, 𝑇) ∈ ℂ)
4338, 41, 42sylancr 587 . 2 (𝜑 → if(𝑆 = 0, 0, 𝑇) ∈ ℂ)
44 nnuz 12806 . . . . . . . . 9 ℕ = (ℤ‘1)
45 1zzd 12534 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
46 nncn 12161 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
4746adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
48 nnne0 12187 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
4948adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ≠ 0)
5015, 47, 49divcld 11931 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑋‘(𝐿𝑘)) / 𝑘) ∈ ℂ)
51 dchrvmasumif.f . . . . . . . . . . . 12 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))
52 2fveq3 6847 . . . . . . . . . . . . . 14 (𝑎 = 𝑘 → (𝑋‘(𝐿𝑎)) = (𝑋‘(𝐿𝑘)))
53 id 22 . . . . . . . . . . . . . 14 (𝑎 = 𝑘𝑎 = 𝑘)
5452, 53oveq12d 7375 . . . . . . . . . . . . 13 (𝑎 = 𝑘 → ((𝑋‘(𝐿𝑎)) / 𝑎) = ((𝑋‘(𝐿𝑘)) / 𝑘))
5554cbvmptv 5218 . . . . . . . . . . . 12 (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)) = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿𝑘)) / 𝑘))
5651, 55eqtri 2764 . . . . . . . . . . 11 𝐹 = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿𝑘)) / 𝑘))
5750, 56fmptd 7062 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶ℂ)
58 ffvelcdm 7032 . . . . . . . . . 10 ((𝐹:ℕ⟶ℂ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
5957, 58sylan 580 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
6044, 45, 59serf 13936 . . . . . . . 8 (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
6160ad2antrr 724 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → seq1( + , 𝐹):ℕ⟶ℂ)
62 3re 12233 . . . . . . . . . . 11 3 ∈ ℝ
63 elicopnf 13362 . . . . . . . . . . 11 (3 ∈ ℝ → (𝑚 ∈ (3[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 3 ≤ 𝑚)))
6462, 63mp1i 13 . . . . . . . . . 10 (𝜑 → (𝑚 ∈ (3[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 3 ≤ 𝑚)))
6564simprbda 499 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → 𝑚 ∈ ℝ)
66 1red 11156 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 1 ∈ ℝ)
6762a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 3 ∈ ℝ)
68 1le3 12365 . . . . . . . . . . 11 1 ≤ 3
6968a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 1 ≤ 3)
7064simplbda 500 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 3 ≤ 𝑚)
7166, 67, 65, 69, 70letrd 11312 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → 1 ≤ 𝑚)
72 flge1nn 13726 . . . . . . . . 9 ((𝑚 ∈ ℝ ∧ 1 ≤ 𝑚) → (⌊‘𝑚) ∈ ℕ)
7365, 71, 72syl2anc 584 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → (⌊‘𝑚) ∈ ℕ)
7473adantr 481 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (⌊‘𝑚) ∈ ℕ)
7561, 74ffvelcdmd 7036 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
7675abscld 15321 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ∈ ℝ)
77 simpl 483 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → 𝜑)
78 0red 11158 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 0 ∈ ℝ)
79 3pos 12258 . . . . . . . . . . 11 0 < 3
8079a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 0 < 3)
8178, 67, 65, 80, 70ltletrd 11315 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → 0 < 𝑚)
8265, 81elrpd 12954 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → 𝑚 ∈ ℝ+)
8377, 82jca 512 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → (𝜑𝑚 ∈ ℝ+))
84 elrege0 13371 . . . . . . . . . 10 (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
8584simplbi 498 . . . . . . . . 9 (𝐶 ∈ (0[,)+∞) → 𝐶 ∈ ℝ)
8635, 85syl 17 . . . . . . . 8 (𝜑𝐶 ∈ ℝ)
87 rerpdivcl 12945 . . . . . . . 8 ((𝐶 ∈ ℝ ∧ 𝑚 ∈ ℝ+) → (𝐶 / 𝑚) ∈ ℝ)
8886, 87sylan 580 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → (𝐶 / 𝑚) ∈ ℝ)
8983, 88syl 17 . . . . . 6 ((𝜑𝑚 ∈ (3[,)+∞)) → (𝐶 / 𝑚) ∈ ℝ)
9089adantr 481 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (𝐶 / 𝑚) ∈ ℝ)
9182relogcld 25978 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → (log‘𝑚) ∈ ℝ)
9265, 71logge0d 25985 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → 0 ≤ (log‘𝑚))
9391, 92jca 512 . . . . . 6 ((𝜑𝑚 ∈ (3[,)+∞)) → ((log‘𝑚) ∈ ℝ ∧ 0 ≤ (log‘𝑚)))
9493adantr 481 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) ∈ ℝ ∧ 0 ≤ (log‘𝑚)))
95 oveq2 7365 . . . . . . . 8 (𝑆 = 0 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 0))
9660adantr 481 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → seq1( + , 𝐹):ℕ⟶ℂ)
9796, 73ffvelcdmd 7036 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
9897subid1d 11501 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 0) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
9995, 98sylan9eqr 2798 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
10099fveq2d 6846 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) = (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))))
101 2fveq3 6847 . . . . . . . . . 10 (𝑦 = 𝑚 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
102101fvoveq1d 7379 . . . . . . . . 9 (𝑦 = 𝑚 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)))
103 oveq2 7365 . . . . . . . . 9 (𝑦 = 𝑚 → (𝐶 / 𝑦) = (𝐶 / 𝑚))
104102, 103breq12d 5118 . . . . . . . 8 (𝑦 = 𝑚 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚)))
105 dchrvmasumif.1 . . . . . . . . 9 (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))
106105adantr 481 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))
107 1re 11155 . . . . . . . . . 10 1 ∈ ℝ
108 elicopnf 13362 . . . . . . . . . 10 (1 ∈ ℝ → (𝑚 ∈ (1[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚)))
109107, 108ax-mp 5 . . . . . . . . 9 (𝑚 ∈ (1[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚))
11065, 71, 109sylanbrc 583 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → 𝑚 ∈ (1[,)+∞))
111104, 106, 110rspcdva 3582 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚))
112111adantr 481 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚))
113100, 112eqbrtrrd 5129 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ≤ (𝐶 / 𝑚))
114 lemul2a 12010 . . . . 5 ((((abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ∈ ℝ ∧ (𝐶 / 𝑚) ∈ ℝ ∧ ((log‘𝑚) ∈ ℝ ∧ 0 ≤ (log‘𝑚))) ∧ (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ≤ (𝐶 / 𝑚)) → ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((log‘𝑚) · (𝐶 / 𝑚)))
11576, 90, 94, 113, 114syl31anc 1373 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((log‘𝑚) · (𝐶 / 𝑚)))
116 iftrue 4492 . . . . . . . . . . . . . . 15 (𝑆 = 0 → if(𝑆 = 0, 𝑚, 𝑘) = 𝑚)
117116fveq2d 6846 . . . . . . . . . . . . . 14 (𝑆 = 0 → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘𝑚))
118117oveq1d 7372 . . . . . . . . . . . . 13 (𝑆 = 0 → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑚) / 𝑘))
119118ad2antlr 725 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑚) / 𝑘))
120119oveq2d 7373 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑚) / 𝑘)))
12116adantlr 713 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
122 relogcl 25931 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℝ+ → (log‘𝑚) ∈ ℝ)
123122adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ+) → (log‘𝑚) ∈ ℝ)
124123recnd 11183 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → (log‘𝑚) ∈ ℂ)
125124ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (log‘𝑚) ∈ ℂ)
12611adantl 482 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℕ)
127126nncnd 12169 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℂ)
128126nnne0d 12203 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ≠ 0)
129121, 125, 127, 128div12d 11967 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘𝑚) / 𝑘)) = ((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
130120, 129eqtrd 2776 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
131130sumeq2dv 15588 . . . . . . . . 9 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
132 iftrue 4492 . . . . . . . . . . 11 (𝑆 = 0 → if(𝑆 = 0, 0, 𝑇) = 0)
133132oveq2d 7373 . . . . . . . . . 10 (𝑆 = 0 → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − 0))
13426subid1d 11501 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℝ+) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − 0) = Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))
135133, 134sylan9eqr 2798 . . . . . . . . 9 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))
136 ovex 7390 . . . . . . . . . . . . . 14 ((𝑋‘(𝐿𝑘)) / 𝑘) ∈ V
13754, 51, 136fvmpt 6948 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝐹𝑘) = ((𝑋‘(𝐿𝑘)) / 𝑘))
13822, 137syl 17 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐹𝑘) = ((𝑋‘(𝐿𝑘)) / 𝑘))
13957adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → 𝐹:ℕ⟶ℂ)
140139, 11, 58syl2an 596 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐹𝑘) ∈ ℂ)
141138, 140eqeltrrd 2839 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) / 𝑘) ∈ ℂ)
1429, 124, 141fsummulc2 15669 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℝ+) → ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
143142adantr 481 . . . . . . . . 9 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
144131, 135, 1433eqtr4d 2786 . . . . . . . 8 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)))
14583, 144sylan 580 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)))
14683, 138sylan 580 . . . . . . . . . 10 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐹𝑘) = ((𝑋‘(𝐿𝑘)) / 𝑘))
14773, 44eleqtrdi 2848 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → (⌊‘𝑚) ∈ (ℤ‘1))
14877, 11, 50syl2an 596 . . . . . . . . . 10 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) / 𝑘) ∈ ℂ)
149146, 147, 148fsumser 15615 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
150149adantr 481 . . . . . . . 8 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
151150oveq2d 7373 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)) = ((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚))))
152145, 151eqtrd 2776 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚))))
153152fveq2d 6846 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = (abs‘((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚)))))
154122ad2antlr 725 . . . . . . . 8 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (log‘𝑚) ∈ ℝ)
155154recnd 11183 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (log‘𝑚) ∈ ℂ)
15683, 155sylan 580 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (log‘𝑚) ∈ ℂ)
157156, 75absmuld 15339 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((abs‘(log‘𝑚)) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))))
15891, 92absidd 15307 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → (abs‘(log‘𝑚)) = (log‘𝑚))
159158oveq1d 7372 . . . . . 6 ((𝜑𝑚 ∈ (3[,)+∞)) → ((abs‘(log‘𝑚)) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))))
160159adantr 481 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((abs‘(log‘𝑚)) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))))
161153, 157, 1603eqtrd 2780 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))))
162 iftrue 4492 . . . . . . . 8 (𝑆 = 0 → if(𝑆 = 0, 𝐶, 𝐸) = 𝐶)
163162adantl 482 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → if(𝑆 = 0, 𝐶, 𝐸) = 𝐶)
164163oveq1d 7372 . . . . . 6 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘𝑚) / 𝑚)))
16586recnd 11183 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
166165ad2antrr 724 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → 𝐶 ∈ ℂ)
167 rpcnne0 12933 . . . . . . . 8 (𝑚 ∈ ℝ+ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
168167ad2antlr 725 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
169 div12 11835 . . . . . . 7 ((𝐶 ∈ ℂ ∧ (log‘𝑚) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → (𝐶 · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚)))
170166, 155, 168, 169syl3anc 1371 . . . . . 6 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (𝐶 · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚)))
171164, 170eqtrd 2776 . . . . 5 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚)))
17283, 171sylan 580 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚)))
173115, 161, 1723brtr4d 5137 . . 3 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)))
174 dchrvmasumif.2 . . . . . 6 (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)))
175 2fveq3 6847 . . . . . . . . 9 (𝑦 = 𝑚 → (seq1( + , 𝐾)‘(⌊‘𝑦)) = (seq1( + , 𝐾)‘(⌊‘𝑚)))
176175fvoveq1d 7379 . . . . . . . 8 (𝑦 = 𝑚 → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)))
177 fveq2 6842 . . . . . . . . . 10 (𝑦 = 𝑚 → (log‘𝑦) = (log‘𝑚))
178 id 22 . . . . . . . . . 10 (𝑦 = 𝑚𝑦 = 𝑚)
179177, 178oveq12d 7375 . . . . . . . . 9 (𝑦 = 𝑚 → ((log‘𝑦) / 𝑦) = ((log‘𝑚) / 𝑚))
180179oveq2d 7373 . . . . . . . 8 (𝑦 = 𝑚 → (𝐸 · ((log‘𝑦) / 𝑦)) = (𝐸 · ((log‘𝑚) / 𝑚)))
181176, 180breq12d 5118 . . . . . . 7 (𝑦 = 𝑚 → ((abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)) ↔ (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚))))
182181rspccva 3580 . . . . . 6 ((∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)) ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚)))
183174, 182sylan 580 . . . . 5 ((𝜑𝑚 ∈ (3[,)+∞)) → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚)))
184183adantr 481 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚)))
185 fveq2 6842 . . . . . . . . . . . 12 (𝑎 = 𝑘 → (log‘𝑎) = (log‘𝑘))
186185, 53oveq12d 7375 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((log‘𝑎) / 𝑎) = ((log‘𝑘) / 𝑘))
18752, 186oveq12d 7375 . . . . . . . . . 10 (𝑎 = 𝑘 → ((𝑋‘(𝐿𝑎)) · ((log‘𝑎) / 𝑎)) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
188 dchrvmasumif.g . . . . . . . . . 10 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) · ((log‘𝑎) / 𝑎)))
189 ovex 7390 . . . . . . . . . 10 ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)) ∈ V
190187, 188, 189fvmpt 6948 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐾𝑘) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
19111, 190syl 17 . . . . . . . 8 (𝑘 ∈ (1...(⌊‘𝑚)) → (𝐾𝑘) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
192 ifnefalse 4498 . . . . . . . . . . . . 13 (𝑆 ≠ 0 → if(𝑆 = 0, 𝑚, 𝑘) = 𝑘)
193192fveq2d 6846 . . . . . . . . . . . 12 (𝑆 ≠ 0 → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘𝑘))
194193oveq1d 7372 . . . . . . . . . . 11 (𝑆 ≠ 0 → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑘) / 𝑘))
195194oveq2d 7373 . . . . . . . . . 10 (𝑆 ≠ 0 → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
196195adantl 482 . . . . . . . . 9 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
197196eqcomd 2742 . . . . . . . 8 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))
198191, 197sylan9eqr 2798 . . . . . . 7 ((((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐾𝑘) = ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))
199147adantr 481 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (⌊‘𝑚) ∈ (ℤ‘1))
200 nnrp 12926 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
201200adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
202201relogcld 25978 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (log‘𝑘) ∈ ℝ)
203202recnd 11183 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (log‘𝑘) ∈ ℂ)
204203, 47, 49divcld 11931 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((log‘𝑘) / 𝑘) ∈ ℂ)
20515, 204mulcld 11175 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)) ∈ ℂ)
206187cbvmptv 5218 . . . . . . . . . . . 12 (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) · ((log‘𝑎) / 𝑎))) = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
207188, 206eqtri 2764 . . . . . . . . . . 11 𝐾 = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
208205, 207fmptd 7062 . . . . . . . . . 10 (𝜑𝐾:ℕ⟶ℂ)
209208ad2antrr 724 . . . . . . . . 9 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → 𝐾:ℕ⟶ℂ)
210 ffvelcdm 7032 . . . . . . . . 9 ((𝐾:ℕ⟶ℂ ∧ 𝑘 ∈ ℕ) → (𝐾𝑘) ∈ ℂ)
211209, 11, 210syl2an 596 . . . . . . . 8 ((((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐾𝑘) ∈ ℂ)
212198, 211eqeltrrd 2839 . . . . . . 7 ((((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
213198, 199, 212fsumser 15615 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = (seq1( + , 𝐾)‘(⌊‘𝑚)))
214 ifnefalse 4498 . . . . . . 7 (𝑆 ≠ 0 → if(𝑆 = 0, 0, 𝑇) = 𝑇)
215214adantl 482 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → if(𝑆 = 0, 0, 𝑇) = 𝑇)
216213, 215oveq12d 7375 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇))
217216fveq2d 6846 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)))
218 ifnefalse 4498 . . . . . 6 (𝑆 ≠ 0 → if(𝑆 = 0, 𝐶, 𝐸) = 𝐸)
219218adantl 482 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → if(𝑆 = 0, 𝐶, 𝐸) = 𝐸)
220219oveq1d 7372 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = (𝐸 · ((log‘𝑚) / 𝑚)))
221184, 217, 2203brtr4d 5137 . . 3 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)))
222173, 221pm2.61dane 3032 . 2 ((𝜑𝑚 ∈ (3[,)+∞)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)))
223 fzfid 13878 . . . 4 (𝜑 → (1...2) ∈ Fin)
2247adantr 481 . . . . . . 7 ((𝜑𝑘 ∈ (1...2)) → 𝑋𝐷)
225 elfzelz 13441 . . . . . . . 8 (𝑘 ∈ (1...2) → 𝑘 ∈ ℤ)
226225adantl 482 . . . . . . 7 ((𝜑𝑘 ∈ (1...2)) → 𝑘 ∈ ℤ)
2274, 1, 5, 2, 224, 226dchrzrhcl 26593 . . . . . 6 ((𝜑𝑘 ∈ (1...2)) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
228227abscld 15321 . . . . 5 ((𝜑𝑘 ∈ (1...2)) → (abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ)
229 3rp 12921 . . . . . . 7 3 ∈ ℝ+
230 relogcl 25931 . . . . . . 7 (3 ∈ ℝ+ → (log‘3) ∈ ℝ)
231229, 230ax-mp 5 . . . . . 6 (log‘3) ∈ ℝ
232 elfznn 13470 . . . . . . 7 (𝑘 ∈ (1...2) → 𝑘 ∈ ℕ)
233232adantl 482 . . . . . 6 ((𝜑𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ)
234 nndivre 12194 . . . . . 6 (((log‘3) ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((log‘3) / 𝑘) ∈ ℝ)
235231, 233, 234sylancr 587 . . . . 5 ((𝜑𝑘 ∈ (1...2)) → ((log‘3) / 𝑘) ∈ ℝ)
236228, 235remulcld 11185 . . . 4 ((𝜑𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
237223, 236fsumrecl 15619 . . 3 (𝜑 → Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
23843abscld 15321 . . 3 (𝜑 → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
239237, 238readdcld 11184 . 2 (𝜑 → (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
240 simpl 483 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → 𝜑)
24162rexri 11213 . . . . . . . . . . 11 3 ∈ ℝ*
242 elico2 13328 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 3 ∈ ℝ*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚𝑚 < 3)))
243107, 241, 242mp2an 690 . . . . . . . . . 10 (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚𝑚 < 3))
244243simp1bi 1145 . . . . . . . . 9 (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ)
245244adantl 482 . . . . . . . 8 ((𝜑𝑚 ∈ (1[,)3)) → 𝑚 ∈ ℝ)
246 0red 11158 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 0 ∈ ℝ)
247 1red 11156 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 1 ∈ ℝ)
248 0lt1 11677 . . . . . . . . . 10 0 < 1
249248a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 0 < 1)
250243simp2bi 1146 . . . . . . . . . 10 (𝑚 ∈ (1[,)3) → 1 ≤ 𝑚)
251250adantl 482 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 1 ≤ 𝑚)
252246, 247, 245, 249, 251ltletrd 11315 . . . . . . . 8 ((𝜑𝑚 ∈ (1[,)3)) → 0 < 𝑚)
253245, 252elrpd 12954 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → 𝑚 ∈ ℝ+)
254240, 253jca 512 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → (𝜑𝑚 ∈ ℝ+))
25543adantr 481 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → if(𝑆 = 0, 0, 𝑇) ∈ ℂ)
25626, 255subcld 11512 . . . . . 6 ((𝜑𝑚 ∈ ℝ+) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) ∈ ℂ)
257254, 256syl 17 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) ∈ ℂ)
258257abscld 15321 . . . 4 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
259254, 26syl 17 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
260259abscld 15321 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
261238adantr 481 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
262260, 261readdcld 11184 . . . 4 ((𝜑𝑚 ∈ (1[,)3)) → ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
263237adantr 481 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
264263, 261readdcld 11184 . . . 4 ((𝜑𝑚 ∈ (1[,)3)) → (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
26526, 255abs2dif2d 15343 . . . . 5 ((𝜑𝑚 ∈ ℝ+) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))))
266254, 265syl 17 . . . 4 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))))
26725abscld 15321 . . . . . . . 8 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
2689, 267fsumrecl 15619 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
269254, 268syl 17 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
2709, 25fsumabs 15686 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
271254, 270syl 17 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
272 fzfid 13878 . . . . . . . . 9 ((𝜑𝑚 ∈ ℝ+) → (1...2) ∈ Fin)
273227adantlr 713 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
27417adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑚 ∈ ℝ+)
275232adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ)
276275nnrpd 12955 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℝ+)
277274, 276ifcld 4532 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+)
278277relogcld 25978 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ)
279278, 275nndivred 12207 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ)
280279recnd 11183 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℂ)
281273, 280mulcld 11175 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
282281abscld 15321 . . . . . . . . 9 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
283272, 282fsumrecl 15619 . . . . . . . 8 ((𝜑𝑚 ∈ ℝ+) → Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
284254, 283syl 17 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
285 fzfid 13878 . . . . . . . 8 ((𝜑𝑚 ∈ (1[,)3)) → (1...2) ∈ Fin)
286254, 281sylan 580 . . . . . . . . 9 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
287286abscld 15321 . . . . . . . 8 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
288286absge0d 15329 . . . . . . . 8 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤ (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
289245flcld 13703 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1[,)3)) → (⌊‘𝑚) ∈ ℤ)
290 2z 12535 . . . . . . . . . . 11 2 ∈ ℤ
291290a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1[,)3)) → 2 ∈ ℤ)
292243simp3bi 1147 . . . . . . . . . . . . . 14 (𝑚 ∈ (1[,)3) → 𝑚 < 3)
293292adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (1[,)3)) → 𝑚 < 3)
294 3z 12536 . . . . . . . . . . . . . 14 3 ∈ ℤ
295 fllt 13711 . . . . . . . . . . . . . 14 ((𝑚 ∈ ℝ ∧ 3 ∈ ℤ) → (𝑚 < 3 ↔ (⌊‘𝑚) < 3))
296245, 294, 295sylancl 586 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (1[,)3)) → (𝑚 < 3 ↔ (⌊‘𝑚) < 3))
297293, 296mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (1[,)3)) → (⌊‘𝑚) < 3)
298 df-3 12217 . . . . . . . . . . . 12 3 = (2 + 1)
299297, 298breqtrdi 5146 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (1[,)3)) → (⌊‘𝑚) < (2 + 1))
300 rpre 12923 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℝ+𝑚 ∈ ℝ)
301300adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ+) → 𝑚 ∈ ℝ)
302301flcld 13703 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → (⌊‘𝑚) ∈ ℤ)
303 zleltp1 12554 . . . . . . . . . . . . 13 (((⌊‘𝑚) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘𝑚) ≤ 2 ↔ (⌊‘𝑚) < (2 + 1)))
304302, 290, 303sylancl 586 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ+) → ((⌊‘𝑚) ≤ 2 ↔ (⌊‘𝑚) < (2 + 1)))
305254, 304syl 17 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (1[,)3)) → ((⌊‘𝑚) ≤ 2 ↔ (⌊‘𝑚) < (2 + 1)))
306299, 305mpbird 256 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1[,)3)) → (⌊‘𝑚) ≤ 2)
307 eluz2 12769 . . . . . . . . . 10 (2 ∈ (ℤ‘(⌊‘𝑚)) ↔ ((⌊‘𝑚) ∈ ℤ ∧ 2 ∈ ℤ ∧ (⌊‘𝑚) ≤ 2))
308289, 291, 306, 307syl3anbrc 1343 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 2 ∈ (ℤ‘(⌊‘𝑚)))
309 fzss2 13481 . . . . . . . . 9 (2 ∈ (ℤ‘(⌊‘𝑚)) → (1...(⌊‘𝑚)) ⊆ (1...2))
310308, 309syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ (1[,)3)) → (1...(⌊‘𝑚)) ⊆ (1...2))
311285, 287, 288, 310fsumless 15681 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
312236adantlr 713 . . . . . . . 8 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
313273, 280absmuld 15339 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) = ((abs‘(𝑋‘(𝐿𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
314254, 313sylan 580 . . . . . . . . 9 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) = ((abs‘(𝑋‘(𝐿𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
315254, 279sylan 580 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ)
316254, 278sylan 580 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ)
317 log1 25941 . . . . . . . . . . . . . 14 (log‘1) = 0
318 elfzle1 13444 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (1...2) → 1 ≤ 𝑘)
319 breq2 5109 . . . . . . . . . . . . . . . . 17 (𝑚 = if(𝑆 = 0, 𝑚, 𝑘) → (1 ≤ 𝑚 ↔ 1 ≤ if(𝑆 = 0, 𝑚, 𝑘)))
320 breq2 5109 . . . . . . . . . . . . . . . . 17 (𝑘 = if(𝑆 = 0, 𝑚, 𝑘) → (1 ≤ 𝑘 ↔ 1 ≤ if(𝑆 = 0, 𝑚, 𝑘)))
321319, 320ifboth 4525 . . . . . . . . . . . . . . . 16 ((1 ≤ 𝑚 ∧ 1 ≤ 𝑘) → 1 ≤ if(𝑆 = 0, 𝑚, 𝑘))
322251, 318, 321syl2an 596 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 1 ≤ if(𝑆 = 0, 𝑚, 𝑘))
323 1rp 12919 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ+
324 logleb 25958 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ+ ∧ if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+) → (1 ≤ if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘))))
325323, 277, 324sylancr 587 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (1 ≤ if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘))))
326254, 325sylan 580 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (1 ≤ if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘))))
327322, 326mpbid 231 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘1) ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘)))
328317, 327eqbrtrrid 5141 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘)))
329276rpregt0d 12963 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
330254, 329sylan 580 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
331 divge0 12024 . . . . . . . . . . . . 13 ((((log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ ∧ 0 ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘))) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))
332316, 328, 330, 331syl21anc 836 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤ ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))
333315, 332absidd 15307 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))
334333, 315eqeltrd 2838 . . . . . . . . . 10 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℝ)
335235adantlr 713 . . . . . . . . . 10 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘3) / 𝑘) ∈ ℝ)
336228adantlr 713 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ)
337273absge0d 15329 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 0 ≤ (abs‘(𝑋‘(𝐿𝑘))))
338336, 337jca 512 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ ∧ 0 ≤ (abs‘(𝑋‘(𝐿𝑘)))))
339254, 338sylan 580 . . . . . . . . . 10 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ ∧ 0 ≤ (abs‘(𝑋‘(𝐿𝑘)))))
340292ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 𝑚 < 3)
341275nnred 12168 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℝ)
342 2re 12227 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
343342a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 2 ∈ ℝ)
34462a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 3 ∈ ℝ)
345 elfzle2 13445 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (1...2) → 𝑘 ≤ 2)
346345adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ≤ 2)
347 2lt3 12325 . . . . . . . . . . . . . . . . . 18 2 < 3
348347a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 2 < 3)
349341, 343, 344, 346, 348lelttrd 11313 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 < 3)
350254, 349sylan 580 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 𝑘 < 3)
351 breq1 5108 . . . . . . . . . . . . . . . 16 (𝑚 = if(𝑆 = 0, 𝑚, 𝑘) → (𝑚 < 3 ↔ if(𝑆 = 0, 𝑚, 𝑘) < 3))
352 breq1 5108 . . . . . . . . . . . . . . . 16 (𝑘 = if(𝑆 = 0, 𝑚, 𝑘) → (𝑘 < 3 ↔ if(𝑆 = 0, 𝑚, 𝑘) < 3))
353351, 352ifboth 4525 . . . . . . . . . . . . . . 15 ((𝑚 < 3 ∧ 𝑘 < 3) → if(𝑆 = 0, 𝑚, 𝑘) < 3)
354340, 350, 353syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) < 3)
355277rpred 12957 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ)
356 ltle 11243 . . . . . . . . . . . . . . . 16 ((if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ ∧ 3 ∈ ℝ) → (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3))
357355, 62, 356sylancl 586 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3))
358254, 357sylan 580 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3))
359354, 358mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3)
360 logleb 25958 . . . . . . . . . . . . . . 15 ((if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+ ∧ 3 ∈ ℝ+) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3)))
361277, 229, 360sylancl 586 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3)))
362254, 361sylan 580 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3)))
363359, 362mpbid 231 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3))
364231a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (log‘3) ∈ ℝ)
365278, 364, 276lediv1d 13003 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3) ↔ ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘)))
366254, 365sylan 580 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3) ↔ ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘)))
367363, 366mpbid 231 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘))
368333, 367eqbrtrd 5127 . . . . . . . . . 10 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ≤ ((log‘3) / 𝑘))
369 lemul2a 12010 . . . . . . . . . 10 ((((abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℝ ∧ ((log‘3) / 𝑘) ∈ ℝ ∧ ((abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ ∧ 0 ≤ (abs‘(𝑋‘(𝐿𝑘))))) ∧ (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ≤ ((log‘3) / 𝑘)) → ((abs‘(𝑋‘(𝐿𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
370334, 335, 339, 368, 369syl31anc 1373 . . . . . . . . 9 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
371314, 370eqbrtrd 5127 . . . . . . . 8 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
372285, 287, 312, 371fsumle 15684 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
373269, 284, 263, 311, 372letrd 11312 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
374260, 269, 263, 271, 373letrd 11312 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
37526abscld 15321 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
376237adantr 481 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
377255abscld 15321 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
378375, 376, 377leadd1d 11749 . . . . . 6 ((𝜑𝑚 ∈ ℝ+) → ((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, 𝑇)))))
379254, 378syl 17 . . . . 5 ((𝜑𝑚 ∈ (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, 𝑇)))))
380374, 379mpbid 231 . . . 4 ((𝜑𝑚 ∈ (1[,)3)) → ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))))
381258, 262, 264, 266, 380letrd 11312 . . 3 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))))
382381ralrimiva 3143 . 2 (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))))
3831, 2, 3, 4, 5, 6, 7, 8, 26, 34, 37, 43, 222, 239, 382dchrvmasumlem3 26847 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · (Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wss 3910  ifcif 4486   class class class wbr 5105  cmpt 5188  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  +∞cpnf 11186  *cxr 11188   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  3c3 12209  cz 12499  cuz 12763  +crp 12915  [,)cico 13266  ...cfz 13424  cfl 13695  seqcseq 13906  abscabs 15119  cli 15366  𝑂(1)co1 15368  Σcsu 15570  Basecbs 17083  0gc0g 17321  ℤRHomczrh 20900  ℤ/nczn 20903  logclog 25910  μcmu 26444  DChrcdchr 26580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-tpos 8157  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-er 8648  df-ec 8650  df-qs 8654  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-acn 9878  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-o1 15372  df-lo1 15373  df-sum 15571  df-ef 15950  df-e 15951  df-sin 15952  df-cos 15953  df-tan 15954  df-pi 15955  df-dvds 16137  df-prm 16548  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-qus 17391  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-nsg 18926  df-eqg 18927  df-ghm 19006  df-cntz 19097  df-od 19310  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-cring 19967  df-oppr 20049  df-dvdsr 20070  df-unit 20071  df-invr 20101  df-dvr 20112  df-rnghom 20146  df-drng 20187  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-sra 20633  df-rgmod 20634  df-lidl 20635  df-rsp 20636  df-2idl 20702  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-zring 20870  df-zrh 20904  df-zn 20907  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231  df-ulm 25736  df-log 25912  df-cxp 25913  df-atan 26217  df-em 26342  df-mu 26450  df-dchr 26581
This theorem is referenced by:  dchrvmasumiflem2  26850
  Copyright terms: Public domain W3C validator