Metamath Proof Explorer

Theorem dchrvmasumiflem2

Description: Lemma for dchrvmasum . (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 dchrvmasumiflem2 
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) 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 1red 
 |-  ( ph -> 1 e. RR )
18 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
19 7 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
20 elfzelz 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. ZZ )
21 20 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. ZZ )
22 4 1 5 2 19 21 dchrzrhcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` d ) ) e. CC )
23 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN )
24 23 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN )
25 mucl 
 |-  ( d e. NN -> ( mmu ` d ) e. ZZ )
26 24 25 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. ZZ )
27 26 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. RR )
28 27 24 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. RR )
29 28 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. CC )
30 22 29 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC )
31 18 30 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC )
32 climcl 
 |-  ( seq 1 ( + , F ) ~~> S -> S e. CC )
33 11 32 syl 
 |-  ( ph -> S e. CC )
34 33 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> S e. CC )
35 31 34 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) e. CC )
36 0cnd 
 |-  ( ( ph /\ S = 0 ) -> 0 e. CC )
37 df-ne 
 |-  ( S =/= 0 <-> -. S = 0 )
38 climcl 
 |-  ( seq 1 ( + , K ) ~~> T -> T e. CC )
39 15 38 syl 
 |-  ( ph -> T e. CC )
40 39 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> T e. CC )
41 33 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> S e. CC )
42 simpr 
 |-  ( ( ph /\ S =/= 0 ) -> S =/= 0 )
43 40 41 42 divcld 
 |-  ( ( ph /\ S =/= 0 ) -> ( T / S ) e. CC )
44 37 43 sylan2br 
 |-  ( ( ph /\ -. S = 0 ) -> ( T / S ) e. CC )
45 36 44 ifclda 
 |-  ( ph -> if ( S = 0 , 0 , ( T / S ) ) e. CC )
46 45 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> if ( S = 0 , 0 , ( T / S ) ) e. CC )
47 1 2 3 4 5 6 7 8 9 10 11 12 dchrmusum2 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) ) e. O(1) )
48 rpssre 
 |-  RR+ C_ RR
49 o1const 
 |-  ( ( RR+ C_ RR /\ if ( S = 0 , 0 , ( T / S ) ) e. CC ) -> ( x e. RR+ |-> if ( S = 0 , 0 , ( T / S ) ) ) e. O(1) )
50 48 45 49 sylancr 
 |-  ( ph -> ( x e. RR+ |-> if ( S = 0 , 0 , ( T / S ) ) ) e. O(1) )
