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

Theorem dchrvmasumiflem1 25659
Description: Lemma for dchrvmasumif 25661. (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 13096 . . 3 ((𝜑𝑚 ∈ ℝ+) → (1...(⌊‘𝑚)) ∈ Fin)
10 simpl 476 . . . . 5 ((𝜑𝑚 ∈ ℝ+) → 𝜑)
11 elfznn 12692 . . . . 5 (𝑘 ∈ (1...(⌊‘𝑚)) → 𝑘 ∈ ℕ)
127adantr 474 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑋𝐷)
13 nnz 11756 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
1413adantl 475 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
154, 1, 5, 2, 12, 14dchrzrhcl 25433 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
1610, 11, 15syl2an 589 . . . 4 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
17 simpr 479 . . . . . . . 8 ((𝜑𝑚 ∈ ℝ+) → 𝑚 ∈ ℝ+)
1811nnrpd 12184 . . . . . . . 8 (𝑘 ∈ (1...(⌊‘𝑚)) → 𝑘 ∈ ℝ+)
19 ifcl 4351 . . . . . . . 8 ((𝑚 ∈ ℝ+𝑘 ∈ ℝ+) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+)
2017, 18, 19syl2an 589 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+)
2120relogcld 24817 . . . . . 6 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ)
2211adantl 475 . . . . . 6 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℕ)
2321, 22nndivred 11434 . . . . 5 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ)
2423recnd 10407 . . . 4 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℂ)
2516, 24mulcld 10399 . . 3 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
269, 25fsumcl 14880 . 2 ((𝜑𝑚 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
27 fveq2 6448 . . . 4 (𝑚 = (𝑥 / 𝑑) → (⌊‘𝑚) = (⌊‘(𝑥 / 𝑑)))
2827oveq2d 6940 . . 3 (𝑚 = (𝑥 / 𝑑) → (1...(⌊‘𝑚)) = (1...(⌊‘(𝑥 / 𝑑))))
29 ifeq1 4311 . . . . . . 7 (𝑚 = (𝑥 / 𝑑) → if(𝑆 = 0, 𝑚, 𝑘) = if(𝑆 = 0, (𝑥 / 𝑑), 𝑘))
3029fveq2d 6452 . . . . . 6 (𝑚 = (𝑥 / 𝑑) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)))
3130oveq1d 6939 . . . . 5 (𝑚 = (𝑥 / 𝑑) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘))
3231oveq2d 6940 . . . 4 (𝑚 = (𝑥 / 𝑑) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)))
3332adantr 474 . . 3 ((𝑚 = (𝑥 / 𝑑) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)))
3428, 33sumeq12rdv 14854 . 2 (𝑚 = (𝑥 / 𝑑) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)))
35 dchrvmasumif.c . . 3 (𝜑𝐶 ∈ (0[,)+∞))
36 dchrvmasumif.e . . 3 (𝜑𝐸 ∈ (0[,)+∞))
3735, 36ifcld 4352 . 2 (𝜑 → if(𝑆 = 0, 𝐶, 𝐸) ∈ (0[,)+∞))
38 0cn 10370 . . 3 0 ∈ ℂ
39 dchrvmasumif.t . . . 4 (𝜑 → seq1( + , 𝐾) ⇝ 𝑇)
40 climcl 14647 . . . 4 (seq1( + , 𝐾) ⇝ 𝑇𝑇 ∈ ℂ)
4139, 40syl 17 . . 3 (𝜑𝑇 ∈ ℂ)
42 ifcl 4351 . . 3 ((0 ∈ ℂ ∧ 𝑇 ∈ ℂ) → if(𝑆 = 0, 0, 𝑇) ∈ ℂ)
4338, 41, 42sylancr 581 . 2 (𝜑 → if(𝑆 = 0, 0, 𝑇) ∈ ℂ)
44 nnuz 12034 . . . . . . . . 9 ℕ = (ℤ‘1)
45 1zzd 11765 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
46 nncn 11388 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
4746adantl 475 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
48 nnne0 11415 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
4948adantl 475 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ≠ 0)
5015, 47, 49divcld 11154 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑋‘(𝐿𝑘)) / 𝑘) ∈ ℂ)
51 dchrvmasumif.f . . . . . . . . . . . 12 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎))
52 2fveq3 6453 . . . . . . . . . . . . . 14 (𝑎 = 𝑘 → (𝑋‘(𝐿𝑎)) = (𝑋‘(𝐿𝑘)))
53 id 22 . . . . . . . . . . . . . 14 (𝑎 = 𝑘𝑎 = 𝑘)
5452, 53oveq12d 6942 . . . . . . . . . . . . 13 (𝑎 = 𝑘 → ((𝑋‘(𝐿𝑎)) / 𝑎) = ((𝑋‘(𝐿𝑘)) / 𝑘))
5554cbvmptv 4987 . . . . . . . . . . . 12 (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / 𝑎)) = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿𝑘)) / 𝑘))
5651, 55eqtri 2802 . . . . . . . . . . 11 𝐹 = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿𝑘)) / 𝑘))
5750, 56fmptd 6650 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶ℂ)
58 ffvelrn 6623 . . . . . . . . . 10 ((𝐹:ℕ⟶ℂ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
5957, 58sylan 575 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
6044, 45, 59serf 13152 . . . . . . . 8 (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
6160ad2antrr 716 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → seq1( + , 𝐹):ℕ⟶ℂ)
62 3re 11460 . . . . . . . . . . 11 3 ∈ ℝ
63 elicopnf 12587 . . . . . . . . . . 11 (3 ∈ ℝ → (𝑚 ∈ (3[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 3 ≤ 𝑚)))
6462, 63mp1i 13 . . . . . . . . . 10 (𝜑 → (𝑚 ∈ (3[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 3 ≤ 𝑚)))
6564simprbda 494 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → 𝑚 ∈ ℝ)
66 1red 10379 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 1 ∈ ℝ)
6762a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 3 ∈ ℝ)
68 1le3 11599 . . . . . . . . . . 11 1 ≤ 3
6968a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 1 ≤ 3)
7064simplbda 495 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 3 ≤ 𝑚)
7166, 67, 65, 69, 70letrd 10535 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → 1 ≤ 𝑚)
72 flge1nn 12946 . . . . . . . . 9 ((𝑚 ∈ ℝ ∧ 1 ≤ 𝑚) → (⌊‘𝑚) ∈ ℕ)
7365, 71, 72syl2anc 579 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → (⌊‘𝑚) ∈ ℕ)
7473adantr 474 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (⌊‘𝑚) ∈ ℕ)
7561, 74ffvelrnd 6626 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
7675abscld 14590 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ∈ ℝ)
77 simpl 476 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → 𝜑)
78 0red 10382 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 0 ∈ ℝ)
79 3pos 11492 . . . . . . . . . . 11 0 < 3
8079a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → 0 < 3)
8178, 67, 65, 80, 70ltletrd 10538 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → 0 < 𝑚)
8265, 81elrpd 12183 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → 𝑚 ∈ ℝ+)
8377, 82jca 507 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → (𝜑𝑚 ∈ ℝ+))
84 elrege0 12597 . . . . . . . . . 10 (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
8584simplbi 493 . . . . . . . . 9 (𝐶 ∈ (0[,)+∞) → 𝐶 ∈ ℝ)
8635, 85syl 17 . . . . . . . 8 (𝜑𝐶 ∈ ℝ)
87 rerpdivcl 12174 . . . . . . . 8 ((𝐶 ∈ ℝ ∧ 𝑚 ∈ ℝ+) → (𝐶 / 𝑚) ∈ ℝ)
8886, 87sylan 575 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → (𝐶 / 𝑚) ∈ ℝ)
8983, 88syl 17 . . . . . 6 ((𝜑𝑚 ∈ (3[,)+∞)) → (𝐶 / 𝑚) ∈ ℝ)
9089adantr 474 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (𝐶 / 𝑚) ∈ ℝ)
9182relogcld 24817 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → (log‘𝑚) ∈ ℝ)
9265, 71logge0d 24824 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → 0 ≤ (log‘𝑚))
9391, 92jca 507 . . . . . 6 ((𝜑𝑚 ∈ (3[,)+∞)) → ((log‘𝑚) ∈ ℝ ∧ 0 ≤ (log‘𝑚)))
9493adantr 474 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) ∈ ℝ ∧ 0 ≤ (log‘𝑚)))
95 oveq2 6932 . . . . . . . 8 (𝑆 = 0 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 0))
9660adantr 474 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → seq1( + , 𝐹):ℕ⟶ℂ)
9796, 73ffvelrnd 6626 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
9897subid1d 10725 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 0) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
9995, 98sylan9eqr 2836 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
10099fveq2d 6452 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) = (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))))
101 2fveq3 6453 . . . . . . . . . 10 (𝑦 = 𝑚 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
102101fvoveq1d 6946 . . . . . . . . 9 (𝑦 = 𝑚 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)))
103 oveq2 6932 . . . . . . . . 9 (𝑦 = 𝑚 → (𝐶 / 𝑦) = (𝐶 / 𝑚))
104102, 103breq12d 4901 . . . . . . . 8 (𝑦 = 𝑚 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚)))
105 dchrvmasumif.1 . . . . . . . . 9 (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))
106105adantr 474 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))
107 1re 10378 . . . . . . . . . 10 1 ∈ ℝ
108 elicopnf 12587 . . . . . . . . . 10 (1 ∈ ℝ → (𝑚 ∈ (1[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚)))
109107, 108ax-mp 5 . . . . . . . . 9 (𝑚 ∈ (1[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚))
11065, 71, 109sylanbrc 578 . . . . . . . 8 ((𝜑𝑚 ∈ (3[,)+∞)) → 𝑚 ∈ (1[,)+∞))
111104, 106, 110rspcdva 3517 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚))
112111adantr 474 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚))
113100, 112eqbrtrrd 4912 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ≤ (𝐶 / 𝑚))
114 lemul2a 11235 . . . . 5 ((((abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ∈ ℝ ∧ (𝐶 / 𝑚) ∈ ℝ ∧ ((log‘𝑚) ∈ ℝ ∧ 0 ≤ (log‘𝑚))) ∧ (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ≤ (𝐶 / 𝑚)) → ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((log‘𝑚) · (𝐶 / 𝑚)))
11576, 90, 94, 113, 114syl31anc 1441 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((log‘𝑚) · (𝐶 / 𝑚)))
116 iftrue 4313 . . . . . . . . . . . . . . 15 (𝑆 = 0 → if(𝑆 = 0, 𝑚, 𝑘) = 𝑚)
117116fveq2d 6452 . . . . . . . . . . . . . 14 (𝑆 = 0 → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘𝑚))
118117oveq1d 6939 . . . . . . . . . . . . 13 (𝑆 = 0 → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑚) / 𝑘))
119118ad2antlr 717 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑚) / 𝑘))
120119oveq2d 6940 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑚) / 𝑘)))
12116adantlr 705 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
122 relogcl 24770 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℝ+ → (log‘𝑚) ∈ ℝ)
123122adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ+) → (log‘𝑚) ∈ ℝ)
124123recnd 10407 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → (log‘𝑚) ∈ ℂ)
125124ad2antrr 716 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (log‘𝑚) ∈ ℂ)
12611adantl 475 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℕ)
127126nncnd 11397 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℂ)
128126nnne0d 11430 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ≠ 0)
129121, 125, 127, 128div12d 11190 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘𝑚) / 𝑘)) = ((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
130120, 129eqtrd 2814 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
131130sumeq2dv 14850 . . . . . . . . 9 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
132 iftrue 4313 . . . . . . . . . . 11 (𝑆 = 0 → if(𝑆 = 0, 0, 𝑇) = 0)
133132oveq2d 6940 . . . . . . . . . 10 (𝑆 = 0 → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − 0))
13426subid1d 10725 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℝ+) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − 0) = Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))
135133, 134sylan9eqr 2836 . . . . . . . . 9 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))
136 ovex 6956 . . . . . . . . . . . . . 14 ((𝑋‘(𝐿𝑘)) / 𝑘) ∈ V
13754, 51, 136fvmpt 6544 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝐹𝑘) = ((𝑋‘(𝐿𝑘)) / 𝑘))
13822, 137syl 17 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐹𝑘) = ((𝑋‘(𝐿𝑘)) / 𝑘))
13957adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → 𝐹:ℕ⟶ℂ)
140139, 11, 58syl2an 589 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐹𝑘) ∈ ℂ)
141138, 140eqeltrrd 2860 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) / 𝑘) ∈ ℂ)
1429, 124, 141fsummulc2 14929 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℝ+) → ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
143142adantr 474 . . . . . . . . 9 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿𝑘)) / 𝑘)))
144131, 135, 1433eqtr4d 2824 . . . . . . . 8 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)))
14583, 144sylan 575 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)))
14683, 138sylan 575 . . . . . . . . . 10 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐹𝑘) = ((𝑋‘(𝐿𝑘)) / 𝑘))
14773, 44syl6eleq 2869 . . . . . . . . . 10 ((𝜑𝑚 ∈ (3[,)+∞)) → (⌊‘𝑚) ∈ (ℤ‘1))
14877, 11, 50syl2an 589 . . . . . . . . . 10 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) / 𝑘) ∈ ℂ)
149146, 147, 148fsumser 14877 . . . . . . . . 9 ((𝜑𝑚 ∈ (3[,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
150149adantr 474 . . . . . . . 8 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
151150oveq2d 6940 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) / 𝑘)) = ((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚))))
152145, 151eqtrd 2814 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚))))
153152fveq2d 6452 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = (abs‘((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚)))))
154122ad2antlr 717 . . . . . . . 8 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (log‘𝑚) ∈ ℝ)
155154recnd 10407 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (log‘𝑚) ∈ ℂ)
15683, 155sylan 575 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (log‘𝑚) ∈ ℂ)
157156, 75absmuld 14608 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((abs‘(log‘𝑚)) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))))
15891, 92absidd 14576 . . . . . . 7 ((𝜑𝑚 ∈ (3[,)+∞)) → (abs‘(log‘𝑚)) = (log‘𝑚))
159158oveq1d 6939 . . . . . 6 ((𝜑𝑚 ∈ (3[,)+∞)) → ((abs‘(log‘𝑚)) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))))
160159adantr 474 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((abs‘(log‘𝑚)) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))))
161153, 157, 1603eqtrd 2818 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))))
162 iftrue 4313 . . . . . . . 8 (𝑆 = 0 → if(𝑆 = 0, 𝐶, 𝐸) = 𝐶)
163162adantl 475 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → if(𝑆 = 0, 𝐶, 𝐸) = 𝐶)
164163oveq1d 6939 . . . . . 6 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘𝑚) / 𝑚)))
16586recnd 10407 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
166165ad2antrr 716 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → 𝐶 ∈ ℂ)
167 rpcnne0 12162 . . . . . . . 8 (𝑚 ∈ ℝ+ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
168167ad2antlr 717 . . . . . . 7 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
169 div12 11058 . . . . . . 7 ((𝐶 ∈ ℂ ∧ (log‘𝑚) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → (𝐶 · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚)))
170166, 155, 168, 169syl3anc 1439 . . . . . 6 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (𝐶 · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚)))
171164, 170eqtrd 2814 . . . . 5 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚)))
17283, 171sylan 575 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚)))
173115, 161, 1723brtr4d 4920 . . 3 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)))
174 dchrvmasumif.2 . . . . . 6 (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)))
175 2fveq3 6453 . . . . . . . . 9 (𝑦 = 𝑚 → (seq1( + , 𝐾)‘(⌊‘𝑦)) = (seq1( + , 𝐾)‘(⌊‘𝑚)))
176175fvoveq1d 6946 . . . . . . . 8 (𝑦 = 𝑚 → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)))
177 fveq2 6448 . . . . . . . . . 10 (𝑦 = 𝑚 → (log‘𝑦) = (log‘𝑚))
178 id 22 . . . . . . . . . 10 (𝑦 = 𝑚𝑦 = 𝑚)
179177, 178oveq12d 6942 . . . . . . . . 9 (𝑦 = 𝑚 → ((log‘𝑦) / 𝑦) = ((log‘𝑚) / 𝑚))
180179oveq2d 6940 . . . . . . . 8 (𝑦 = 𝑚 → (𝐸 · ((log‘𝑦) / 𝑦)) = (𝐸 · ((log‘𝑚) / 𝑚)))
181176, 180breq12d 4901 . . . . . . 7 (𝑦 = 𝑚 → ((abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)) ↔ (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚))))
182181rspccva 3510 . . . . . 6 ((∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)) ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚)))
183174, 182sylan 575 . . . . 5 ((𝜑𝑚 ∈ (3[,)+∞)) → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚)))
184183adantr 474 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚)))
185 fveq2 6448 . . . . . . . . . . . 12 (𝑎 = 𝑘 → (log‘𝑎) = (log‘𝑘))
186185, 53oveq12d 6942 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((log‘𝑎) / 𝑎) = ((log‘𝑘) / 𝑘))
18752, 186oveq12d 6942 . . . . . . . . . 10 (𝑎 = 𝑘 → ((𝑋‘(𝐿𝑎)) · ((log‘𝑎) / 𝑎)) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
188 dchrvmasumif.g . . . . . . . . . 10 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) · ((log‘𝑎) / 𝑎)))
189 ovex 6956 . . . . . . . . . 10 ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)) ∈ V
190187, 188, 189fvmpt 6544 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐾𝑘) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
19111, 190syl 17 . . . . . . . 8 (𝑘 ∈ (1...(⌊‘𝑚)) → (𝐾𝑘) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
192 ifnefalse 4319 . . . . . . . . . . . . 13 (𝑆 ≠ 0 → if(𝑆 = 0, 𝑚, 𝑘) = 𝑘)
193192fveq2d 6452 . . . . . . . . . . . 12 (𝑆 ≠ 0 → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘𝑘))
194193oveq1d 6939 . . . . . . . . . . 11 (𝑆 ≠ 0 → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑘) / 𝑘))
195194oveq2d 6940 . . . . . . . . . 10 (𝑆 ≠ 0 → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
196195adantl 475 . . . . . . . . 9 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
197196eqcomd 2784 . . . . . . . 8 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)) = ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))
198191, 197sylan9eqr 2836 . . . . . . 7 ((((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐾𝑘) = ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))
199147adantr 474 . . . . . . 7 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (⌊‘𝑚) ∈ (ℤ‘1))
200 nnrp 12155 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
201200adantl 475 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
202201relogcld 24817 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (log‘𝑘) ∈ ℝ)
203202recnd 10407 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (log‘𝑘) ∈ ℂ)
204203, 47, 49divcld 11154 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((log‘𝑘) / 𝑘) ∈ ℂ)
20515, 204mulcld 10399 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)) ∈ ℂ)
206187cbvmptv 4987 . . . . . . . . . . . 12 (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) · ((log‘𝑎) / 𝑎))) = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
207188, 206eqtri 2802 . . . . . . . . . . 11 𝐾 = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿𝑘)) · ((log‘𝑘) / 𝑘)))
208205, 207fmptd 6650 . . . . . . . . . 10 (𝜑𝐾:ℕ⟶ℂ)
209208ad2antrr 716 . . . . . . . . 9 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → 𝐾:ℕ⟶ℂ)
210 ffvelrn 6623 . . . . . . . . 9 ((𝐾:ℕ⟶ℂ ∧ 𝑘 ∈ ℕ) → (𝐾𝑘) ∈ ℂ)
211209, 11, 210syl2an 589 . . . . . . . 8 ((((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝐾𝑘) ∈ ℂ)
212198, 211eqeltrrd 2860 . . . . . . 7 ((((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
213198, 199, 212fsumser 14877 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = (seq1( + , 𝐾)‘(⌊‘𝑚)))
214 ifnefalse 4319 . . . . . . 7 (𝑆 ≠ 0 → if(𝑆 = 0, 0, 𝑇) = 𝑇)
215214adantl 475 . . . . . 6 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → if(𝑆 = 0, 0, 𝑇) = 𝑇)
216213, 215oveq12d 6942 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇))
217216fveq2d 6452 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)))
218 ifnefalse 4319 . . . . . 6 (𝑆 ≠ 0 → if(𝑆 = 0, 𝐶, 𝐸) = 𝐸)
219218adantl 475 . . . . 5 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → if(𝑆 = 0, 𝐶, 𝐸) = 𝐸)
220219oveq1d 6939 . . . 4 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = (𝐸 · ((log‘𝑚) / 𝑚)))
221184, 217, 2203brtr4d 4920 . . 3 (((𝜑𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)))
222173, 221pm2.61dane 3057 . 2 ((𝜑𝑚 ∈ (3[,)+∞)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)))
223 fzfid 13096 . . . 4 (𝜑 → (1...2) ∈ Fin)
2247adantr 474 . . . . . . 7 ((𝜑𝑘 ∈ (1...2)) → 𝑋𝐷)
225 elfzelz 12664 . . . . . . . 8 (𝑘 ∈ (1...2) → 𝑘 ∈ ℤ)
226225adantl 475 . . . . . . 7 ((𝜑𝑘 ∈ (1...2)) → 𝑘 ∈ ℤ)
2274, 1, 5, 2, 224, 226dchrzrhcl 25433 . . . . . 6 ((𝜑𝑘 ∈ (1...2)) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
228227abscld 14590 . . . . 5 ((𝜑𝑘 ∈ (1...2)) → (abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ)
22962, 79elrpii 12145 . . . . . . 7 3 ∈ ℝ+
230 relogcl 24770 . . . . . . 7 (3 ∈ ℝ+ → (log‘3) ∈ ℝ)
231229, 230ax-mp 5 . . . . . 6 (log‘3) ∈ ℝ
232 elfznn 12692 . . . . . . 7 (𝑘 ∈ (1...2) → 𝑘 ∈ ℕ)
233232adantl 475 . . . . . 6 ((𝜑𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ)
234 nndivre 11421 . . . . . 6 (((log‘3) ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((log‘3) / 𝑘) ∈ ℝ)
235231, 233, 234sylancr 581 . . . . 5 ((𝜑𝑘 ∈ (1...2)) → ((log‘3) / 𝑘) ∈ ℝ)
236228, 235remulcld 10409 . . . 4 ((𝜑𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
237223, 236fsumrecl 14881 . . 3 (𝜑 → Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
23843abscld 14590 . . 3 (𝜑 → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
239237, 238readdcld 10408 . 2 (𝜑 → (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
240 simpl 476 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → 𝜑)
24162rexri 10437 . . . . . . . . . . 11 3 ∈ ℝ*
242 elico2 12554 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 3 ∈ ℝ*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚𝑚 < 3)))
243107, 241, 242mp2an 682 . . . . . . . . . 10 (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚𝑚 < 3))
244243simp1bi 1136 . . . . . . . . 9 (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ)
245244adantl 475 . . . . . . . 8 ((𝜑𝑚 ∈ (1[,)3)) → 𝑚 ∈ ℝ)
246 0red 10382 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 0 ∈ ℝ)
247 1red 10379 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 1 ∈ ℝ)
248 0lt1 10900 . . . . . . . . . 10 0 < 1
249248a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 0 < 1)
250243simp2bi 1137 . . . . . . . . . 10 (𝑚 ∈ (1[,)3) → 1 ≤ 𝑚)
251250adantl 475 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 1 ≤ 𝑚)
252246, 247, 245, 249, 251ltletrd 10538 . . . . . . . 8 ((𝜑𝑚 ∈ (1[,)3)) → 0 < 𝑚)
253245, 252elrpd 12183 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → 𝑚 ∈ ℝ+)
254240, 253jca 507 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → (𝜑𝑚 ∈ ℝ+))
25543adantr 474 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → if(𝑆 = 0, 0, 𝑇) ∈ ℂ)
25626, 255subcld 10736 . . . . . 6 ((𝜑𝑚 ∈ ℝ+) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) ∈ ℂ)
257254, 256syl 17 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) ∈ ℂ)
258257abscld 14590 . . . 4 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
259254, 26syl 17 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
260259abscld 14590 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
261238adantr 474 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
262260, 261readdcld 10408 . . . 4 ((𝜑𝑚 ∈ (1[,)3)) → ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
263237adantr 474 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
264263, 261readdcld 10408 . . . 4 ((𝜑𝑚 ∈ (1[,)3)) → (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
26526, 255abs2dif2d 14612 . . . . 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 14590 . . . . . . . 8 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
2689, 267fsumrecl 14881 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
269254, 268syl 17 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
2709, 25fsumabs 14946 . . . . . . 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 13096 . . . . . . . . 9 ((𝜑𝑚 ∈ ℝ+) → (1...2) ∈ Fin)
273227adantlr 705 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (𝑋‘(𝐿𝑘)) ∈ ℂ)
27417adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑚 ∈ ℝ+)
275232adantl 475 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ)
276275nnrpd 12184 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℝ+)
277274, 276ifcld 4352 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+)
278277relogcld 24817 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ)
279278, 275nndivred 11434 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ)
280279recnd 10407 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℂ)
281273, 280mulcld 10399 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
282281abscld 14590 . . . . . . . . 9 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
283272, 282fsumrecl 14881 . . . . . . . 8 ((𝜑𝑚 ∈ ℝ+) → Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
284254, 283syl 17 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
285 fzfid 13096 . . . . . . . 8 ((𝜑𝑚 ∈ (1[,)3)) → (1...2) ∈ Fin)
286254, 281sylan 575 . . . . . . . . 9 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ)
287286abscld 14590 . . . . . . . 8 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
288286absge0d 14598 . . . . . . . 8 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤ (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
289245flcld 12923 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1[,)3)) → (⌊‘𝑚) ∈ ℤ)
290 2z 11766 . . . . . . . . . . 11 2 ∈ ℤ
291290a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1[,)3)) → 2 ∈ ℤ)
292243simp3bi 1138 . . . . . . . . . . . . . 14 (𝑚 ∈ (1[,)3) → 𝑚 < 3)
293292adantl 475 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (1[,)3)) → 𝑚 < 3)
294 3z 11767 . . . . . . . . . . . . . 14 3 ∈ ℤ
295 fllt 12931 . . . . . . . . . . . . . 14 ((𝑚 ∈ ℝ ∧ 3 ∈ ℤ) → (𝑚 < 3 ↔ (⌊‘𝑚) < 3))
296245, 294, 295sylancl 580 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (1[,)3)) → (𝑚 < 3 ↔ (⌊‘𝑚) < 3))
297293, 296mpbid 224 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (1[,)3)) → (⌊‘𝑚) < 3)
298 df-3 11444 . . . . . . . . . . . 12 3 = (2 + 1)
299297, 298syl6breq 4929 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (1[,)3)) → (⌊‘𝑚) < (2 + 1))
300 rpre 12150 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℝ+𝑚 ∈ ℝ)
301300adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ+) → 𝑚 ∈ ℝ)
302301flcld 12923 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → (⌊‘𝑚) ∈ ℤ)
303 zleltp1 11785 . . . . . . . . . . . . 13 (((⌊‘𝑚) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘𝑚) ≤ 2 ↔ (⌊‘𝑚) < (2 + 1)))
304302, 290, 303sylancl 580 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ+) → ((⌊‘𝑚) ≤ 2 ↔ (⌊‘𝑚) < (2 + 1)))
305254, 304syl 17 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (1[,)3)) → ((⌊‘𝑚) ≤ 2 ↔ (⌊‘𝑚) < (2 + 1)))
306299, 305mpbird 249 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1[,)3)) → (⌊‘𝑚) ≤ 2)
307 eluz2 12003 . . . . . . . . . 10 (2 ∈ (ℤ‘(⌊‘𝑚)) ↔ ((⌊‘𝑚) ∈ ℤ ∧ 2 ∈ ℤ ∧ (⌊‘𝑚) ≤ 2))
308289, 291, 306, 307syl3anbrc 1400 . . . . . . . . 9 ((𝜑𝑚 ∈ (1[,)3)) → 2 ∈ (ℤ‘(⌊‘𝑚)))
309 fzss2 12703 . . . . . . . . 9 (2 ∈ (ℤ‘(⌊‘𝑚)) → (1...(⌊‘𝑚)) ⊆ (1...2))
310308, 309syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ (1[,)3)) → (1...(⌊‘𝑚)) ⊆ (1...2))
311285, 287, 288, 310fsumless 14941 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
312236adantlr 705 . . . . . . . 8 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
313273, 280absmuld 14608 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) = ((abs‘(𝑋‘(𝐿𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
314254, 313sylan 575 . . . . . . . . 9 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) = ((abs‘(𝑋‘(𝐿𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))))
315254, 279sylan 575 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ)
316254, 278sylan 575 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ)
317 log1 24780 . . . . . . . . . . . . . 14 (log‘1) = 0
318 elfzle1 12666 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (1...2) → 1 ≤ 𝑘)
319 breq2 4892 . . . . . . . . . . . . . . . . 17 (𝑚 = if(𝑆 = 0, 𝑚, 𝑘) → (1 ≤ 𝑚 ↔ 1 ≤ if(𝑆 = 0, 𝑚, 𝑘)))
320 breq2 4892 . . . . . . . . . . . . . . . . 17 (𝑘 = if(𝑆 = 0, 𝑚, 𝑘) → (1 ≤ 𝑘 ↔ 1 ≤ if(𝑆 = 0, 𝑚, 𝑘)))
321319, 320ifboth 4345 . . . . . . . . . . . . . . . 16 ((1 ≤ 𝑚 ∧ 1 ≤ 𝑘) → 1 ≤ if(𝑆 = 0, 𝑚, 𝑘))
322251, 318, 321syl2an 589 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 1 ≤ if(𝑆 = 0, 𝑚, 𝑘))
323 1rp 12146 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ+
324 logleb 24797 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ+ ∧ if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+) → (1 ≤ if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘))))
325323, 277, 324sylancr 581 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (1 ≤ if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘))))
326254, 325sylan 575 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (1 ≤ if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘))))
327322, 326mpbid 224 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘1) ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘)))
328317, 327syl5eqbrr 4924 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘)))
329276rpregt0d 12192 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
330254, 329sylan 575 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
331 divge0 11249 . . . . . . . . . . . . 13 ((((log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ ∧ 0 ≤ (log‘if(𝑆 = 0, 𝑚, 𝑘))) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))
332316, 328, 330, 331syl21anc 828 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤ ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))
333315, 332absidd 14576 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))
334333, 315eqeltrd 2859 . . . . . . . . . 10 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℝ)
335235adantlr 705 . . . . . . . . . 10 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘3) / 𝑘) ∈ ℝ)
336228adantlr 705 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ)
337273absge0d 14598 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 0 ≤ (abs‘(𝑋‘(𝐿𝑘))))
338336, 337jca 507 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ ∧ 0 ≤ (abs‘(𝑋‘(𝐿𝑘)))))
339254, 338sylan 575 . . . . . . . . . 10 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) ∈ ℝ ∧ 0 ≤ (abs‘(𝑋‘(𝐿𝑘)))))
340292ad2antlr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 𝑚 < 3)
341275nnred 11396 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℝ)
342 2re 11454 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
343342a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 2 ∈ ℝ)
34462a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 3 ∈ ℝ)
345 elfzle2 12667 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (1...2) → 𝑘 ≤ 2)
346345adantl 475 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ≤ 2)
347 2lt3 11559 . . . . . . . . . . . . . . . . . 18 2 < 3
348347a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 2 < 3)
349341, 343, 344, 346, 348lelttrd 10536 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 < 3)
350254, 349sylan 575 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 𝑘 < 3)
351 breq1 4891 . . . . . . . . . . . . . . . 16 (𝑚 = if(𝑆 = 0, 𝑚, 𝑘) → (𝑚 < 3 ↔ if(𝑆 = 0, 𝑚, 𝑘) < 3))
352 breq1 4891 . . . . . . . . . . . . . . . 16 (𝑘 = if(𝑆 = 0, 𝑚, 𝑘) → (𝑘 < 3 ↔ if(𝑆 = 0, 𝑚, 𝑘) < 3))
353351, 352ifboth 4345 . . . . . . . . . . . . . . 15 ((𝑚 < 3 ∧ 𝑘 < 3) → if(𝑆 = 0, 𝑚, 𝑘) < 3)
354340, 350, 353syl2anc 579 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) < 3)
355277rpred 12186 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ)
356 ltle 10467 . . . . . . . . . . . . . . . 16 ((if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ ∧ 3 ∈ ℝ) → (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3))
357355, 62, 356sylancl 580 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3))
358254, 357sylan 575 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3))
359354, 358mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3)
360 logleb 24797 . . . . . . . . . . . . . . 15 ((if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+ ∧ 3 ∈ ℝ+) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3)))
361277, 229, 360sylancl 580 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3)))
362254, 361sylan 575 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3)))
363359, 362mpbid 224 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3))
364231a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (log‘3) ∈ ℝ)
365278, 364, 276lediv1d 12232 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3) ↔ ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘)))
366254, 365sylan 575 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3) ↔ ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘)))
367363, 366mpbid 224 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘))
368333, 367eqbrtrd 4910 . . . . . . . . . 10 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ≤ ((log‘3) / 𝑘))
369 lemul2a 11235 . . . . . . . . . 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 1441 . . . . . . . . 9 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
371314, 370eqbrtrd 4910 . . . . . . . 8 (((𝜑𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
372285, 287, 312, 371fsumle 14944 . . . . . . 7 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
373269, 284, 263, 311, 372letrd 10535 . . . . . 6 ((𝜑𝑚 ∈ (1[,)3)) → Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
374260, 269, 263, 271, 373letrd 10535 . . . . 5 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)))
37526abscld 14590 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ)
376237adantr 474 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) ∈ ℝ)
377255abscld 14590 . . . . . . 7 ((𝜑𝑚 ∈ ℝ+) → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
378375, 376, 377leadd1d 10972 . . . . . 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 224 . . . 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 10535 . . 3 ((𝜑𝑚 ∈ (1[,)3)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))))
382381ralrimiva 3148 . 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 25657 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · (Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2107  wne 2969  wral 3090  wss 3792  ifcif 4307   class class class wbr 4888  cmpt 4967  wf 6133  cfv 6137  (class class class)co 6924  cc 10272  cr 10273  0cc0 10274  1c1 10275   + caddc 10277   · cmul 10279  +∞cpnf 10410  *cxr 10412   < clt 10413  cle 10414  cmin 10608   / cdiv 11035  cn 11379  2c2 11435  3c3 11436  cz 11733  cuz 11997  +crp 12142  [,)cico 12494  ...cfz 12648  cfl 12915  seqcseq 13124  abscabs 14387  cli 14632  𝑂(1)co1 14634  Σcsu 14833  Basecbs 16266  0gc0g 16497  ℤRHomczrh 20255  ℤ/nczn 20258  logclog 24749  μcmu 25284  DChrcdchr 25420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353  ax-mulf 10354
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-iin 4758  df-disj 4857  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-supp 7579  df-tpos 7636  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-omul 7850  df-er 8028  df-ec 8030  df-qs 8034  df-map 8144  df-pm 8145  df-ixp 8197  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-fsupp 8566  df-fi 8607  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-acn 9103  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11036  df-nn 11380  df-2 11443  df-3 11444  df-4 11445  df-5 11446  df-6 11447  df-7 11448  df-8 11449  df-9 11450  df-n0 11648  df-z 11734  df-dec 11851  df-uz 11998  df-q 12101  df-rp 12143  df-xneg 12262  df-xadd 12263  df-xmul 12264  df-ioo 12496  df-ioc 12497  df-ico 12498  df-icc 12499  df-fz 12649  df-fzo 12790  df-fl 12917  df-mod 12993  df-seq 13125  df-exp 13184  df-fac 13385  df-bc 13414  df-hash 13442  df-shft 14220  df-cj 14252  df-re 14253  df-im 14254  df-sqrt 14388  df-abs 14389  df-limsup 14619  df-clim 14636  df-rlim 14637  df-o1 14638  df-lo1 14639  df-sum 14834  df-ef 15209  df-e 15210  df-sin 15211  df-cos 15212  df-pi 15214  df-dvds 15397  df-prm 15801  df-struct 16268  df-ndx 16269  df-slot 16270  df-base 16272  df-sets 16273  df-ress 16274  df-plusg 16362  df-mulr 16363  df-starv 16364  df-sca 16365  df-vsca 16366  df-ip 16367  df-tset 16368  df-ple 16369  df-ds 16371  df-unif 16372  df-hom 16373  df-cco 16374  df-rest 16480  df-topn 16481  df-0g 16499  df-gsum 16500  df-topgen 16501  df-pt 16502  df-prds 16505  df-xrs 16559  df-qtop 16564  df-imas 16565  df-qus 16566  df-xps 16567  df-mre 16643  df-mrc 16644  df-acs 16646  df-mgm 17639  df-sgrp 17681  df-mnd 17692  df-mhm 17732  df-submnd 17733  df-grp 17823  df-minusg 17824  df-sbg 17825  df-mulg 17939  df-subg 17986  df-nsg 17987  df-eqg 17988  df-ghm 18053  df-cntz 18144  df-od 18343  df-cmn 18592  df-abl 18593  df-mgp 18888  df-ur 18900  df-ring 18947  df-cring 18948  df-oppr 19021  df-dvdsr 19039  df-unit 19040  df-invr 19070  df-dvr 19081  df-rnghom 19115  df-drng 19152  df-subrg 19181  df-lmod 19268  df-lss 19336  df-lsp 19378  df-sra 19580  df-rgmod 19581  df-lidl 19582  df-rsp 19583  df-2idl 19640  df-psmet 20145  df-xmet 20146  df-met 20147  df-bl 20148  df-mopn 20149  df-fbas 20150  df-fg 20151  df-cnfld 20154  df-zring 20226  df-zrh 20259  df-zn 20262  df-top 21117  df-topon 21134  df-topsp 21156  df-bases 21169  df-cld 21242  df-ntr 21243  df-cls 21244  df-nei 21321  df-lp 21359  df-perf 21360  df-cn 21450  df-cnp 21451  df-haus 21538  df-cmp 21610  df-tx 21785  df-hmeo 21978  df-fil 22069  df-fm 22161  df-flim 22162  df-flf 22163  df-xms 22544  df-ms 22545  df-tms 22546  df-cncf 23100  df-limc 24078  df-dv 24079  df-log 24751  df-cxp 24752  df-em 25182  df-mu 25290  df-dchr 25421
This theorem is referenced by:  dchrvmasumiflem2  25660
  Copyright terms: Public domain W3C validator