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 ffvelcdm 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdm 
 |-  ( ( 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) )