Theorem rpvmasum2 20609

Description: A partial result along the lines of rpvmasum 20623. 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.)

Hypotheses

Ref	Expression
rpvmasum.z	|- Z = (ℤ/nℤ ` 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

Ref	Expression
rpvmasum2	|- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) e. O ( 1 ) )

Distinct variable groups:   m, n, x, y, f, .1.   A, f, m, x, y   f, G   f, N, m, n, x, y   ph, f, m, n, x   T, m, n, x, y   U, m, n, x   f, W, x   f, Z, m, n, x, y   D, f, m, n, x, y   f, L, m, n, x, y   A, n

Allowed substitution hints:   ph( y)   T( f)   U( y, f)   G( x, y, m, n)   W( y, m, n)

Proof of Theorem rpvmasum2

Step	Hyp	Ref	Expression
1		rpvmasum.a	. . . . . . 7 |- ( ph -> N e. NN )
2	1	adantr 453	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> N e. NN )
3		rpvmasum2.g	. . . . . . 7 |- G = (DChr ` N )
4		rpvmasum2.d	. . . . . . 7 |- D = ( Base ` G )
5	3, 4	dchrfi 20442	. . . . . 6 |- ( N e. NN -> D e. Fin )
6	2, 5	syl 17	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> D e. Fin )
7		fzfid 10987	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
8		rpvmasum.z	. . . . . . . . . . . . 13 |- Z = (ℤ/nℤ ` N )
9		eqid 2256	. . . . . . . . . . . . 13 |- ( Base ` Z ) = ( Base ` Z )
10		simpr 449	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> f e. D )
11	3, 8, 4, 9, 10	dchrf 20429	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> f : ( Base ` Z ) --> CC )
12		rpvmasum2.u	. . . . . . . . . . . . . . 15 |- U = (Unit ` Z )
13	9, 12	unitss 15390	. . . . . . . . . . . . . 14 |- U C_ ( Base ` Z )
14		rpvmasum2.b	. . . . . . . . . . . . . 14 |- ( ph -> A e. U )
15	13, 14	sseldi 3139	. . . . . . . . . . . . 13 |- ( ph -> A e. ( Base ` Z ) )
16	15	adantr 453	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> A e. ( Base ` Z ) )
17		ffvelrn 5583	. . . . . . . . . . . 12 |- ( ( f : ( Base ` Z ) --> CC /\ A e. ( Base ` Z ) ) -> ( f ` A ) e. CC )
18	11, 16, 17	syl2anc 645	. . . . . . . . . . 11 |- ( ( ph /\ f e. D ) -> ( f ` A ) e. CC )
19	18	cjcld 11632	. . . . . . . . . 10 |- ( ( ph /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
20	19	adantlr 698	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
21	20	adantrl 699	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( * ` ( f ` A ) ) e. CC )
22	11	adantlr 698	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
23	22	adantlr 698	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
24	1	nnnn0d 9971	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
25		rpvmasum.l	. . . . . . . . . . . . . . . 16 |- L = ( ZRHom ` Z )
26	8, 9, 25	znzrhfo 16449	. . . . . . . . . . . . . . 15 |- ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
27		fof 5375	. . . . . . . . . . . . . . 15 |- ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
28	24, 26, 27	3syl 20	. . . . . . . . . . . . . 14 |- ( ph -> L : ZZ --> ( Base ` Z ) )
29	28	adantr 453	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L : ZZ --> ( Base ` Z ) )
30		elfzelz 10750	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
31		ffvelrn 5583	. . . . . . . . . . . . 13 |- ( ( L : ZZ --> ( Base ` Z ) /\ n e. ZZ ) -> ( L ` n ) e. ( Base ` Z ) )
32	29, 30, 31	syl2an 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` n ) e. ( Base ` Z ) )
33	32	adantr 453	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( L ` n ) e. ( Base ` Z ) )
34		ffvelrn 5583	. . . . . . . . . . 11 |- ( ( f : ( Base ` Z ) --> CC /\ ( L ` n ) e. ( Base ` Z ) ) -> ( f ` ( L ` n ) ) e. CC )
35	23, 33, 34	syl2anc 645	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( f ` ( L ` n ) ) e. CC )
36	35	anasss 631	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( f ` ( L ` n ) ) e. CC )
37		elfznn 10771	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
38	37	adantl 454	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
39		vmacl 20304	. . . . . . . . . . . . 13 |- ( n e. NN -> (Λ ` n ) e. RR )
40	38, 39	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (Λ ` n ) e. RR )
41	40, 38	nndivred 9748	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. RR )
42	41	recnd 8815	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. CC )
43	42	adantrr 700	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( (Λ ` n ) / n ) e. CC )
44	36, 43	mulcld 8809	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
45	21, 44	mulcld 8809	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) e. CC )
46	45	anass1rs 785	. . . . . 6 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) e. CC )
47	7, 46	fsumcl 12157	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) e. CC )
48		relogcl 19880	. . . . . . . . 9 |- ( x e. RR+ -> ( log ` x ) e. RR )
49	48	adantl 454	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
50	49	recnd 8815	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
51	50	adantr 453	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( log ` x ) e. CC )
52		ax-1cn 8749	. . . . . . 7 |- 1 e. CC
53		neg1cn 9767	. . . . . . . 8 |- -u 1 e. CC
54		0cn 8785	. . . . . . . 8 |- 0 e. CC
55	53, 54	keepel 3582	. . . . . . 7 |- if ( f e. W , -u 1 , 0 ) e. CC
56	52, 55	keepel 3582	. . . . . 6 |- if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC
57		mulcl 8775	. . . . . 6 |- ( ( ( 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 )
58	51, 56, 57	sylancl 646	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) e. CC )
59	6, 47, 58	fsumsub 12201	. . . 4 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. D ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) ) - sum_ f e. D ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
60	44	anass1rs 785	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
61	7, 60	fsumcl 12157	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
62	20, 61, 58	subdid 9189	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) ) - ( ( * ` ( f ` A ) ) x. ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) )
63	7, 20, 60	fsummulc2 12197	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
64	56	a1i 12	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC )
65	20, 51, 64	mul12d 8975	. . . . . . . 8 |- ( ( ( 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 ) ) ) ) )
66		oveq2 5786	. . . . . . . . . . 11 |- ( if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = 1 -> ( ( * ` ( f ` A ) ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( * ` ( f ` A ) ) x. 1 ) )
67		oveq2 5786	. . . . . . . . . . 11 |- ( if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) -> ( ( * ` ( f ` A ) ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) )
68	66, 67	ifsb 3534	. . . . . . . . . 10 |- ( ( * ` ( 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 ) ) )
69		fveq1 5443	. . . . . . . . . . . . . . . . 17 |- ( f = .1. -> ( f ` A ) = ( .1. ` A ) )
70		rpvmasum2.1	. . . . . . . . . . . . . . . . . 18 |- .1. = ( 0g ` G )
71	1	ad2antrr 709	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> N e. NN )
72	14	ad2antrr 709	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> A e. U )
73	3, 8, 70, 12, 71, 72	dchr1 20444	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( .1. ` A ) = 1 )
74	69, 73	sylan9eqr 2310	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( f ` A ) = 1 )
75	74	fveq2d 5448	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
76		1re 8791	. . . . . . . . . . . . . . . 16 |- 1 e. RR
77		cjre 11575	. . . . . . . . . . . . . . . 16 |- ( 1 e. RR -> ( * ` 1 ) = 1 )
78	76, 77	ax-mp 10	. . . . . . . . . . . . . . 15 |- ( * ` 1 ) = 1
79	75, 78	syl6eq 2304	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = 1 )
80	79	oveq1d 5793	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = ( 1 x. 1 ) )
81		1t1e1 9823	. . . . . . . . . . . . 13 |- ( 1 x. 1 ) = 1
82	80, 81	syl6eq 2304	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = 1 )
83	82	ifeq1da 3550	. . . . . . . . . . 11 |- ( ( ( 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 , ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) ) )
84		df-ne 2421	. . . . . . . . . . . . 13 |- ( f =/= .1. <-> -. f = .1. )
85		oveq2 5786	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , -u 1 , 0 ) = -u 1 -> ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = ( ( * ` ( f ` A ) ) x. -u 1 ) )
86		oveq2 5786	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , -u 1 , 0 ) = 0 -> ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = ( ( * ` ( f ` A ) ) x. 0 ) )
87	85, 86	ifsb 3534	. . . . . . . . . . . . . 14 |- ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( * ` ( f ` A ) ) x. -u 1 ) , ( ( * ` ( f ` A ) ) x. 0 ) )
88		simplll 737	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ph )
89		rpvmasum2.z1	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ f e. W ) -> A = ( 1r ` Z ) )
90	89	fveq2d 5448	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
91	88, 90	sylan 459	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
92	3, 8, 4	dchrmhm 20428	. . . . . . . . . . . . . . . . . . . . . . . 24 |- D C_ ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) )
93		simpr 449	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. D )
94	92, 93	sseldi 3139	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) )
95		eqid 2256	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` Z ) = (mulGrp ` Z )
96		eqid 2256	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1r ` Z ) = ( 1r ` Z )
97	95, 96	rngidval 15291	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1r ` Z ) = ( 0g ` (mulGrp ` Z ) )
98		eqid 2256	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` ℂfld ) = (mulGrp ` ℂfld )
99		cnfld1 16347	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 = ( 1r ` ℂfld )
100	98, 99	rngidval 15291	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 = ( 0g ` (mulGrp ` ℂfld ) )
101	97, 100	mhm0 14371	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) -> ( f ` ( 1r ` Z ) ) = 1 )
102	94, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` ( 1r ` Z ) ) = 1 )
103	102	ad2antrr 709	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` ( 1r ` Z ) ) = 1 )
104	91, 103	eqtrd 2288	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = 1 )
105	104	fveq2d 5448	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
106	105, 78	syl6eq 2304	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = 1 )
107	106	oveq1d 5793	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = ( 1 x. -u 1 ) )
108	53	mulid2i 8794	. . . . . . . . . . . . . . . . 17 |- ( 1 x. -u 1 ) = -u 1
109	107, 108	syl6eq 2304	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = -u 1 )
110	109	ifeq1da 3550	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
111	20	adantr 453	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( * ` ( f ` A ) ) e. CC )
112	111	mul01d 8965	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( ( * ` ( f ` A ) ) x. 0 ) = 0 )
113	112	ifeq2d 3540	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) )
114	110, 113	eqtrd 2288	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
115	87, 114	syl5eq 2300	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
116	84, 115	sylan2br 464	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
117	116	ifeq2da 3551	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> if ( f = .1. , 1 , ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) ) = if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) )
118	83, 117	eqtrd 2288	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
119	68, 118	syl5eq 2300	. . . . . . . . 9 |- ( ( ( 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 ) ) )
120	119	oveq2d 5794	. . . . . . . 8 |- ( ( ( 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 ) ) ) )
121	65, 120	eqtrd 2288	. . . . . . 7 |- ( ( ( 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 ) ) ) )
122	63, 121	oveq12d 5796	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( ( * ` ( f ` A ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
123	62, 122	eqtrd 2288	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
124	123	sumeq2dv 12127	. . . 4 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. D ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
125		fzfid 10987	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
126		inss1 3350	. . . . . . . . 9 |- ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) )
127		ssfi 7037	. . . . . . . . 9 |- ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
128	125, 126, 127	sylancl 646	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
129	2	phicld 12788	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. NN )
130	129	nncnd 9716	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. CC )
131	126	a1i 12	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) )
132	131	sselda 3141	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
133	132, 42	syldan 458	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( (Λ ` n ) / n ) e. CC )
134	128, 130, 133	fsummulc2 12197	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( (Λ ` n ) / n ) ) = sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) )
135	130	adantr 453	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( phi ` N ) e. CC )
136	135, 42	mulcld 8809	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
137	132, 136	syldan 458	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
138	137	ralrimiva 2599	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> A. n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
139	125	olcd 384	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` x ) ) e. Fin ) )
140		sumss2 12150	. . . . . . . 8 |- ( ( ( ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) /\ A. n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC ) /\ ( ( 1 ... ( |_ ` x ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` x ) ) e. Fin ) ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , 0 ) )
141	131, 138, 139, 140	syl21anc 1186	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , 0 ) )
142		elin 3319	. . . . . . . . . . . . 13 |- ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> ( n e. ( 1 ... ( |_ ` x ) ) /\ n e. T ) )
143	142	baib 876	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( |_ ` x ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
144	143	adantl 454	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
145		rpvmasum2.t	. . . . . . . . . . . . 13 |- T = ( `' L " { A } )
146	145	eleq2i 2320	. . . . . . . . . . . 12 |- ( n e. T <-> n e. ( `' L " { A } ) )
147		ffn 5313	. . . . . . . . . . . . . 14 |- ( L : ZZ --> ( Base ` Z ) -> L Fn ZZ )
148	29, 147	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L Fn ZZ )
149		fniniseg 5566	. . . . . . . . . . . . . 14 |- ( L Fn ZZ -> ( n e. ( `' L " { A } ) <-> ( n e. ZZ /\ ( L ` n ) = A ) ) )
150	149	baibd 880	. . . . . . . . . . . . 13 |- ( ( L Fn ZZ /\ n e. ZZ ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
151	148, 30, 150	syl2an 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
152	146, 151	syl5bb 250	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. T <-> ( L ` n ) = A ) )
153	144, 152	bitr2d 247	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( L ` n ) = A <-> n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) )
154	42	mul02d 8964	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 x. ( (Λ ` n ) / n ) ) = 0 )
155	153, 154	ifbieq2d 3545	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> if ( ( L ` n ) = A , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , ( 0 x. ( (Λ ` n ) / n ) ) ) = if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , 0 ) )
156		oveq1 5785	. . . . . . . . . . 11 |- ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) = ( phi ` N ) -> ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( (Λ ` n ) / n ) ) = ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) )
157		oveq1 5785	. . . . . . . . . . 11 |- ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) = 0 -> ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( (Λ ` n ) / n ) ) = ( 0 x. ( (Λ ` n ) / n ) ) )
158	156, 157	ifsb 3534	. . . . . . . . . 10 |- ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( (Λ ` n ) / n ) ) = if ( ( L ` n ) = A , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , ( 0 x. ( (Λ ` n ) / n ) ) )
159	1	ad2antrr 709	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> N e. NN )
160	159, 5	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> D e. Fin )
161	20	adantlr 698	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
162	35, 161	mulcld 8809	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) e. CC )
163	160, 42, 162	fsummulc1 12198	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ f e. D ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( (Λ ` n ) / n ) ) = sum_ f e. D ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( (Λ ` n ) / n ) ) )
164	14	ad2antrr 709	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. U )
165	3, 4, 8, 9, 12, 159, 32, 164	sum2dchr 20461	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
166	165	oveq1d 5793	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ f e. D ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( (Λ ` n ) / n ) ) = ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( (Λ ` n ) / n ) ) )
167	42	adantr 453	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( (Λ ` n ) / n ) e. CC )
168		mulass 8779	. . . . . . . . . . . . . 14 |- ( ( ( f ` ( L ` n ) ) e. CC /\ ( * ` ( f ` A ) ) e. CC /\ ( (Λ ` n ) / n ) e. CC ) -> ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( (Λ ` n ) / n ) ) = ( ( f ` ( L ` n ) ) x. ( ( * ` ( f ` A ) ) x. ( (Λ ` n ) / n ) ) ) )
169		mul12 8932	. . . . . . . . . . . . . 14 |- ( ( ( f ` ( L ` n ) ) e. CC /\ ( * ` ( f ` A ) ) e. CC /\ ( (Λ ` n ) / n ) e. CC ) -> ( ( f ` ( L ` n ) ) x. ( ( * ` ( f ` A ) ) x. ( (Λ ` n ) / n ) ) ) = ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
170	168, 169	eqtrd 2288	. . . . . . . . . . . . 13 |- ( ( ( f ` ( L ` n ) ) e. CC /\ ( * ` ( f ` A ) ) e. CC /\ ( (Λ ` n ) / n ) e. CC ) -> ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( (Λ ` n ) / n ) ) = ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
171	35, 161, 167, 170	syl3anc 1187	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( (Λ ` n ) / n ) ) = ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
172	171	sumeq2dv 12127	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ f e. D ( ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) x. ( (Λ ` n ) / n ) ) = sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
173	163, 166, 172	3eqtr3d 2296	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( (Λ ` n ) / n ) ) = sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
174	158, 173	syl5eqr 2302	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> if ( ( L ` n ) = A , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , ( 0 x. ( (Λ ` n ) / n ) ) ) = sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
175	155, 174	eqtr3d 2290	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , 0 ) = sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
176	175	sumeq2dv 12127	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) if ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , 0 ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
177	134, 141, 176	3eqtrd 2292	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( (Λ ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
178	125, 6, 45	fsumcom 12189	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ f e. D ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) = sum_ f e. D sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
179	177, 178	eqtrd 2288	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( (Λ ` n ) / n ) ) = sum_ f e. D sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) )
180	3	dchrabl 20441	. . . . . . . . . . 11 |- ( N e. NN -> G e. Abel )
181		ablgrp 15042	. . . . . . . . . . 11 |- ( G e. Abel -> G e. Grp )
182	2, 180, 181	3syl 20	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> G e. Grp )
183	4, 70	grpidcl 14458	. . . . . . . . . 10 |- ( G e. Grp -> .1. e. D )
184	182, 183	syl 17	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> .1. e. D )
185	50	mulid1d 8806	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
186	185, 50	eqeltrd 2330	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) e. CC )
187		iftrue 3531	. . . . . . . . . . 11 |- ( f = .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = 1 )
188	187	oveq2d 5794	. . . . . . . . . 10 |- ( f = .1. -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. 1 ) )
189	188	sumsn 12164	. . . . . . . . 9 |- ( ( .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 ) )
190	184, 186, 189	syl2anc 645	. . . . . . . 8 |- ( ( 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 ) )
191		eldifsn 3709	. . . . . . . . . . 11 |- ( f e. ( D \ { .1. } ) <-> ( f e. D /\ f =/= .1. ) )
192		ifnefalse 3533	. . . . . . . . . . . . . . 15 |- ( f =/= .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
193	192	ad2antll 712	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
194		negeq 8998	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 1 -> -u if ( f e. W , 1 , 0 ) = -u 1 )
195		negeq 8998	. . . . . . . . . . . . . . . 16 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = -u 0 )
196		neg0 9047	. . . . . . . . . . . . . . . 16 |- -u 0 = 0
197	195, 196	syl6eq 2304	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = 0 )
198	194, 197	ifsb 3534	. . . . . . . . . . . . . 14 |- -u if ( f e. W , 1 , 0 ) = if ( f e. W , -u 1 , 0 )
199	193, 198	syl6eqr 2306	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
200	199	oveq2d 5794	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
201	50	adantr 453	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( log ` x ) e. CC )
202	52, 54	keepel 3582	. . . . . . . . . . . . 13 |- if ( f e. W , 1 , 0 ) e. CC
203		mulneg2 9171	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
204	201, 202, 203	sylancl 646	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
205	200, 204	eqtrd 2288	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
206	191, 205	sylan2b 463	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
207	206	sumeq2dv 12127	. . . . . . . . 9 |- ( ( 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 ) ) )
208		diffi 7043	. . . . . . . . . . 11 |- ( D e. Fin -> ( D \ { .1. } ) e. Fin )
209	6, 208	syl 17	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( D \ { .1. } ) e. Fin )
210	50	adantr 453	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( log ` x ) e. CC )
211		mulcl 8775	. . . . . . . . . . 11 |- ( ( ( log ` x ) e. CC /\ if ( f e. W , 1 , 0 ) e. CC ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
212	210, 202, 211	sylancl 646	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
213	209, 212	fsumneg 12200	. . . . . . . . 9 |- ( ( 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 ) ) )
214	202	a1i 12	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> if ( f e. W , 1 , 0 ) e. CC )
215	209, 50, 214	fsummulc2 12197	. . . . . . . . . . 11 |- ( ( 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 ) ) )
216		rpvmasum2.w	. . . . . . . . . . . . . . . . 17 |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
217		ssrab2 3219	. . . . . . . . . . . . . . . . 17 |- { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } C_ ( D \ { .1. } )
218	216, 217	eqsstri 3169	. . . . . . . . . . . . . . . 16 |- W C_ ( D \ { .1. } )
219		difss 3264	. . . . . . . . . . . . . . . 16 |- ( D \ { .1. } ) C_ D
220	218, 219	sstri 3149	. . . . . . . . . . . . . . 15 |- W C_ D
221		ssfi 7037	. . . . . . . . . . . . . . 15 |- ( ( D e. Fin /\ W C_ D ) -> W e. Fin )
222	6, 220, 221	sylancl 646	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W e. Fin )
223		fsumconst 12203	. . . . . . . . . . . . . 14 |- ( ( W e. Fin /\ 1 e. CC ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
224	222, 52, 223	sylancl 646	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
225	218	a1i 12	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W C_ ( D \ { .1. } ) )
226	52	a1i 12	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> 1 e. CC )
227	226	ralrimivw 2600	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> A. f e. W 1 e. CC )
228	209	olcd 384	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( ( D \ { .1. } ) C_ ( ZZ>= ` 1 ) \/ ( D \ { .1. } ) e. Fin ) )
229		sumss2 12150	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
230	225, 227, 228, 229	syl21anc 1186	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) )
231		hashcl 11302	. . . . . . . . . . . . . . . 16 |- ( W e. Fin -> ( # ` W ) e. NN0 )
232	222, 231	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. NN0 )
233	232	nn0cnd 9973	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. CC )
234	233	mulid1d 8806	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> ( ( # ` W ) x. 1 ) = ( # ` W ) )
235	224, 230, 234	3eqtr3d 2296	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) = ( # ` W ) )
236	235	oveq2d 5794	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
237	215, 236	eqtr3d 2290	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
238	237	negeqd 9000	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> -u sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) = -u ( ( log ` x ) x. ( # ` W ) ) )
239	207, 213, 238	3eqtrd 2292	. . . . . . . 8 |- ( ( 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 ) ) )
240	190, 239	oveq12d 5796	. . . . . . 7 |- ( ( 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 ) ) ) )
241	50, 233	mulcld 8809	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( # ` W ) ) e. CC )
242	186, 241	negsubd 9117	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( ( ( log ` x ) x. 1 ) + -u ( ( log ` x ) x. ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
243	240, 242	eqtrd 2288	. . . . . 6 |- ( ( 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 ) ) ) )
244		disjdif 3487	. . . . . . . 8 |- ( { .1. } i^i ( D \ { .1. } ) ) = (/)
245	244	a1i 12	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } i^i ( D \ { .1. } ) ) = (/) )
246		undif2 3491	. . . . . . . 8 |- ( { .1. } u. ( D \ { .1. } ) ) = ( { .1. } u. D )
247	184	snssd 3720	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> { .1. } C_ D )
248		ssequn1 3306	. . . . . . . . 9 |- ( { .1. } C_ D <-> ( { .1. } u. D ) = D )
249	247, 248	sylib 190	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } u. D ) = D )
250	246, 249	syl5req 2301	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> D = ( { .1. } u. ( D \ { .1. } ) ) )
251	245, 250, 6, 58	fsumsplit 12163	. . . . . 6 |- ( ( 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 ) ) ) ) )
252	50, 226, 233	subdid 9189	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
253	243, 251, 252	3eqtr4rd 2299	. . . . 5 |- ( ( 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 ) ) ) )
254	179, 253	oveq12d 5796	. . . 4 |- ( ( ph /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) = ( sum_ f e. D sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) - sum_ f e. D ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) )
255	59, 124, 254	3eqtr4d 2298	. . 3 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. D ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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 ) ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) )
256	255	mpteq2dva 4066	. 2 |- ( ph -> ( x e. RR+ |-> sum_ f e. D ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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 ) ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) )
257		rpssre 10317	. . . 4 |- RR+ C_ RR
258	257	a1i 12	. . 3 |- ( ph -> RR+ C_ RR )
259	1, 5	syl 17	. . 3 |- ( ph -> D e. Fin )
260	18	adantlr 698	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` A ) e. CC )
261	260	cjcld 11632	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
262	61, 58	subcld 9111	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) e. CC )
263	261, 262	mulcld 8809	. . . 4 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) e. CC )
264	263	anasss 631	. . 3 |- ( ( ph /\ ( x e. RR+ /\ f e. D ) ) -> ( ( * ` ( f ` A ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) e. CC )
265	19	adantr 453	. . . 4 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( * ` ( f ` A ) ) e. CC )
266	262	an32s 782	. . . 4 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) e. CC )
267		o1const 12044	. . . . 5 |- ( ( RR+ C_ RR /\ ( * ` ( f ` A ) ) e. CC ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O ( 1 ) )
268	257, 19, 267	sylancr 647	. . . 4 |- ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O ( 1 ) )
269		fveq1 5443	. . . . . . . . . . . 12 |- ( f = .1. -> ( f ` ( L ` n ) ) = ( .1. ` ( L ` n ) ) )
270	269	oveq1d 5793	. . . . . . . . . . 11 |- ( f = .1. -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) = ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) )
271	270	sumeq2sdv 12128	. . . . . . . . . 10 |- ( f = .1. -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) )
272	271, 188	oveq12d 5796	. . . . . . . . 9 |- ( f = .1. -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. 1 ) ) )
273	272	adantl 454	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f = .1. ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. 1 ) ) )
274	48	recnd 8815	. . . . . . . . . 10 |- ( x e. RR+ -> ( log ` x ) e. CC )
275	274	mulid1d 8806	. . . . . . . . 9 |- ( x e. RR+ -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
276	275	oveq2d 5794	. . . . . . . 8 |- ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. 1 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( log ` x ) ) )
277	273, 276	sylan9eq 2308	. . . . . . 7 |- ( ( ( ( ph /\ f e. D ) /\ f = .1. ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) - ( log ` x ) ) )
278	277	mpteq2dva 4066	. . . . . 6 |- ( ( ( ph /\ f e. D ) /\ f = .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) )
279	8, 25, 1, 3, 4, 70	rpvmasumlem 20584	. . . . . . 7 |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) e. O ( 1 ) )
280	279	ad2antrr 709	. . . . . 6 |- ( ( ( ph /\ f e. D ) /\ f = .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) e. O ( 1 ) )
281	278, 280	eqeltrd 2330	. . . . 5 |- ( ( ( ph /\ f e. D ) /\ f = .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) ) ) e. O ( 1 ) )
282	192	oveq2d 5794	. . . . . . . . . 10 |- ( 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 ) ) )
283	282	oveq2d 5794	. . . . . . . . 9 |- ( f =/= .1. -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) ) )
284	50	adantlr 698	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
285		mulcom 8777	. . . . . . . . . . . . . . 15 |- ( ( ( log ` x ) e. CC /\ -u 1 e. CC ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
286	284, 53, 285	sylancl 646	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
287	284	mulm1d 9185	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( -u 1 x. ( log ` x ) ) = -u ( log ` x ) )
288	286, 287	eqtrd 2288	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = -u ( log ` x ) )
289	284	mul01d 8965	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. 0 ) = 0 )
290	288, 289	ifeq12d 3541	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
291		oveq2 5786	. . . . . . . . . . . . 13 |- ( if ( f e. W , -u 1 , 0 ) = -u 1 -> ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = ( ( log ` x ) x. -u 1 ) )
292		oveq2 5786	. . . . . . . . . . . . 13 |- ( if ( f e. W , -u 1 , 0 ) = 0 -> ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = ( ( log ` x ) x. 0 ) )
293	291, 292	ifsb 3534	. . . . . . . . . . . 12 |- ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( log ` x ) x. -u 1 ) , ( ( log ` x ) x. 0 ) )
294		negeq 8998	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = ( log ` x ) -> -u if ( f e. W , ( log ` x ) , 0 ) = -u ( log ` x ) )
295		negeq 8998	. . . . . . . . . . . . . 14 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = -u 0 )
296	295, 196	syl6eq 2304	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = 0 )
297	294, 296	ifsb 3534	. . . . . . . . . . . 12 |- -u if ( f e. W , ( log ` x ) , 0 ) = if ( f e. W , -u ( log ` x ) , 0 )
298	290, 293, 297	3eqtr4g 2313	. . . . . . . . . . 11 |- ( ( ( 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 ) )
299	298	oveq2d 5794	. . . . . . . . . 10 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - -u if ( f e. W , ( log ` x ) , 0 ) ) )
300	61	an32s 782	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
301		ifcl 3561	. . . . . . . . . . . 12 |- ( ( ( log ` x ) e. CC /\ 0 e. CC ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
302	284, 54, 301	sylancl 646	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
303	300, 302	subnegd 9118	. . . . . . . . . 10 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - -u if ( f e. W , ( log ` x ) , 0 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) )
304	299, 303	eqtrd 2288	. . . . . . . . 9 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) )
305	283, 304	sylan9eqr 2310	. . . . . . . 8 |- ( ( ( ( ph /\ f e. D ) /\ x e. RR+ ) /\ f =/= .1. ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) )
306	305	an32s 782	. . . . . . 7 |- ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) )
307	306	mpteq2dva 4066	. . . . . 6 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` 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. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) )
308	1	ad2antrr 709	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> N e. NN )
309		simplr 734	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f e. D )
310		simpr 449	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f =/= .1. )
311		eqid 2256	. . . . . . . 8 |- ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) = ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) )
312	8, 25, 308, 3, 4, 70, 309, 310, 311	dchrmusumlema 20590	. . . . . . 7 |- ( ( ( 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 ) ) )
313	1	adantr 453	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. D ) -> N e. NN )
314	313	ad2antrr 709	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
315	309	adantr 453	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
316		simplr 734	. . . . . . . . . . . . 13 |- ( ( ( ( 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. )
317		simprl 735	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
318		simprrl 743	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
319		simprrr 744	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
320	8, 25, 314, 3, 4, 70, 315, 316, 311, 317, 318, 319, 216	dchrvmaeq0 20601	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
321		ifbi 3542	. . . . . . . . . . . . . 14 |- ( ( f e. W <-> t = 0 ) -> if ( f e. W , ( log ` x ) , 0 ) = if ( t = 0 , ( log ` x ) , 0 ) )
322	321	oveq2d 5794	. . . . . . . . . . . . 13 |- ( ( f e. W <-> t = 0 ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( t = 0 , ( log ` x ) , 0 ) ) )
323	322	mpteq2dv 4067	. . . . . . . . . . . 12 |- ( ( f