51 35 46 47 50 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) ) e. O(1) )
52 fzfid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / d ) ) ) e. Fin )
53 19 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> X e. D )
54 elfzelz 
 |-  ( k e. ( 1 ... ( |_ ` ( x / d ) ) ) -> k e. ZZ )
55 54 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> k e. ZZ )
56 4 1 5 2 53 55 dchrzrhcl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( X ` ( L ` k ) ) e. CC )
57 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
58 23 nnrpd 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. RR+ )
59 rpdivcl 
 |-  ( ( x e. RR+ /\ d e. RR+ ) -> ( x / d ) e. RR+ )
60 57 58 59 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR+ )
61 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( x / d ) ) ) -> k e. NN )
62 61 nnrpd 
 |-  ( k e. ( 1 ... ( |_ ` ( x / d ) ) ) -> k e. RR+ )
63 ifcl 
 |-  ( ( ( x / d ) e. RR+ /\ k e. RR+ ) -> if ( S = 0 , ( x / d ) , k ) e. RR+ )
64 60 62 63 syl2an 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> if ( S = 0 , ( x / d ) , k ) e. RR+ )
65 64 relogcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( log ` if ( S = 0 , ( x / d ) , k ) ) e. RR )
66 61 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> k e. NN )
67 65 66 nndivred 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( log ` if ( S = 0 , ( x / d ) , k ) ) / k ) e. RR )
68 67 recnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( log ` if ( S = 0 , ( x / d ) , k ) ) / k ) e. CC )
69 56 68 mulcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` k ) ) x. ( ( log ` if ( S = 0 , ( x / d ) , k ) ) / k ) ) e. CC )
70 52 69 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` k ) ) x. ( ( log ` if ( S = 0 , ( x / d ) , k ) ) / k ) ) e. CC )
71 30 70 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ 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 ) ) ) e. CC )
72 18 71 fsumcl 
 |-  ( ( 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 ) ) ) e. CC )
73 35 46 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) e. CC )
74 0cn 
 |-  0 e. CC
75 39 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> T e. CC )
76 ifcl 
 |-  ( ( 0 e. CC /\ T e. CC ) -> if ( S = 0 , 0 , T ) e. CC )
77 74 75 76 sylancr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> if ( S = 0 , 0 , T ) e. CC )
78 30 70 77 subdid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ 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 ) ) ) = ( ( ( ( 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 ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) ) )
79 78 sumeq2dv 
 |-  ( ( 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 ) ) ) = 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 ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) ) )
80 30 77 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) e. CC )
81 18 71 80 fsumsub 
 |-  ( ( 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 ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) ) = ( 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 ) ) ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) ) )
82 31 34 46 mulassd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( S x. if ( S = 0 , 0 , ( T / S ) ) ) ) )
83 ovif2 
 |-  ( S x. if ( S = 0 , 0 , ( T / S ) ) ) = if ( S = 0 , ( S x. 0 ) , ( S x. ( T / S ) ) )
84 33 mul01d 
 |-  ( ph -> ( S x. 0 ) = 0 )
85 84 ifeq1d 
 |-  ( ph -> if ( S = 0 , ( S x. 0 ) , ( S x. ( T / S ) ) ) = if ( S = 0 , 0 , ( S x. ( T / S ) ) ) )
86 40 41 42 divcan2d 
 |-  ( ( ph /\ S =/= 0 ) -> ( S x. ( T / S ) ) = T )
87 37 86 sylan2br 
 |-  ( ( ph /\ -. S = 0 ) -> ( S x. ( T / S ) ) = T )
88 87 ifeq2da 
 |-  ( ph -> if ( S = 0 , 0 , ( S x. ( T / S ) ) ) = if ( S = 0 , 0 , T ) )
89 85 88 eqtrd 
 |-  ( ph -> if ( S = 0 , ( S x. 0 ) , ( S x. ( T / S ) ) ) = if ( S = 0 , 0 , T ) )
90 83 89 eqtrid 
 |-  ( ph -> ( S x. if ( S = 0 , 0 , ( T / S ) ) ) = if ( S = 0 , 0 , T ) )
91 90 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( S x. if ( S = 0 , 0 , ( T / S ) ) ) = if ( S = 0 , 0 , T ) )
92 91 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( S x. if ( S = 0 , 0 , ( T / S ) ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) )
93 74 39 76 sylancr 
 |-  ( ph -> if ( S = 0 , 0 , T ) e. CC )
94 93 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> if ( S = 0 , 0 , T ) e. CC )
95 18 94 30 fsummulc1 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) )
96 82 92 95 3eqtrrd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) = ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) )
97 96 oveq2d 
 |-  ( ( 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 ) ) ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. if ( S = 0 , 0 , T ) ) ) = ( 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 ) ) ) - ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) ) )
98 79 81 97 3eqtrd 
 |-  ( ( 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 ) ) ) = ( 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 ) ) ) - ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) ) )
99 98 mpteq2dva 
 |-  ( 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 ) ) ) ) = ( 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 ) ) ) - ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) ) ) )
100 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 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) )
101 99 100 eqeltrrd 
 |-  ( 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 ) ) ) - ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) ) ) e. O(1) )
102 72 73 101 o1dif 
 |-  ( 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 ) ) ) ) e. O(1) <-> ( x e. RR+ |-> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. S ) x. if ( S = 0 , 0 , ( T / S ) ) ) ) e. O(1) ) )
103 51 102 mpbird 
 |-  ( 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 ) ) ) ) e. O(1) )
104 7 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
105 elfzelz 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
106 105 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. ZZ )
107 4 1 5 2 104 106 dchrzrhcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` n ) ) e. CC )
108 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
109 108 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
110 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
111 nndivre 
 |-  ( ( ( Lam ` n ) e. RR /\ n e. NN ) -> ( ( Lam ` n ) / n ) e. RR )
112 110 111 mpancom 
 |-  ( n e. NN -> ( ( Lam ` n ) / n ) e. RR )
113 109 112 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
114 113 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
115 107 114 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
116 18 115 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
117 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
118 117 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
119 118 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
120 ifcl 
 |-  ( ( ( log ` x ) e. CC /\ 0 e. CC ) -> if ( S = 0 , ( log ` x ) , 0 ) e. CC )
121 119 74 120 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> if ( S = 0 , ( log ` x ) , 0 ) e. CC )
122 116 121 addcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) e. CC )
123 122 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. RR )
124 123 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. RR )
125 3 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> N e. NN )
126 7 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> X e. D )
127 8 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> X =/= .1. )
128 simprl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ )
129 simprr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
130 1 2 125 4 5 6 126 127 128 129 dchrvmasum2if 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) = 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 ) ) ) )
131 130 fveq2d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) = ( abs ` 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 ) ) ) ) )
132 124 131 eqled 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) <_ ( abs ` 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 ) ) ) ) )
133 17 103 72 122 132 o1le 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )