Metamath Proof Explorer

Theorem rpvmasum2

Description: A partial result along the lines of rpvmasum . The sum of the von Mangoldt function over those integers n == A (mod N ) is asymptotic to ( 1 - M ) ( log x / phi ( x ) ) + O(1) , where M is the number of non-principal Dirichlet characters with sum_ n e. NN , X ( n ) / n = 0 . Our goal is to show this set is empty. Equation 9.4.3 of Shapiro, p. 375. (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 )
rpvmasum2.g 
|- G = ( DChr ` N )
rpvmasum2.d 
|- D = ( Base ` G )
rpvmasum2.1 
|- .1. = ( 0g ` G )
rpvmasum2.w 
|- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
rpvmasum2.u 
|- U = ( Unit ` Z )
rpvmasum2.b 
|- ( ph -> A e. U )
rpvmasum2.t 
|- T = ( `' L " { A } )
rpvmasum2.z1 
|- ( ( ph /\ f e. W ) -> A = ( 1r ` Z ) )
Assertion rpvmasum2 
|- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) 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 rpvmasum2.g 
 |-  G = ( DChr ` N )
5 rpvmasum2.d 
 |-  D = ( Base ` G )
6 rpvmasum2.1 
 |-  .1. = ( 0g ` G )
7 rpvmasum2.w 
 |-  W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
8 rpvmasum2.u 
 |-  U = ( Unit ` Z )
9 rpvmasum2.b 
 |-  ( ph -> A e. U )
10 rpvmasum2.t 
 |-  T = ( `' L " { A } )
11 rpvmasum2.z1 
 |-  ( ( ph /\ f e. W ) -> A = ( 1r ` Z ) )
12 3 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> N e. NN )
13 4 5 dchrfi 
 |-  ( N e. NN -> D e. Fin )
14 12 13 syl 
 |-  ( ( ph /\ x e. RR+ ) -> D e. Fin )
15 fzfid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
16 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
17 simpr 
 |-  ( ( ph /\ f e. D ) -> f e. D )
18 4 1 5 16 17 dchrf 
 |-  ( ( ph /\ f e. D ) -> f : ( Base ` Z ) --> CC )
19 16 8 unitss 
 |-  U C_ ( Base ` Z )
20 19 9 sselid 
 |-  ( ph -> A e. ( Base ` Z ) )
21 20 adantr 
 |-  ( ( ph /\ f e. D ) -> A e. ( Base ` Z ) )
22 18 21 ffvelrnd 
 |-  ( ( ph /\ f e. D ) -> ( f ` A ) e. CC )
23 22 cjcld 
 |-  ( ( ph /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
24 23 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
25 24 adantrl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( * ` ( f ` A ) ) e. CC )
26 18 ad4ant14 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
27 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
28 1 16 2 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
29 fof 
 |-  ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
30 27 28 29 3syl 
 |-  ( ph -> L : ZZ --> ( Base ` Z ) )
31 30 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> L : ZZ --> ( Base ` Z ) )
32 elfzelz 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
33 ffvelrn 
 |-  ( ( L : ZZ --> ( Base ` Z ) /\ n e. ZZ ) -> ( L ` n ) e. ( Base ` Z ) )
34 31 32 33 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` n ) e. ( Base ` Z ) )
35 34 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( L ` n ) e. ( Base ` Z ) )
36 26 35 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( f ` ( L ` n ) ) e. CC )
37 36 anasss 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( f ` ( L ` n ) ) e. CC )
38 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
39 38 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
40 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
41 39 40 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
42 41 39 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
43 42 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
44 43 adantrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( Lam ` n ) / n ) e. CC )
45 37 44 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
46 25 45 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) e. CC )
47 46 anass1rs 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) e. CC )
48 15 47 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) e. CC )
49 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
50 49 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
51 50 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
52 51 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( log ` x ) e. CC )
53 ax-1cn 
 |-  1 e. CC
54 neg1cn 
 |-  -u 1 e. CC
55 0cn 
 |-  0 e. CC
56 54 55 ifcli 
 |-  if ( f e. W , -u 1 , 0 ) e. CC
57 53 56 ifcli 
 |-  if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC
58 mulcl 
 |-  ( ( ( log ` x ) e. CC /\ if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC ) -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) e. CC )
59 52 57 58 sylancl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) e. CC )
60 14 48 59 fsumsub 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. D ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( sum_ f e. D sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) - sum_ f e. D ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
61 45 anass1rs 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
62 15 61 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
63 24 62 59 subdid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) = ( ( ( * ` ( f ` A ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) - ( ( * ` ( f ` A ) ) x. ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) )
64 15 24 61 fsummulc2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
65 57 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC )
66 24 52 65 mul12d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( ( log ` x ) x. ( ( * ` ( f ` A ) ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
67 ovif2 
 |-  ( ( * ` ( f ` A ) ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = if ( f = .1. , ( ( * ` ( f ` A ) ) x. 1 ) , ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) )
68 fveq1 
 |-  ( f = .1. -> ( f ` A ) = ( .1. ` A ) )
69 3 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> N e. NN )
70 9 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> A e. U )
71 4 1 6 8 69 70 dchr1 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( .1. ` A ) = 1 )
72 68 71 sylan9eqr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( f ` A ) = 1 )
73 72 fveq2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
74 1re 
 |-  1 e. RR
75 cjre 
 |-  ( 1 e. RR -> ( * ` 1 ) = 1 )
76 74 75 ax-mp 
 |-  ( * ` 1 ) = 1
77 73 76 eqtrdi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = 1 )
78 77 oveq1d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = ( 1 x. 1 ) )
79 1t1e1 
 |-  ( 1 x. 1 ) = 1
80 78 79 eqtrdi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = 1 )
81 df-ne 
 |-  ( f =/= .1. <-> -. f = .1. )
82 ovif2 
 |-  ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( * ` ( f ` A ) ) x. -u 1 ) , ( ( * ` ( f ` A ) ) x. 0 ) )
83 11 fveq2d 
 |-  ( ( ph /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
84 83 ad5ant15 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
85 4 1 5 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
86 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. D )
87 85 86 sselid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
88 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
89 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
90 88 89 ringidval 
 |-  ( 1r ` Z ) = ( 0g ` ( mulGrp ` Z ) )
91 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
92 cnfld1 
 |-  1 = ( 1r ` CCfld )
93 91 92 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
94 90 93 mhm0 
 |-  ( f e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> ( f ` ( 1r ` Z ) ) = 1 )
95 87 94 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` ( 1r ` Z ) ) = 1 )
96 95 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` ( 1r ` Z ) ) = 1 )
97 84 96 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = 1 )
98 97 fveq2d 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
99 98 76 eqtrdi 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = 1 )
100 99 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = ( 1 x. -u 1 ) )
101 54 mulid2i 
 |-  ( 1 x. -u 1 ) = -u 1
102 100 101 eqtrdi 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = -u 1 )
103 102 ifeq1da 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> if ( f e. W , ( ( * ` ( f ` A ) ) x. -u 1 ) , ( ( * ` ( f ` A ) ) x. 0 ) ) = if ( f e. W , -u 1 , ( ( * ` ( f ` A ) ) x. 0 ) ) )
104 24 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( * ` ( f ` A ) ) e. CC )
105 104 mul01d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( ( * ` ( f ` A ) ) x. 0 ) = 0 )
106 105 ifeq2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> if ( f e. W , -u 1 , ( ( * ` ( f ` A ) ) x. 0 ) ) = if ( f e. W , -u 1 , 0 ) )
107 103 106 eqtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> if ( f e. W , ( ( * ` ( f ` A ) ) x. -u 1 ) , ( ( * ` ( f ` A ) ) x. 0 ) ) = if ( f e. W , -u 1 , 0 ) )
108 82 107 eqtrid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
109 81 108 sylan2br 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ -. f = .1. ) -> ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
110 80 109 ifeq12da 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> if ( f = .1. , ( ( * ` ( f ` A ) ) x. 1 ) , ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) ) = if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) )
111 67 110 eqtrid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) )
112 111 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( log ` x ) x. ( ( * ` ( f ` A ) ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) )
113 66 112 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) )
114 64 113 oveq12d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( ( * ` ( f ` A ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) - ( ( * ` ( f ` A ) ) x. ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
115 63 114 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
116 115 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. D ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) = sum_ f e. D ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
117 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
118 inss1 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) )
119 ssfi 
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
120 117 118 119 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
121 12 phicld 
 |-  ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. NN )
122 121 nncnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. CC )
123 118 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) )
124 123 sselda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
125 124 43 syldan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( Lam ` n ) / n ) e. CC )
126 120 122 125 fsummulc2 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) = sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) )
127 122 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( phi ` N ) e. CC )
128 127 43 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) e. CC )
129 124 128 syldan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) e. CC )
130 129 ralrimiva 
 |-  ( ( ph /\ x e. RR+ ) -> A. n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) e. CC )
131 117 olcd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` x ) ) e. Fin ) )
132 sumss2 
 |-  ( ( ( ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) /\ A. n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) e. CC ) /\ ( ( 1 ... ( |_ ` x ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` x ) ) e. Fin ) ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) , 0 ) )
