Metamath Proof Explorer


Theorem dchrvmasumiflem1

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

Ref Expression
Hypotheses rpvmasum.z
|- Z = ( Z/nZ ` N )
rpvmasum.l
|- L = ( ZRHom ` Z )
rpvmasum.a
|- ( ph -> N e. NN )
rpvmasum.g
|- G = ( DChr ` N )
rpvmasum.d
|- D = ( Base ` G )
rpvmasum.1
|- .1. = ( 0g ` G )
dchrisum.b
|- ( ph -> X e. D )
dchrisum.n1
|- ( ph -> X =/= .1. )
dchrvmasumif.f
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
dchrvmasumif.c
|- ( ph -> C e. ( 0 [,) +oo ) )
dchrvmasumif.s
|- ( ph -> seq 1 ( + , F ) ~~> S )
dchrvmasumif.1
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )
dchrvmasumif.g
|- K = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) )
dchrvmasumif.e
|- ( ph -> E e. ( 0 [,) +oo ) )
dchrvmasumif.t
|- ( ph -> seq 1 ( + , K ) ~~> T )
dchrvmasumif.2
|- ( ph -> A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E x. ( ( log ` y ) / y ) ) )
Assertion dchrvmasumiflem1
|- ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( sum_ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` k ) ) x. ( ( log ` if ( S = 0 , ( x / d ) , k ) ) / k ) ) - if ( S = 0 , 0 , T ) ) ) ) e. O(1) )

Proof

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