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

Theorem dchrvmasumiflem1 26865
Description: Lemma for dchrvmasumif 26867. (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 13885 . . 3 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (1...(βŒŠβ€˜π‘š)) ∈ Fin)
10 simpl 484 . . . . 5 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ πœ‘)
11 elfznn 13477 . . . . 5 (π‘˜ ∈ (1...(βŒŠβ€˜π‘š)) β†’ π‘˜ ∈ β„•)
127adantr 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝑋 ∈ 𝐷)
13 nnz 12527 . . . . . . 7 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„€)
1413adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„€)
154, 1, 5, 2, 12, 14dchrzrhcl 26609 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘‹β€˜(πΏβ€˜π‘˜)) ∈ β„‚)
1610, 11, 15syl2an 597 . . . 4 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (π‘‹β€˜(πΏβ€˜π‘˜)) ∈ β„‚)
17 simpr 486 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ π‘š ∈ ℝ+)
1811nnrpd 12962 . . . . . . . 8 (π‘˜ ∈ (1...(βŒŠβ€˜π‘š)) β†’ π‘˜ ∈ ℝ+)
19 ifcl 4536 . . . . . . . 8 ((π‘š ∈ ℝ+ ∧ π‘˜ ∈ ℝ+) β†’ if(𝑆 = 0, π‘š, π‘˜) ∈ ℝ+)
2017, 18, 19syl2an 597 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ if(𝑆 = 0, π‘š, π‘˜) ∈ ℝ+)
2120relogcld 25994 . . . . . 6 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)) ∈ ℝ)
2211adantl 483 . . . . . 6 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ π‘˜ ∈ β„•)
2321, 22nndivred 12214 . . . . 5 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) ∈ ℝ)
2423recnd 11190 . . . 4 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) ∈ β„‚)
2516, 24mulcld 11182 . . 3 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) ∈ β„‚)
269, 25fsumcl 15625 . 2 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) ∈ β„‚)
27 fveq2 6847 . . . 4 (π‘š = (π‘₯ / 𝑑) β†’ (βŒŠβ€˜π‘š) = (βŒŠβ€˜(π‘₯ / 𝑑)))
2827oveq2d 7378 . . 3 (π‘š = (π‘₯ / 𝑑) β†’ (1...(βŒŠβ€˜π‘š)) = (1...(βŒŠβ€˜(π‘₯ / 𝑑))))
29 ifeq1 4495 . . . . . . 7 (π‘š = (π‘₯ / 𝑑) β†’ if(𝑆 = 0, π‘š, π‘˜) = if(𝑆 = 0, (π‘₯ / 𝑑), π‘˜))
3029fveq2d 6851 . . . . . 6 (π‘š = (π‘₯ / 𝑑) β†’ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)) = (logβ€˜if(𝑆 = 0, (π‘₯ / 𝑑), π‘˜)))
3130oveq1d 7377 . . . . 5 (π‘š = (π‘₯ / 𝑑) β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) = ((logβ€˜if(𝑆 = 0, (π‘₯ / 𝑑), π‘˜)) / π‘˜))
3231oveq2d 7378 . . . 4 (π‘š = (π‘₯ / 𝑑) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, (π‘₯ / 𝑑), π‘˜)) / π‘˜)))
3332adantr 482 . . 3 ((π‘š = (π‘₯ / 𝑑) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑑)))) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, (π‘₯ / 𝑑), π‘˜)) / π‘˜)))
3428, 33sumeq12rdv 15599 . 2 (π‘š = (π‘₯ / 𝑑) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑑)))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, (π‘₯ / 𝑑), π‘˜)) / π‘˜)))
35 dchrvmasumif.c . . 3 (πœ‘ β†’ 𝐢 ∈ (0[,)+∞))
36 dchrvmasumif.e . . 3 (πœ‘ β†’ 𝐸 ∈ (0[,)+∞))
3735, 36ifcld 4537 . 2 (πœ‘ β†’ if(𝑆 = 0, 𝐢, 𝐸) ∈ (0[,)+∞))
38 0cn 11154 . . 3 0 ∈ β„‚
39 dchrvmasumif.t . . . 4 (πœ‘ β†’ seq1( + , 𝐾) ⇝ 𝑇)
40 climcl 15388 . . . 4 (seq1( + , 𝐾) ⇝ 𝑇 β†’ 𝑇 ∈ β„‚)
4139, 40syl 17 . . 3 (πœ‘ β†’ 𝑇 ∈ β„‚)
42 ifcl 4536 . . 3 ((0 ∈ β„‚ ∧ 𝑇 ∈ β„‚) β†’ if(𝑆 = 0, 0, 𝑇) ∈ β„‚)
4338, 41, 42sylancr 588 . 2 (πœ‘ β†’ if(𝑆 = 0, 0, 𝑇) ∈ β„‚)
44 nnuz 12813 . . . . . . . . 9 β„• = (β„€β‰₯β€˜1)
45 1zzd 12541 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ β„€)
46 nncn 12168 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
4746adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„‚)
48 nnne0 12194 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• β†’ π‘˜ β‰  0)
4948adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ β‰  0)
5015, 47, 49divcld 11938 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜) ∈ β„‚)
51 dchrvmasumif.f . . . . . . . . . . . 12 𝐹 = (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))
52 2fveq3 6852 . . . . . . . . . . . . . 14 (π‘Ž = π‘˜ β†’ (π‘‹β€˜(πΏβ€˜π‘Ž)) = (π‘‹β€˜(πΏβ€˜π‘˜)))
53 id 22 . . . . . . . . . . . . . 14 (π‘Ž = π‘˜ β†’ π‘Ž = π‘˜)
5452, 53oveq12d 7380 . . . . . . . . . . . . 13 (π‘Ž = π‘˜ β†’ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž) = ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜))
5554cbvmptv 5223 . . . . . . . . . . . 12 (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)) = (π‘˜ ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜))
5651, 55eqtri 2765 . . . . . . . . . . 11 𝐹 = (π‘˜ ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜))
5750, 56fmptd 7067 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„•βŸΆβ„‚)
58 ffvelcdm 7037 . . . . . . . . . 10 ((𝐹:β„•βŸΆβ„‚ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ β„‚)
5957, 58sylan 581 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ β„‚)
6044, 45, 59serf 13943 . . . . . . . 8 (πœ‘ β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
6160ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
62 3re 12240 . . . . . . . . . . 11 3 ∈ ℝ
63 elicopnf 13369 . . . . . . . . . . 11 (3 ∈ ℝ β†’ (π‘š ∈ (3[,)+∞) ↔ (π‘š ∈ ℝ ∧ 3 ≀ π‘š)))
6462, 63mp1i 13 . . . . . . . . . 10 (πœ‘ β†’ (π‘š ∈ (3[,)+∞) ↔ (π‘š ∈ ℝ ∧ 3 ≀ π‘š)))
6564simprbda 500 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ π‘š ∈ ℝ)
66 1red 11163 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 1 ∈ ℝ)
6762a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 3 ∈ ℝ)
68 1le3 12372 . . . . . . . . . . 11 1 ≀ 3
6968a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 1 ≀ 3)
7064simplbda 501 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 3 ≀ π‘š)
7166, 67, 65, 69, 70letrd 11319 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 1 ≀ π‘š)
72 flge1nn 13733 . . . . . . . . 9 ((π‘š ∈ ℝ ∧ 1 ≀ π‘š) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
7365, 71, 72syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
7473adantr 482 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
7561, 74ffvelcdmd 7041 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) ∈ β„‚)
7675abscld 15328 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))) ∈ ℝ)
77 simpl 484 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ πœ‘)
78 0red 11165 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 0 ∈ ℝ)
79 3pos 12265 . . . . . . . . . . 11 0 < 3
8079a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 0 < 3)
8178, 67, 65, 80, 70ltletrd 11322 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 0 < π‘š)
8265, 81elrpd 12961 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ π‘š ∈ ℝ+)
8377, 82jca 513 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (πœ‘ ∧ π‘š ∈ ℝ+))
84 elrege0 13378 . . . . . . . . . 10 (𝐢 ∈ (0[,)+∞) ↔ (𝐢 ∈ ℝ ∧ 0 ≀ 𝐢))
8584simplbi 499 . . . . . . . . 9 (𝐢 ∈ (0[,)+∞) β†’ 𝐢 ∈ ℝ)
8635, 85syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐢 ∈ ℝ)
87 rerpdivcl 12952 . . . . . . . 8 ((𝐢 ∈ ℝ ∧ π‘š ∈ ℝ+) β†’ (𝐢 / π‘š) ∈ ℝ)
8886, 87sylan 581 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (𝐢 / π‘š) ∈ ℝ)
8983, 88syl 17 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (𝐢 / π‘š) ∈ ℝ)
9089adantr 482 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (𝐢 / π‘š) ∈ ℝ)
9182relogcld 25994 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (logβ€˜π‘š) ∈ ℝ)
9265, 71logge0d 26001 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ 0 ≀ (logβ€˜π‘š))
9391, 92jca 513 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ ((logβ€˜π‘š) ∈ ℝ ∧ 0 ≀ (logβ€˜π‘š)))
9493adantr 482 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ ((logβ€˜π‘š) ∈ ℝ ∧ 0 ≀ (logβ€˜π‘š)))
95 oveq2 7370 . . . . . . . 8 (𝑆 = 0 β†’ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑆) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 0))
9660adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
9796, 73ffvelcdmd 7041 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) ∈ β„‚)
9897subid1d 11508 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 0) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
9995, 98sylan9eqr 2799 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑆) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
10099fveq2d 6851 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑆)) = (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))))
101 2fveq3 6852 . . . . . . . . . 10 (𝑦 = π‘š β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘¦)) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
102101fvoveq1d 7384 . . . . . . . . 9 (𝑦 = π‘š β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑆)) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑆)))
103 oveq2 7370 . . . . . . . . 9 (𝑦 = π‘š β†’ (𝐢 / 𝑦) = (𝐢 / π‘š))
104102, 103breq12d 5123 . . . . . . . 8 (𝑦 = π‘š β†’ ((absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑆)) ≀ (𝐢 / 𝑦) ↔ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑆)) ≀ (𝐢 / π‘š)))
105 dchrvmasumif.1 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑆)) ≀ (𝐢 / 𝑦))
106105adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑆)) ≀ (𝐢 / 𝑦))
107 1re 11162 . . . . . . . . . 10 1 ∈ ℝ
108 elicopnf 13369 . . . . . . . . . 10 (1 ∈ ℝ β†’ (π‘š ∈ (1[,)+∞) ↔ (π‘š ∈ ℝ ∧ 1 ≀ π‘š)))
109107, 108ax-mp 5 . . . . . . . . 9 (π‘š ∈ (1[,)+∞) ↔ (π‘š ∈ ℝ ∧ 1 ≀ π‘š))
11065, 71, 109sylanbrc 584 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ π‘š ∈ (1[,)+∞))
111104, 106, 110rspcdva 3585 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑆)) ≀ (𝐢 / π‘š))
112111adantr 482 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑆)) ≀ (𝐢 / π‘š))
113100, 112eqbrtrrd 5134 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))) ≀ (𝐢 / π‘š))
114 lemul2a 12017 . . . . 5 ((((absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))) ∈ ℝ ∧ (𝐢 / π‘š) ∈ ℝ ∧ ((logβ€˜π‘š) ∈ ℝ ∧ 0 ≀ (logβ€˜π‘š))) ∧ (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))) ≀ (𝐢 / π‘š)) β†’ ((logβ€˜π‘š) Β· (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))) ≀ ((logβ€˜π‘š) Β· (𝐢 / π‘š)))
11576, 90, 94, 113, 114syl31anc 1374 . . . 4 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ ((logβ€˜π‘š) Β· (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))) ≀ ((logβ€˜π‘š) Β· (𝐢 / π‘š)))
116 iftrue 4497 . . . . . . . . . . . . . . 15 (𝑆 = 0 β†’ if(𝑆 = 0, π‘š, π‘˜) = π‘š)
117116fveq2d 6851 . . . . . . . . . . . . . 14 (𝑆 = 0 β†’ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)) = (logβ€˜π‘š))
118117oveq1d 7377 . . . . . . . . . . . . 13 (𝑆 = 0 β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) = ((logβ€˜π‘š) / π‘˜))
119118ad2antlr 726 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) = ((logβ€˜π‘š) / π‘˜))
120119oveq2d 7378 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘š) / π‘˜)))
12116adantlr 714 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (π‘‹β€˜(πΏβ€˜π‘˜)) ∈ β„‚)
122 relogcl 25947 . . . . . . . . . . . . . . 15 (π‘š ∈ ℝ+ β†’ (logβ€˜π‘š) ∈ ℝ)
123122adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (logβ€˜π‘š) ∈ ℝ)
124123recnd 11190 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (logβ€˜π‘š) ∈ β„‚)
125124ad2antrr 725 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (logβ€˜π‘š) ∈ β„‚)
12611adantl 483 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ π‘˜ ∈ β„•)
127126nncnd 12176 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ π‘˜ ∈ β„‚)
128126nnne0d 12210 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ π‘˜ β‰  0)
129121, 125, 127, 128div12d 11974 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘š) / π‘˜)) = ((logβ€˜π‘š) Β· ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)))
130120, 129eqtrd 2777 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = ((logβ€˜π‘š) Β· ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)))
131130sumeq2dv 15595 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((logβ€˜π‘š) Β· ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)))
132 iftrue 4497 . . . . . . . . . . 11 (𝑆 = 0 β†’ if(𝑆 = 0, 0, 𝑇) = 0)
133132oveq2d 7378 . . . . . . . . . 10 (𝑆 = 0 β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)) = (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ 0))
13426subid1d 11508 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ 0) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)))
135133, 134sylan9eqr 2799 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)))
136 ovex 7395 . . . . . . . . . . . . . 14 ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜) ∈ V
13754, 51, 136fvmpt 6953 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• β†’ (πΉβ€˜π‘˜) = ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜))
13822, 137syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (πΉβ€˜π‘˜) = ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜))
13957adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ 𝐹:β„•βŸΆβ„‚)
140139, 11, 58syl2an 597 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (πΉβ€˜π‘˜) ∈ β„‚)
141138, 140eqeltrrd 2839 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜) ∈ β„‚)
1429, 124, 141fsummulc2 15676 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ ((logβ€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((logβ€˜π‘š) Β· ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)))
143142adantr 482 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ ((logβ€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((logβ€˜π‘š) Β· ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)))
144131, 135, 1433eqtr4d 2787 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)) = ((logβ€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)))
14583, 144sylan 581 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)) = ((logβ€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)))
14683, 138sylan 581 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (πΉβ€˜π‘˜) = ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜))
14773, 44eleqtrdi 2848 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (βŒŠβ€˜π‘š) ∈ (β„€β‰₯β€˜1))
14877, 11, 50syl2an 597 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜) ∈ β„‚)
149146, 147, 148fsumser 15622 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
150149adantr 482 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
151150oveq2d 7378 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ ((logβ€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) / π‘˜)) = ((logβ€˜π‘š) Β· (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))))
152145, 151eqtrd 2777 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)) = ((logβ€˜π‘š) Β· (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))))
153152fveq2d 6851 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇))) = (absβ€˜((logβ€˜π‘š) Β· (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
154122ad2antlr 726 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ (logβ€˜π‘š) ∈ ℝ)
155154recnd 11190 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ (logβ€˜π‘š) ∈ β„‚)
15683, 155sylan 581 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (logβ€˜π‘š) ∈ β„‚)
157156, 75absmuld 15346 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (absβ€˜((logβ€˜π‘š) Β· (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))) = ((absβ€˜(logβ€˜π‘š)) Β· (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
15891, 92absidd 15314 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (absβ€˜(logβ€˜π‘š)) = (logβ€˜π‘š))
159158oveq1d 7377 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ ((absβ€˜(logβ€˜π‘š)) Β· (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))) = ((logβ€˜π‘š) Β· (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
160159adantr 482 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ ((absβ€˜(logβ€˜π‘š)) Β· (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))) = ((logβ€˜π‘š) Β· (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
161153, 157, 1603eqtrd 2781 . . . 4 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇))) = ((logβ€˜π‘š) Β· (absβ€˜(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
162 iftrue 4497 . . . . . . . 8 (𝑆 = 0 β†’ if(𝑆 = 0, 𝐢, 𝐸) = 𝐢)
163162adantl 483 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ if(𝑆 = 0, 𝐢, 𝐸) = 𝐢)
164163oveq1d 7377 . . . . . 6 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ (if(𝑆 = 0, 𝐢, 𝐸) Β· ((logβ€˜π‘š) / π‘š)) = (𝐢 Β· ((logβ€˜π‘š) / π‘š)))
16586recnd 11190 . . . . . . . 8 (πœ‘ β†’ 𝐢 ∈ β„‚)
166165ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ 𝐢 ∈ β„‚)
167 rpcnne0 12940 . . . . . . . 8 (π‘š ∈ ℝ+ β†’ (π‘š ∈ β„‚ ∧ π‘š β‰  0))
168167ad2antlr 726 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ (π‘š ∈ β„‚ ∧ π‘š β‰  0))
169 div12 11842 . . . . . . 7 ((𝐢 ∈ β„‚ ∧ (logβ€˜π‘š) ∈ β„‚ ∧ (π‘š ∈ β„‚ ∧ π‘š β‰  0)) β†’ (𝐢 Β· ((logβ€˜π‘š) / π‘š)) = ((logβ€˜π‘š) Β· (𝐢 / π‘š)))
170166, 155, 168, 169syl3anc 1372 . . . . . 6 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ (𝐢 Β· ((logβ€˜π‘š) / π‘š)) = ((logβ€˜π‘š) Β· (𝐢 / π‘š)))
171164, 170eqtrd 2777 . . . . 5 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ 𝑆 = 0) β†’ (if(𝑆 = 0, 𝐢, 𝐸) Β· ((logβ€˜π‘š) / π‘š)) = ((logβ€˜π‘š) Β· (𝐢 / π‘š)))
17283, 171sylan 581 . . . 4 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (if(𝑆 = 0, 𝐢, 𝐸) Β· ((logβ€˜π‘š) / π‘š)) = ((logβ€˜π‘š) Β· (𝐢 / π‘š)))
173115, 161, 1723brtr4d 5142 . . 3 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 = 0) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇))) ≀ (if(𝑆 = 0, 𝐢, 𝐸) Β· ((logβ€˜π‘š) / π‘š)))
174 dchrvmasumif.2 . . . . . 6 (πœ‘ β†’ βˆ€π‘¦ ∈ (3[,)+∞)(absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑇)) ≀ (𝐸 Β· ((logβ€˜π‘¦) / 𝑦)))
175 2fveq3 6852 . . . . . . . . 9 (𝑦 = π‘š β†’ (seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘¦)) = (seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)))
176175fvoveq1d 7384 . . . . . . . 8 (𝑦 = π‘š β†’ (absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑇)) = (absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑇)))
177 fveq2 6847 . . . . . . . . . 10 (𝑦 = π‘š β†’ (logβ€˜π‘¦) = (logβ€˜π‘š))
178 id 22 . . . . . . . . . 10 (𝑦 = π‘š β†’ 𝑦 = π‘š)
179177, 178oveq12d 7380 . . . . . . . . 9 (𝑦 = π‘š β†’ ((logβ€˜π‘¦) / 𝑦) = ((logβ€˜π‘š) / π‘š))
180179oveq2d 7378 . . . . . . . 8 (𝑦 = π‘š β†’ (𝐸 Β· ((logβ€˜π‘¦) / 𝑦)) = (𝐸 Β· ((logβ€˜π‘š) / π‘š)))
181176, 180breq12d 5123 . . . . . . 7 (𝑦 = π‘š β†’ ((absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑇)) ≀ (𝐸 Β· ((logβ€˜π‘¦) / 𝑦)) ↔ (absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑇)) ≀ (𝐸 Β· ((logβ€˜π‘š) / π‘š))))
182181rspccva 3583 . . . . . 6 ((βˆ€π‘¦ ∈ (3[,)+∞)(absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑇)) ≀ (𝐸 Β· ((logβ€˜π‘¦) / 𝑦)) ∧ π‘š ∈ (3[,)+∞)) β†’ (absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑇)) ≀ (𝐸 Β· ((logβ€˜π‘š) / π‘š)))
183174, 182sylan 581 . . . . 5 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑇)) ≀ (𝐸 Β· ((logβ€˜π‘š) / π‘š)))
184183adantr 482 . . . 4 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ (absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑇)) ≀ (𝐸 Β· ((logβ€˜π‘š) / π‘š)))
185 fveq2 6847 . . . . . . . . . . . 12 (π‘Ž = π‘˜ β†’ (logβ€˜π‘Ž) = (logβ€˜π‘˜))
186185, 53oveq12d 7380 . . . . . . . . . . 11 (π‘Ž = π‘˜ β†’ ((logβ€˜π‘Ž) / π‘Ž) = ((logβ€˜π‘˜) / π‘˜))
18752, 186oveq12d 7380 . . . . . . . . . 10 (π‘Ž = π‘˜ β†’ ((π‘‹β€˜(πΏβ€˜π‘Ž)) Β· ((logβ€˜π‘Ž) / π‘Ž)) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)))
188 dchrvmasumif.g . . . . . . . . . 10 𝐾 = (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) Β· ((logβ€˜π‘Ž) / π‘Ž)))
189 ovex 7395 . . . . . . . . . 10 ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)) ∈ V
190187, 188, 189fvmpt 6953 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ (πΎβ€˜π‘˜) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)))
19111, 190syl 17 . . . . . . . 8 (π‘˜ ∈ (1...(βŒŠβ€˜π‘š)) β†’ (πΎβ€˜π‘˜) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)))
192 ifnefalse 4503 . . . . . . . . . . . . 13 (𝑆 β‰  0 β†’ if(𝑆 = 0, π‘š, π‘˜) = π‘˜)
193192fveq2d 6851 . . . . . . . . . . . 12 (𝑆 β‰  0 β†’ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)) = (logβ€˜π‘˜))
194193oveq1d 7377 . . . . . . . . . . 11 (𝑆 β‰  0 β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) = ((logβ€˜π‘˜) / π‘˜))
195194oveq2d 7378 . . . . . . . . . 10 (𝑆 β‰  0 β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)))
196195adantl 483 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)))
197196eqcomd 2743 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)))
198191, 197sylan9eqr 2799 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (πΎβ€˜π‘˜) = ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)))
199147adantr 482 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ (βŒŠβ€˜π‘š) ∈ (β„€β‰₯β€˜1))
200 nnrp 12933 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ+)
201200adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ ℝ+)
202201relogcld 25994 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (logβ€˜π‘˜) ∈ ℝ)
203202recnd 11190 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (logβ€˜π‘˜) ∈ β„‚)
204203, 47, 49divcld 11938 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((logβ€˜π‘˜) / π‘˜) ∈ β„‚)
20515, 204mulcld 11182 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)) ∈ β„‚)
206187cbvmptv 5223 . . . . . . . . . . . 12 (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) Β· ((logβ€˜π‘Ž) / π‘Ž))) = (π‘˜ ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)))
207188, 206eqtri 2765 . . . . . . . . . . 11 𝐾 = (π‘˜ ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜π‘˜) / π‘˜)))
208205, 207fmptd 7067 . . . . . . . . . 10 (πœ‘ β†’ 𝐾:β„•βŸΆβ„‚)
209208ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ 𝐾:β„•βŸΆβ„‚)
210 ffvelcdm 7037 . . . . . . . . 9 ((𝐾:β„•βŸΆβ„‚ ∧ π‘˜ ∈ β„•) β†’ (πΎβ€˜π‘˜) ∈ β„‚)
211209, 11, 210syl2an 597 . . . . . . . 8 ((((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (πΎβ€˜π‘˜) ∈ β„‚)
212198, 211eqeltrrd 2839 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) ∈ β„‚)
213198, 199, 212fsumser 15622 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) = (seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)))
214 ifnefalse 4503 . . . . . . 7 (𝑆 β‰  0 β†’ if(𝑆 = 0, 0, 𝑇) = 𝑇)
215214adantl 483 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ if(𝑆 = 0, 0, 𝑇) = 𝑇)
216213, 215oveq12d 7380 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)) = ((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑇))
217216fveq2d 6851 . . . 4 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇))) = (absβ€˜((seq1( + , 𝐾)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑇)))
218 ifnefalse 4503 . . . . . 6 (𝑆 β‰  0 β†’ if(𝑆 = 0, 𝐢, 𝐸) = 𝐸)
219218adantl 483 . . . . 5 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ if(𝑆 = 0, 𝐢, 𝐸) = 𝐸)
220219oveq1d 7377 . . . 4 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ (if(𝑆 = 0, 𝐢, 𝐸) Β· ((logβ€˜π‘š) / π‘š)) = (𝐸 Β· ((logβ€˜π‘š) / π‘š)))
221184, 217, 2203brtr4d 5142 . . 3 (((πœ‘ ∧ π‘š ∈ (3[,)+∞)) ∧ 𝑆 β‰  0) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇))) ≀ (if(𝑆 = 0, 𝐢, 𝐸) Β· ((logβ€˜π‘š) / π‘š)))
222173, 221pm2.61dane 3033 . 2 ((πœ‘ ∧ π‘š ∈ (3[,)+∞)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇))) ≀ (if(𝑆 = 0, 𝐢, 𝐸) Β· ((logβ€˜π‘š) / π‘š)))
223 fzfid 13885 . . . 4 (πœ‘ β†’ (1...2) ∈ Fin)
2247adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (1...2)) β†’ 𝑋 ∈ 𝐷)
225 elfzelz 13448 . . . . . . . 8 (π‘˜ ∈ (1...2) β†’ π‘˜ ∈ β„€)
226225adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (1...2)) β†’ π‘˜ ∈ β„€)
2274, 1, 5, 2, 224, 226dchrzrhcl 26609 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (1...2)) β†’ (π‘‹β€˜(πΏβ€˜π‘˜)) ∈ β„‚)
228227abscld 15328 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (1...2)) β†’ (absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) ∈ ℝ)
229 3rp 12928 . . . . . . 7 3 ∈ ℝ+
230 relogcl 25947 . . . . . . 7 (3 ∈ ℝ+ β†’ (logβ€˜3) ∈ ℝ)
231229, 230ax-mp 5 . . . . . 6 (logβ€˜3) ∈ ℝ
232 elfznn 13477 . . . . . . 7 (π‘˜ ∈ (1...2) β†’ π‘˜ ∈ β„•)
233232adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (1...2)) β†’ π‘˜ ∈ β„•)
234 nndivre 12201 . . . . . 6 (((logβ€˜3) ∈ ℝ ∧ π‘˜ ∈ β„•) β†’ ((logβ€˜3) / π‘˜) ∈ ℝ)
235231, 233, 234sylancr 588 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (1...2)) β†’ ((logβ€˜3) / π‘˜) ∈ ℝ)
236228, 235remulcld 11192 . . . 4 ((πœ‘ ∧ π‘˜ ∈ (1...2)) β†’ ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)) ∈ ℝ)
237223, 236fsumrecl 15626 . . 3 (πœ‘ β†’ Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)) ∈ ℝ)
23843abscld 15328 . . 3 (πœ‘ β†’ (absβ€˜if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
239237, 238readdcld 11191 . 2 (πœ‘ β†’ (Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)) + (absβ€˜if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
240 simpl 484 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ πœ‘)
24162rexri 11220 . . . . . . . . . . 11 3 ∈ ℝ*
242 elico2 13335 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 3 ∈ ℝ*) β†’ (π‘š ∈ (1[,)3) ↔ (π‘š ∈ ℝ ∧ 1 ≀ π‘š ∧ π‘š < 3)))
243107, 241, 242mp2an 691 . . . . . . . . . 10 (π‘š ∈ (1[,)3) ↔ (π‘š ∈ ℝ ∧ 1 ≀ π‘š ∧ π‘š < 3))
244243simp1bi 1146 . . . . . . . . 9 (π‘š ∈ (1[,)3) β†’ π‘š ∈ ℝ)
245244adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ π‘š ∈ ℝ)
246 0red 11165 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ 0 ∈ ℝ)
247 1red 11163 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ 1 ∈ ℝ)
248 0lt1 11684 . . . . . . . . . 10 0 < 1
249248a1i 11 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ 0 < 1)
250243simp2bi 1147 . . . . . . . . . 10 (π‘š ∈ (1[,)3) β†’ 1 ≀ π‘š)
251250adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ 1 ≀ π‘š)
252246, 247, 245, 249, 251ltletrd 11322 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ 0 < π‘š)
253245, 252elrpd 12961 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ π‘š ∈ ℝ+)
254240, 253jca 513 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (πœ‘ ∧ π‘š ∈ ℝ+))
25543adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ if(𝑆 = 0, 0, 𝑇) ∈ β„‚)
25626, 255subcld 11519 . . . . . 6 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)) ∈ β„‚)
257254, 256syl 17 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)) ∈ β„‚)
258257abscld 15328 . . . 4 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
259254, 26syl 17 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) ∈ β„‚)
260259abscld 15328 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
261238adantr 482 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (absβ€˜if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
262260, 261readdcld 11191 . . . 4 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) + (absβ€˜if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
263237adantr 482 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)) ∈ ℝ)
264263, 261readdcld 11191 . . . 4 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)) + (absβ€˜if(𝑆 = 0, 0, 𝑇))) ∈ ℝ)
26526, 255abs2dif2d 15350 . . . . 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 15328 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘š))) β†’ (absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
2689, 267fsumrecl 15626 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))(absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
269254, 268syl 17 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))(absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
2709, 25fsumabs 15693 . . . . . . 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 13885 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (1...2) ∈ Fin)
273227adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (π‘‹β€˜(πΏβ€˜π‘˜)) ∈ β„‚)
27417adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ π‘š ∈ ℝ+)
275232adantl 483 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ π‘˜ ∈ β„•)
276275nnrpd 12962 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ π‘˜ ∈ ℝ+)
277274, 276ifcld 4537 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ if(𝑆 = 0, π‘š, π‘˜) ∈ ℝ+)
278277relogcld 25994 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)) ∈ ℝ)
279278, 275nndivred 12214 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) ∈ ℝ)
280279recnd 11190 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) ∈ β„‚)
281273, 280mulcld 11182 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) ∈ β„‚)
282281abscld 15328 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
283272, 282fsumrecl 15626 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ Ξ£π‘˜ ∈ (1...2)(absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
284254, 283syl 17 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ Ξ£π‘˜ ∈ (1...2)(absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
285 fzfid 13885 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (1...2) ∈ Fin)
286254, 281sylan 581 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ ((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) ∈ β„‚)
287286abscld 15328 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ (absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
288286absge0d 15336 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ 0 ≀ (absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))))
289245flcld 13710 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (βŒŠβ€˜π‘š) ∈ β„€)
290 2z 12542 . . . . . . . . . . 11 2 ∈ β„€
291290a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ 2 ∈ β„€)
292243simp3bi 1148 . . . . . . . . . . . . . 14 (π‘š ∈ (1[,)3) β†’ π‘š < 3)
293292adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ π‘š < 3)
294 3z 12543 . . . . . . . . . . . . . 14 3 ∈ β„€
295 fllt 13718 . . . . . . . . . . . . . 14 ((π‘š ∈ ℝ ∧ 3 ∈ β„€) β†’ (π‘š < 3 ↔ (βŒŠβ€˜π‘š) < 3))
296245, 294, 295sylancl 587 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (π‘š < 3 ↔ (βŒŠβ€˜π‘š) < 3))
297293, 296mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (βŒŠβ€˜π‘š) < 3)
298 df-3 12224 . . . . . . . . . . . 12 3 = (2 + 1)
299297, 298breqtrdi 5151 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (βŒŠβ€˜π‘š) < (2 + 1))
300 rpre 12930 . . . . . . . . . . . . . . 15 (π‘š ∈ ℝ+ β†’ π‘š ∈ ℝ)
301300adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ π‘š ∈ ℝ)
302301flcld 13710 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (βŒŠβ€˜π‘š) ∈ β„€)
303 zleltp1 12561 . . . . . . . . . . . . 13 (((βŒŠβ€˜π‘š) ∈ β„€ ∧ 2 ∈ β„€) β†’ ((βŒŠβ€˜π‘š) ≀ 2 ↔ (βŒŠβ€˜π‘š) < (2 + 1)))
304302, 290, 303sylancl 587 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ ((βŒŠβ€˜π‘š) ≀ 2 ↔ (βŒŠβ€˜π‘š) < (2 + 1)))
305254, 304syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ ((βŒŠβ€˜π‘š) ≀ 2 ↔ (βŒŠβ€˜π‘š) < (2 + 1)))
306299, 305mpbird 257 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (βŒŠβ€˜π‘š) ≀ 2)
307 eluz2 12776 . . . . . . . . . 10 (2 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š)) ↔ ((βŒŠβ€˜π‘š) ∈ β„€ ∧ 2 ∈ β„€ ∧ (βŒŠβ€˜π‘š) ≀ 2))
308289, 291, 306, 307syl3anbrc 1344 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ 2 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š)))
309 fzss2 13488 . . . . . . . . 9 (2 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š)) β†’ (1...(βŒŠβ€˜π‘š)) βŠ† (1...2))
310308, 309syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (1...(βŒŠβ€˜π‘š)) βŠ† (1...2))
311285, 287, 288, 310fsumless 15688 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))(absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ≀ Ξ£π‘˜ ∈ (1...2)(absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))))
312236adantlr 714 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)) ∈ ℝ)
313273, 280absmuld 15346 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) = ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· (absβ€˜((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))))
314254, 313sylan 581 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ (absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) = ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· (absβ€˜((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))))
315254, 279sylan 581 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) ∈ ℝ)
316254, 278sylan 581 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)) ∈ ℝ)
317 log1 25957 . . . . . . . . . . . . . 14 (logβ€˜1) = 0
318 elfzle1 13451 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ (1...2) β†’ 1 ≀ π‘˜)
319 breq2 5114 . . . . . . . . . . . . . . . . 17 (π‘š = if(𝑆 = 0, π‘š, π‘˜) β†’ (1 ≀ π‘š ↔ 1 ≀ if(𝑆 = 0, π‘š, π‘˜)))
320 breq2 5114 . . . . . . . . . . . . . . . . 17 (π‘˜ = if(𝑆 = 0, π‘š, π‘˜) β†’ (1 ≀ π‘˜ ↔ 1 ≀ if(𝑆 = 0, π‘š, π‘˜)))
321319, 320ifboth 4530 . . . . . . . . . . . . . . . 16 ((1 ≀ π‘š ∧ 1 ≀ π‘˜) β†’ 1 ≀ if(𝑆 = 0, π‘š, π‘˜))
322251, 318, 321syl2an 597 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ 1 ≀ if(𝑆 = 0, π‘š, π‘˜))
323 1rp 12926 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ+
324 logleb 25974 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ+ ∧ if(𝑆 = 0, π‘š, π‘˜) ∈ ℝ+) β†’ (1 ≀ if(𝑆 = 0, π‘š, π‘˜) ↔ (logβ€˜1) ≀ (logβ€˜if(𝑆 = 0, π‘š, π‘˜))))
325323, 277, 324sylancr 588 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (1 ≀ if(𝑆 = 0, π‘š, π‘˜) ↔ (logβ€˜1) ≀ (logβ€˜if(𝑆 = 0, π‘š, π‘˜))))
326254, 325sylan 581 . . . . . . . . . . . . . . 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 5146 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ 0 ≀ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)))
329276rpregt0d 12970 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (π‘˜ ∈ ℝ ∧ 0 < π‘˜))
330254, 329sylan 581 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ (π‘˜ ∈ ℝ ∧ 0 < π‘˜))
331 divge0 12031 . . . . . . . . . . . . 13 ((((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) ∈ ℝ ∧ 0 ≀ (logβ€˜if(𝑆 = 0, π‘š, π‘˜))) ∧ (π‘˜ ∈ ℝ ∧ 0 < π‘˜)) β†’ 0 ≀ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))
332316, 328, 330, 331syl21anc 837 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ 0 ≀ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))
333315, 332absidd 15314 . . . . . . . . . . 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 714 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ ((logβ€˜3) / π‘˜) ∈ ℝ)
336228adantlr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) ∈ ℝ)
337273absge0d 15336 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ 0 ≀ (absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))))
338336, 337jca 513 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) ∈ ℝ ∧ 0 ≀ (absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜)))))
339254, 338sylan 581 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) ∈ ℝ ∧ 0 ≀ (absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜)))))
340292ad2antlr 726 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ π‘š < 3)
341275nnred 12175 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ π‘˜ ∈ ℝ)
342 2re 12234 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
343342a1i 11 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ 2 ∈ ℝ)
34462a1i 11 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ 3 ∈ ℝ)
345 elfzle2 13452 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ (1...2) β†’ π‘˜ ≀ 2)
346345adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ π‘˜ ≀ 2)
347 2lt3 12332 . . . . . . . . . . . . . . . . . 18 2 < 3
348347a1i 11 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ 2 < 3)
349341, 343, 344, 346, 348lelttrd 11320 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ π‘˜ < 3)
350254, 349sylan 581 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ π‘˜ < 3)
351 breq1 5113 . . . . . . . . . . . . . . . 16 (π‘š = if(𝑆 = 0, π‘š, π‘˜) β†’ (π‘š < 3 ↔ if(𝑆 = 0, π‘š, π‘˜) < 3))
352 breq1 5113 . . . . . . . . . . . . . . . 16 (π‘˜ = if(𝑆 = 0, π‘š, π‘˜) β†’ (π‘˜ < 3 ↔ if(𝑆 = 0, π‘š, π‘˜) < 3))
353351, 352ifboth 4530 . . . . . . . . . . . . . . 15 ((π‘š < 3 ∧ π‘˜ < 3) β†’ if(𝑆 = 0, π‘š, π‘˜) < 3)
354340, 350, 353syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ if(𝑆 = 0, π‘š, π‘˜) < 3)
355277rpred 12964 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ if(𝑆 = 0, π‘š, π‘˜) ∈ ℝ)
356 ltle 11250 . . . . . . . . . . . . . . . 16 ((if(𝑆 = 0, π‘š, π‘˜) ∈ ℝ ∧ 3 ∈ ℝ) β†’ (if(𝑆 = 0, π‘š, π‘˜) < 3 β†’ if(𝑆 = 0, π‘š, π‘˜) ≀ 3))
357355, 62, 356sylancl 587 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (if(𝑆 = 0, π‘š, π‘˜) < 3 β†’ if(𝑆 = 0, π‘š, π‘˜) ≀ 3))
358254, 357sylan 581 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ (if(𝑆 = 0, π‘š, π‘˜) < 3 β†’ if(𝑆 = 0, π‘š, π‘˜) ≀ 3))
359354, 358mpd 15 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ if(𝑆 = 0, π‘š, π‘˜) ≀ 3)
360 logleb 25974 . . . . . . . . . . . . . . 15 ((if(𝑆 = 0, π‘š, π‘˜) ∈ ℝ+ ∧ 3 ∈ ℝ+) β†’ (if(𝑆 = 0, π‘š, π‘˜) ≀ 3 ↔ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)) ≀ (logβ€˜3)))
361277, 229, 360sylancl 587 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ (if(𝑆 = 0, π‘š, π‘˜) ≀ 3 ↔ (logβ€˜if(𝑆 = 0, π‘š, π‘˜)) ≀ (logβ€˜3)))
362254, 361sylan 581 . . . . . . . . . . . . 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 13010 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ ℝ+) ∧ π‘˜ ∈ (1...2)) β†’ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) ≀ (logβ€˜3) ↔ ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜) ≀ ((logβ€˜3) / π‘˜)))
366254, 365sylan 581 . . . . . . . . . . . 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 5132 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ (absβ€˜((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) ≀ ((logβ€˜3) / π‘˜))
369 lemul2a 12017 . . . . . . . . . 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 1374 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· (absβ€˜((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ≀ ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)))
371314, 370eqbrtrd 5132 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (1[,)3)) ∧ π‘˜ ∈ (1...2)) β†’ (absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ≀ ((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)))
372285, 287, 312, 371fsumle 15691 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ Ξ£π‘˜ ∈ (1...2)(absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ≀ Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)))
373269, 284, 263, 311, 372letrd 11319 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))(absβ€˜((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ≀ Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)))
374260, 269, 263, 271, 373letrd 11319 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ≀ Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)))
37526abscld 15328 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜))) ∈ ℝ)
376237adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)) ∈ ℝ)
377255abscld 15328 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ (absβ€˜if(𝑆 = 0, 0, 𝑇)) ∈ ℝ)
378375, 376, 377leadd1d 11756 . . . . . 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 11319 . . 3 ((πœ‘ ∧ π‘š ∈ (1[,)3)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘š))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, π‘š, π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇))) ≀ (Ξ£π‘˜ ∈ (1...2)((absβ€˜(π‘‹β€˜(πΏβ€˜π‘˜))) Β· ((logβ€˜3) / π‘˜)) + (absβ€˜if(𝑆 = 0, 0, 𝑇))))
382381ralrimiva 3144 . 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 26863 1 (πœ‘ β†’ (π‘₯ ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(βŒŠβ€˜π‘₯))(((π‘‹β€˜(πΏβ€˜π‘‘)) Β· ((ΞΌβ€˜π‘‘) / 𝑑)) Β· (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑑)))((π‘‹β€˜(πΏβ€˜π‘˜)) Β· ((logβ€˜if(𝑆 = 0, (π‘₯ / 𝑑), π‘˜)) / π‘˜)) βˆ’ if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065   βŠ† wss 3915  ifcif 4491   class class class wbr 5110   ↦ cmpt 5193  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392   / cdiv 11819  β„•cn 12160  2c2 12215  3c3 12216  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  [,)cico 13273  ...cfz 13431  βŒŠcfl 13702  seqcseq 13913  abscabs 15126   ⇝ cli 15373  π‘‚(1)co1 15375  Ξ£csu 15577  Basecbs 17090  0gc0g 17328  β„€RHomczrh 20916  β„€/nβ„€czn 20919  logclog 25926  ΞΌcmu 26460  DChrcdchr 26596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-disj 5076  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-tpos 8162  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-er 8655  df-ec 8657  df-qs 8661  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-acn 9885  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-xnn0 12493  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-o1 15379  df-lo1 15380  df-sum 15578  df-ef 15957  df-e 15958  df-sin 15959  df-cos 15960  df-tan 15961  df-pi 15962  df-dvds 16144  df-prm 16555  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-qus 17398  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-mhm 18608  df-submnd 18609  df-grp 18758  df-minusg 18759  df-sbg 18760  df-mulg 18880  df-subg 18932  df-nsg 18933  df-eqg 18934  df-ghm 19013  df-cntz 19104  df-od 19317  df-cmn 19571  df-abl 19572  df-mgp 19904  df-ur 19921  df-ring 19973  df-cring 19974  df-oppr 20056  df-dvdsr 20077  df-unit 20078  df-invr 20108  df-dvr 20119  df-rnghom 20155  df-drng 20201  df-subrg 20236  df-lmod 20340  df-lss 20409  df-lsp 20449  df-sra 20649  df-rgmod 20650  df-lidl 20651  df-rsp 20652  df-2idl 20718  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-zring 20886  df-zrh 20920  df-zn 20923  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-ulm 25752  df-log 25928  df-cxp 25929  df-atan 26233  df-em 26358  df-mu 26466  df-dchr 26597
This theorem is referenced by:  dchrvmasumiflem2  26866
  Copyright terms: Public domain W3C validator