133 123 130 131 132 syl21anc 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) , 0 ) )
134 elin 
 |-  ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> ( n e. ( 1 ... ( |_ ` x ) ) /\ n e. T ) )
135 134 baib 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
136 135 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
137 10 eleq2i 
 |-  ( n e. T <-> n e. ( `' L " { A } ) )
138 31 ffnd 
 |-  ( ( ph /\ x e. RR+ ) -> L Fn ZZ )
139 fniniseg 
 |-  ( L Fn ZZ -> ( n e. ( `' L " { A } ) <-> ( n e. ZZ /\ ( L ` n ) = A ) ) )
140 139 baibd 
 |-  ( ( L Fn ZZ /\ n e. ZZ ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
141 138 32 140 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
142 137 141 syl5bb 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. T <-> ( L ` n ) = A ) )
143 136 142 bitr2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( L ` n ) = A <-> n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) )
144 43 mul02d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 x. ( ( Lam ` n ) / n ) ) = 0 )
145 143 144 ifbieq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> if ( ( L ` n ) = A , ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) , ( 0 x. ( ( Lam ` n ) / n ) ) ) = if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) , 0 ) )
146 ovif 
 |-  ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( ( Lam ` n ) / n ) ) = if ( ( L ` n ) = A , ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) , ( 0 x. ( ( Lam ` n ) / n ) ) )
147 3 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> N e. NN )
148 147 13 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> D e. Fin )
149 23 ad4ant14 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
150 36 149 mulcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) e. CC )
151 148 43 150 fsummulc1 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ f e. D ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( ( Lam ` n ) / n ) ) = sum_ f e. D ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( ( Lam ` n ) / n ) ) )
152 9 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. U )
153 4 5 1 16 8 147 34 152 sum2dchr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ f e. D ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) = if ( ( L ` n ) = A , ( phi ` N ) , 0 ) )
154 153 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ f e. D ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( ( Lam ` n ) / n ) ) = ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( ( Lam ` n ) / n ) ) )
155 43 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( ( Lam ` n ) / n ) e. CC )
156 mulass 
 |-  ( ( ( f ` ( L ` n ) ) e. CC /\ ( * ` ( f ` A ) ) e. CC /\ ( ( Lam ` n ) / n ) e. CC ) -> ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( ( Lam ` n ) / n ) ) = ( ( f ` ( L ` n ) ) x. ( ( * ` ( f ` A ) ) x. ( ( Lam ` n ) / n ) ) ) )
157 mul12 
 |-  ( ( ( f ` ( L ` n ) ) e. CC /\ ( * ` ( f ` A ) ) e. CC /\ ( ( Lam ` n ) / n ) e. CC ) -> ( ( f ` ( L ` n ) ) x. ( ( * ` ( f ` A ) ) x. ( ( Lam ` n ) / n ) ) ) = ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
158 156 157 eqtrd 
 |-  ( ( ( f ` ( L ` n ) ) e. CC /\ ( * ` ( f ` A ) ) e. CC /\ ( ( Lam ` n ) / n ) e. CC ) -> ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( ( Lam ` n ) / n ) ) = ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
159 36 149 155 158 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( ( Lam ` n ) / n ) ) = ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
160 159 sumeq2dv 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ f e. D ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( ( Lam ` n ) / n ) ) = sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
161 151 154 160 3eqtr3d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( ( Lam ` n ) / n ) ) = sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
162 146 161 eqtr3id 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> if ( ( L ` n ) = A , ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) , ( 0 x. ( ( Lam ` n ) / n ) ) ) = sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
163 145 162 eqtr3d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) , 0 ) = sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
164 163 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( ( Lam ` n ) / n ) ) , 0 ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
165 126 133 164 3eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
166 117 14 46 fsumcom 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) = sum_ f e. D sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
167 165 166 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) = sum_ f e. D sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
168 4 dchrabl 
 |-  ( N e. NN -> G e. Abel )
169 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
170 5 6 grpidcl 
 |-  ( G e. Grp -> .1. e. D )
171 12 168 169 170 4syl 
 |-  ( ( ph /\ x e. RR+ ) -> .1. e. D )
172 51 mulid1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
173 172 51 eqeltrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) e. CC )
174 iftrue 
 |-  ( f = .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = 1 )
175 174 oveq2d 
 |-  ( f = .1. -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. 1 ) )
176 175 sumsn 
 |-  ( ( .1. e. D /\ ( ( log ` x ) x. 1 ) e. CC ) -> sum_ f e. { .1. } ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. 1 ) )
177 171 173 176 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. { .1. } ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. 1 ) )
178 eldifsn 
 |-  ( f e. ( D \ { .1. } ) <-> ( f e. D /\ f =/= .1. ) )
179 ifnefalse 
 |-  ( f =/= .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
180 179 ad2antll 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
181 negeq 
 |-  ( if ( f e. W , 1 , 0 ) = 1 -> -u if ( f e. W , 1 , 0 ) = -u 1 )
182 negeq 
 |-  ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = -u 0 )
183 neg0 
 |-  -u 0 = 0
184 182 183 eqtrdi 
 |-  ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = 0 )
185 181 184 ifsb 
 |-  -u if ( f e. W , 1 , 0 ) = if ( f e. W , -u 1 , 0 )
186 180 185 eqtr4di 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = -u if ( f e. W , 1 , 0 ) )
187 186 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. -u if ( f e. W , 1 , 0 ) ) )
188 51 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( log ` x ) e. CC )
189 53 55 ifcli 
 |-  if ( f e. W , 1 , 0 ) e. CC
190 mulneg2 
 |-  ( ( ( log ` x ) e. CC /\ if ( f e. W , 1 , 0 ) e. CC ) -> ( ( log ` x ) x. -u if ( f e. W , 1 , 0 ) ) = -u ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) )
191 188 189 190 sylancl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( ( log ` x ) x. -u if ( f e. W , 1 , 0 ) ) = -u ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) )
192 187 191 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = -u ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) )
193 178 192 sylan2b 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = -u ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) )
194 193 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = sum_ f e. ( D \ { .1. } ) -u ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) )
195 diffi 
 |-  ( D e. Fin -> ( D \ { .1. } ) e. Fin )
196 14 195 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( D \ { .1. } ) e. Fin )
197 51 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( log ` x ) e. CC )
198 mulcl 
 |-  ( ( ( log ` x ) e. CC /\ if ( f e. W , 1 , 0 ) e. CC ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
199 197 189 198 sylancl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
200 196 199 fsumneg 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) -u ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) = -u sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) )
201 189 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> if ( f e. W , 1 , 0 ) e. CC )
202 196 51 201 fsummulc2 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) ) = sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) )
203 7 ssrab3 
 |-  W C_ ( D \ { .1. } )
204 difss 
 |-  ( D \ { .1. } ) C_ D
205 203 204 sstri 
 |-  W C_ D
206 ssfi 
 |-  ( ( D e. Fin /\ W C_ D ) -> W e. Fin )
207 14 205 206 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> W e. Fin )
208 fsumconst 
 |-  ( ( W e. Fin /\ 1 e. CC ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
209 207 53 208 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
210 203 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> W C_ ( D \ { .1. } ) )
211 53 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 1 e. CC )
212 211 ralrimivw 
 |-  ( ( ph /\ x e. RR+ ) -> A. f e. W 1 e. CC )
213 196 olcd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( D \ { .1. } ) C_ ( ZZ>= ` 1 ) \/ ( D \ { .1. } ) e. Fin ) )
214 sumss2 
 |-  ( ( ( W C_ ( D \ { .1. } ) /\ A. f e. W 1 e. CC ) /\ ( ( D \ { .1. } ) C_ ( ZZ>= ` 1 ) \/ ( D \ { .1. } ) e. Fin ) ) -> sum_ f e. W 1 = sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) )
215 210 212 213 214 syl21anc 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) )
216 hashcl 
 |-  ( W e. Fin -> ( # ` W ) e. NN0 )
217 207 216 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. NN0 )
218 217 nn0cnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. CC )
219 218 mulid1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( # ` W ) x. 1 ) = ( # ` W ) )
220 209 215 219 3eqtr3d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) = ( # ` W ) )
221 220 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
222 202 221 eqtr3d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
223 222 negeqd 
 |-  ( ( ph /\ x e. RR+ ) -> -u sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) = -u ( ( log ` x ) x. ( # ` W ) ) )
224 194 200 223 3eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = -u ( ( log ` x ) x. ( # ` W ) ) )
225 177 224 oveq12d 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ f e. { .1. } ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) + sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( ( ( log ` x ) x. 1 ) + -u ( ( log ` x ) x. ( # ` W ) ) ) )
226 51 218 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( # ` W ) ) e. CC )
227 173 226 negsubd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( log ` x ) x. 1 ) + -u ( ( log ` x ) x. ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
228 225 227 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ f e. { .1. } ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) + sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
229 disjdif 
 |-  ( { .1. } i^i ( D \ { .1. } ) ) = (/)
230 229 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> ( { .1. } i^i ( D \ { .1. } ) ) = (/) )
231 undif2 
 |-  ( { .1. } u. ( D \ { .1. } ) ) = ( { .1. } u. D )
232 171 snssd 
 |-  ( ( ph /\ x e. RR+ ) -> { .1. } C_ D )
233 ssequn1 
 |-  ( { .1. } C_ D <-> ( { .1. } u. D ) = D )
234 232 233 sylib 
 |-  ( ( ph /\ x e. RR+ ) -> ( { .1. } u. D ) = D )
235 231 234 eqtr2id 
 |-  ( ( ph /\ x e. RR+ ) -> D = ( { .1. } u. ( D \ { .1. } ) ) )
236 230 235 14 59 fsumsplit 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. D ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( sum_ f e. { .1. } ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) + sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
237 51 211 218 subdid 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
238 228 236 237 3eqtr4rd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) = sum_ f e. D ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) )
239 167 238 oveq12d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) = ( sum_ f e. D sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) - sum_ f e. D ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
240 60 116 239 3eqtr4d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ f e. D ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) = ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) )
241 240 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> sum_ f e. D ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) ) = ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) )
242 rpssre 
 |-  RR+ C_ RR
243 242 a1i 
 |-  ( ph -> RR+ C_ RR )
244 3 13 syl 
 |-  ( ph -> D e. Fin )
245 22 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` A ) e. CC )
246 245 cjcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
247 62 59 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) e. CC )
248 246 247 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) e. CC )
249 248 anasss 
 |-  ( ( ph /\ ( x e. RR+ /\ f e. D ) ) -> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) e. CC )
250 23 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( * ` ( f ` A ) ) e. CC )
251 247 an32s 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) e. CC )
252 o1const 
 |-  ( ( RR+ C_ RR /\ ( * ` ( f ` A ) ) e. CC ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O(1) )
253 242 23 252 sylancr 
 |-  ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O(1) )
254 fveq1 
 |-  ( f = .1. -> ( f ` ( L ` n ) ) = ( .1. ` ( L ` n ) ) )
255 254 oveq1d 
 |-  ( f = .1. -> ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) = ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) )
256 255 sumeq2sdv 
 |-  ( f = .1. -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) )
257 256 175 oveq12d 
 |-  ( f = .1. -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. 1 ) ) )
258 257 adantl 
 |-  ( ( ( ph /\ f e. D ) /\ f = .1. ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. 1 ) ) )
259 49 recnd 
 |-  ( x e. RR+ -> ( log ` x ) e. CC )
260 259 mulid1d 
 |-  ( x e. RR+ -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
261 260 oveq2d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. 1 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) )
262 258 261 sylan9eq 
 |-  ( ( ( ( ph /\ f e. D ) /\ f = .1. ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) )
263 262 mpteq2dva 
 |-  ( ( ( ph /\ f e. D ) /\ f = .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) )
264 1 2 3 4 5 6 rpvmasumlem 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
265 264 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ f = .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
266 263 265 eqeltrd 
 |-  ( ( ( ph /\ f e. D ) /\ f = .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) e. O(1) )
267 179 oveq2d 
 |-  ( f =/= .1. -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) )
268 267 oveq2d 
 |-  ( f =/= .1. -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) ) )
269 51 adantlr 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
270 mulcom 
 |-  ( ( ( log ` x ) e. CC /\ -u 1 e. CC ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
271 269 54 270 sylancl 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
272 269 mulm1d 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( -u 1 x. ( log ` x ) ) = -u ( log ` x ) )
273 271 272 eqtrd 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = -u ( log ` x ) )
274 269 mul01d 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. 0 ) = 0 )
275 273 274 ifeq12d 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> if ( f e. W , ( ( log ` x ) x. -u 1 ) , ( ( log ` x ) x. 0 ) ) = if ( f e. W , -u ( log ` x ) , 0 ) )
276 ovif2 
 |-  ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( log ` x ) x. -u 1 ) , ( ( log ` x ) x. 0 ) )
277 negeq 
 |-  ( if ( f e. W , ( log ` x ) , 0 ) = ( log ` x ) -> -u if ( f e. W , ( log ` x ) , 0 ) = -u ( log ` x ) )
278 negeq 
 |-  ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = -u 0 )
279 278 183 eqtrdi 
 |-  ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = 0 )
280 277 279 ifsb 
 |-  -u if ( f e. W , ( log ` x ) , 0 ) = if ( f e. W , -u ( log ` x ) , 0 )
281 275 276 280 3eqtr4g 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = -u if ( f e. W , ( log ` x ) , 0 ) )
282 281 oveq2d 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - -u if ( f e. W , ( log ` x ) , 0 ) ) )
283 62 an32s 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
284 ifcl 
 |-  ( ( ( log ` x ) e. CC /\ 0 e. CC ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
285 269 55 284 sylancl 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
286 283 285 subnegd 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - -u if ( f e. W , ( log ` x ) , 0 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) )
287 282 286 eqtrd 
 |-  ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) )
288 268 287 sylan9eqr 
 |-  ( ( ( ( ph /\ f e. D ) /\ x e. RR+ ) /\ f =/= .1. ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) )
289 288 an32s 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) )
290 289 mpteq2dva 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) )
291 3 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> N e. NN )
292 simplr 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f e. D )
293 simpr 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f =/= .1. )
294 eqid 
 |-  ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) = ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) )
295 1 2 291 4 5 6 292 293 294 dchrmusumlema 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) )
296 3 adantr 
 |-  ( ( ph /\ f e. D ) -> N e. NN )
297 296 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> N e. NN )
298 292 adantr 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> f e. D )
299 simplr 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> f =/= .1. )
300 simprl 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> c e. ( 0 [,) +oo ) )
301 simprrl 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t )
302 simprrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) )
303 1 2 297 4 5 6 298 299 294 300 301 302 7 dchrvmaeq0 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( f e. W <-> t = 0 ) )
304 ifbi 
 |-  ( ( f e. W <-> t = 0 ) -> if ( f e. W , ( log ` x ) , 0 ) = if ( t = 0 , ( log ` x ) , 0 ) )
305 304 oveq2d 
 |-  ( ( f e. W <-> t = 0 ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( t = 0 , ( log ` x ) , 0 ) ) )
306 305 mpteq2dv 
 |-  ( ( f e. W <-> t = 0 ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( t = 0 , ( log ` x ) , 0 ) ) ) )
307 303 306 syl 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( t = 0 , ( log ` x ) , 0 ) ) ) )
308 1 2 297 4 5 6 298 299 294 300 301 302 dchrvmasumif 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( t = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )
309 307 308 eqeltrd 
 |-  ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) e. O(1) )
310 309 rexlimdvaa 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) e. O(1) ) )
311 310 exlimdv 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) e. O(1) ) )
312 295 311 mpd 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) e. O(1) )
313 290 312 eqeltrd 
 |-  ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) e. O(1) )
314 266 313 pm2.61dane 
 |-  ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) e. O(1) )
315 250 251 253 314 o1mul2 
 |-  ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) ) e. O(1) )
316 243 244 249 315 fsumo1 
 |-  ( ph -> ( x e. RR+ |-> sum_ f e. D ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) ) e. O(1) )
317 241 316 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) e. O(1) )