Theorem rpvmasum2 23425

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

Dummy variables c t a are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpvmasum.a	. . . . . . 7 |- ( ph -> N e. NN )
2	1	adantr 465	. . . . . 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 23258	. . . . . 6 |- ( N e. NN -> D e. Fin )
6	2, 5	syl 16	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> D e. Fin )
7		fzfid 12047	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
8		rpvmasum.z	. . . . . . . . . . . . 13 |- Z = (ℤ/nℤ ` N )
9		eqid 2467	. . . . . . . . . . . . 13 |- ( Base ` Z ) = ( Base ` Z )
10		simpr 461	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> f e. D )
11	3, 8, 4, 9, 10	dchrf 23245	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> f : ( Base ` Z ) --> CC )
12		rpvmasum2.u	. . . . . . . . . . . . . . 15 |- U = (Unit ` Z )
13	9, 12	unitss 17093	. . . . . . . . . . . . . 14 |- U C_ ( Base ` Z )
14		rpvmasum2.b	. . . . . . . . . . . . . 14 |- ( ph -> A e. U )
15	13, 14	sseldi 3502	. . . . . . . . . . . . 13 |- ( ph -> A e. ( Base ` Z ) )
16	15	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> A e. ( Base ` Z ) )
17	11, 16	ffvelrnd 6020	. . . . . . . . . . 11 |- ( ( ph /\ f e. D ) -> ( f ` A ) e. CC )
18	17	cjcld 12988	. . . . . . . . . 10 |- ( ( ph /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
19	18	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
20	19	adantrl 715	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( * ` ( f ` A ) ) e. CC )
21	11	adantlr 714	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
22	21	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
23	1	nnnn0d 10848	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
24		rpvmasum.l	. . . . . . . . . . . . . . . 16 |- L = ( ZRHom ` Z )
25	8, 9, 24	znzrhfo 18353	. . . . . . . . . . . . . . 15 |- ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
26		fof 5793	. . . . . . . . . . . . . . 15 |- ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
27	23, 25, 26	3syl 20	. . . . . . . . . . . . . 14 |- ( ph -> L : ZZ --> ( Base ` Z ) )
28	27	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L : ZZ --> ( Base ` Z ) )
29		elfzelz 11684	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
30		ffvelrn 6017	. . . . . . . . . . . . 13 |- ( ( L : ZZ --> ( Base ` Z ) /\ n e. ZZ ) -> ( L ` n ) e. ( Base ` Z ) )
31	28, 29, 30	syl2an 477	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` n ) e. ( Base ` Z ) )
32	31	adantr 465	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( L ` n ) e. ( Base ` Z ) )
33	22, 32	ffvelrnd 6020	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( f ` ( L ` n ) ) e. CC )
34	33	anasss 647	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( f ` ( L ` n ) ) e. CC )
35		elfznn 11710	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
36	35	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
37		vmacl 23120	. . . . . . . . . . . . 13 |- ( n e. NN -> (Λ ` n ) e. RR )
38	36, 37	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (Λ ` n ) e. RR )
39	38, 36	nndivred 10580	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. RR )
40	39	recnd 9618	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. CC )
41	40	adantrr 716	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( (Λ ` n ) / n ) e. CC )
42	34, 41	mulcld 9612	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
43	20, 42	mulcld 9612	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) e. CC )
44	43	anass1rs 805	. . . . . 6 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) e. CC )
45	7, 44	fsumcl 13514	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( * ` ( f ` A ) ) x. ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) e. CC )
46		relogcl 22691	. . . . . . . . 9 |- ( x e. RR+ -> ( log ` x ) e. RR )
47	46	adantl 466	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
48	47	recnd 9618	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
49	48	adantr 465	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( log ` x ) e. CC )
50		ax-1cn 9546	. . . . . . 7 |- 1 e. CC
51		neg1cn 10635	. . . . . . . 8 |- -u 1 e. CC
52		0cn 9584	. . . . . . . 8 |- 0 e. CC
53	51, 52	keepel 4007	. . . . . . 7 |- if ( f e. W , -u 1 , 0 ) e. CC
54	50, 53	keepel 4007	. . . . . 6 |- if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC
55		mulcl 9572	. . . . . 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 )
56	49, 54, 55	sylancl 662	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) e. CC )
57	6, 45, 56	fsumsub 13562	. . . 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 ) ) ) ) )
58	42	anass1rs 805	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
59	7, 58	fsumcl 13514	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
60	19, 59, 56	subdid 10008	. . . . . 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 ) ) ) ) ) )
61	7, 19, 58	fsummulc2 13558	. . . . . . 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 ) ) ) )
62	54	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC )
63	19, 49, 62	mul12d 9784	. . . . . . . 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 ) ) ) ) )
64		oveq2 6290	. . . . . . . . . . 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 ) )
65		oveq2 6290	. . . . . . . . . . 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 ) ) )
66	64, 65	ifsb 3952	. . . . . . . . . 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 ) ) )
67		fveq1 5863	. . . . . . . . . . . . . . . . 17 |- ( f = .1. -> ( f ` A ) = ( .1. ` A ) )
68		rpvmasum2.1	. . . . . . . . . . . . . . . . . 18 |- .1. = ( 0g ` G )
69	1	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> N e. NN )
70	14	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> A e. U )
71	3, 8, 68, 12, 69, 70	dchr1 23260	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( .1. ` A ) = 1 )
72	67, 71	sylan9eqr 2530	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( f ` A ) = 1 )
73	72	fveq2d 5868	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
74		1re 9591	. . . . . . . . . . . . . . . 16 |- 1 e. RR
75		cjre 12931	. . . . . . . . . . . . . . . 16 |- ( 1 e. RR -> ( * ` 1 ) = 1 )
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( * ` 1 ) = 1
77	73, 76	syl6eq 2524	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = 1 )
78	77	oveq1d 6297	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = ( 1 x. 1 ) )
79		1t1e1 10679	. . . . . . . . . . . . 13 |- ( 1 x. 1 ) = 1
80	78, 79	syl6eq 2524	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = 1 )
81	80	ifeq1da 3969	. . . . . . . . . . 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 ) ) ) )
82		df-ne 2664	. . . . . . . . . . . . 13 |- ( f =/= .1. <-> -. f = .1. )
83		oveq2 6290	. . . . . . . . . . . . . . 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 ) )
84		oveq2 6290	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , -u 1 , 0 ) = 0 -> ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = ( ( * ` ( f ` A ) ) x. 0 ) )
85	83, 84	ifsb 3952	. . . . . . . . . . . . . 14 |- ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( * ` ( f ` A ) ) x. -u 1 ) , ( ( * ` ( f ` A ) ) x. 0 ) )
86		simplll 757	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ph )
87		rpvmasum2.z1	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ f e. W ) -> A = ( 1r ` Z ) )
88	87	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
89	86, 88	sylan 471	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
90	3, 8, 4	dchrmhm 23244	. . . . . . . . . . . . . . . . . . . . . . . 24 |- D C_ ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) )
91		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. D )
92	90, 91	sseldi 3502	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) )
93		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` Z ) = (mulGrp ` Z )
94		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1r ` Z ) = ( 1r ` Z )
95	93, 94	rngidval 16945	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1r ` Z ) = ( 0g ` (mulGrp ` Z ) )
96		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` ℂfld ) = (mulGrp ` ℂfld )
97		cnfld1 18214	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 = ( 1r ` ℂfld )
98	96, 97	rngidval 16945	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 = ( 0g ` (mulGrp ` ℂfld ) )
99	95, 98	mhm0 15785	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) -> ( f ` ( 1r ` Z ) ) = 1 )
100	92, 99	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` ( 1r ` Z ) ) = 1 )
101	100	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` ( 1r ` Z ) ) = 1 )
102	89, 101	eqtrd 2508	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = 1 )
103	102	fveq2d 5868	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
104	103, 76	syl6eq 2524	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = 1 )
105	104	oveq1d 6297	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = ( 1 x. -u 1 ) )
106	51	mulid2i 9595	. . . . . . . . . . . . . . . . 17 |- ( 1 x. -u 1 ) = -u 1
107	105, 106	syl6eq 2524	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = -u 1 )
108	107	ifeq1da 3969	. . . . . . . . . . . . . . 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 ) ) )
109	19	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( * ` ( f ` A ) ) e. CC )
110	109	mul01d 9774	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( ( * ` ( f ` A ) ) x. 0 ) = 0 )
111	110	ifeq2d 3958	. . . . . . . . . . . . . . 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 ) )
112	108, 111	eqtrd 2508	. . . . . . . . . . . . . 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 ) )
113	85, 112	syl5eq 2520	. . . . . . . . . . . . 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 ) )
114	82, 113	sylan2br 476	. . . . . . . . . . . 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 ) )
115	114	ifeq2da 3970	. . . . . . . . . . 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 ) ) )
116	81, 115	eqtrd 2508	. . . . . . . . . 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 ) ) )
117	66, 116	syl5eq 2520	. . . . . . . . 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 ) ) )
118	117	oveq2d 6298	. . . . . . . 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 ) ) ) )
119	63, 118	eqtrd 2508	. . . . . . 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 ) ) ) )
120	61, 119	oveq12d 6300	. . . . . 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 ) ) ) ) )
121	60, 120	eqtrd 2508	. . . . 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 ) ) ) ) )
122	121	sumeq2dv 13484	. . . 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 ) ) ) ) )
123		fzfid 12047	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
124		inss1 3718	. . . . . . . . 9 |- ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) )
125		ssfi 7737	. . . . . . . . 9 |- ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
126	123, 124, 125	sylancl 662	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
127	2	phicld 14157	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. NN )
128	127	nncnd 10548	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. CC )
129	124	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) )
130	129	sselda 3504	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
131	130, 40	syldan 470	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( (Λ ` n ) / n ) e. CC )
132	126, 128, 131	fsummulc2 13558	. . . . . . 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 ) ) )
133	128	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( phi ` N ) e. CC )
134	133, 40	mulcld 9612	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
135	130, 134	syldan 470	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
136	135	ralrimiva 2878	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> A. n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
137	123	olcd 393	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` x ) ) e. Fin ) )
138		sumss2 13507	. . . . . . . 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 ) )
139	129, 136, 137, 138	syl21anc 1227	. . . . . . 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 ) )
140		elin 3687	. . . . . . . . . . . . 13 |- ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> ( n e. ( 1 ... ( |_ ` x ) ) /\ n e. T ) )
141	140	baib 901	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( |_ ` x ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
142	141	adantl 466	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
143		rpvmasum2.t	. . . . . . . . . . . . 13 |- T = ( `' L " { A } )
144	143	eleq2i 2545	. . . . . . . . . . . 12 |- ( n e. T <-> n e. ( `' L " { A } ) )
145		ffn 5729	. . . . . . . . . . . . . 14 |- ( L : ZZ --> ( Base ` Z ) -> L Fn ZZ )
146	28, 145	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L Fn ZZ )
147		fniniseg 6000	. . . . . . . . . . . . . 14 |- ( L Fn ZZ -> ( n e. ( `' L " { A } ) <-> ( n e. ZZ /\ ( L ` n ) = A ) ) )
148	147	baibd 907	. . . . . . . . . . . . 13 |- ( ( L Fn ZZ /\ n e. ZZ ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
149	146, 29, 148	syl2an 477	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
150	144, 149	syl5bb 257	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. T <-> ( L ` n ) = A ) )
151	142, 150	bitr2d 254	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( L ` n ) = A <-> n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) )
152	40	mul02d 9773	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 x. ( (Λ ` n ) / n ) ) = 0 )
153	151, 152	ifbieq2d 3964	. . . . . . . . 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 ) )
154		oveq1 6289	. . . . . . . . . . 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 ) ) )
155		oveq1 6289	. . . . . . . . . . 11 |- ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) = 0 -> ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( (Λ ` n ) / n ) ) = ( 0 x. ( (Λ ` n ) / n ) ) )
156	154, 155	ifsb 3952	. . . . . . . . . 10 |- ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( (Λ ` n ) / n ) ) = if ( ( L ` n ) = A , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , ( 0 x. ( (Λ ` n ) / n ) ) )
157	1	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> N e. NN )
158	157, 5	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> D e. Fin )
159	19	adantlr 714	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
160	33, 159	mulcld 9612	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) e. CC )
161	158, 40, 160	fsummulc1 13559	. . . . . . . . . . 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 ) ) )
162	14	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. U )
163	3, 4, 8, 9, 12, 157, 31, 162	sum2dchr 23277	. . . . . . . . . . . 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 ) )
164	163	oveq1d 6297	. . . . . . . . . . 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 ) ) )
165	40	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( (Λ ` n ) / n ) e. CC )
166		mulass 9576	. . . . . . . . . . . . . 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 ) ) ) )
167		mul12 9741	. . . . . . . . . . . . . 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 ) ) ) )
168	166, 167	eqtrd 2508	. . . . . . . . . . . . 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 ) ) ) )
169	33, 159, 165, 168	syl3anc 1228	. . . . . . . . . . . 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 ) ) ) )
170	169	sumeq2dv 13484	. . . . . . . . . . 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 ) ) ) )
171	161, 164, 170	3eqtr3d 2516	. . . . . . . . . 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 ) ) ) )
172	156, 171	syl5eqr 2522	. . . . . . . . 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 ) ) ) )
173	153, 172	eqtr3d 2510	. . . . . . . 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 ) ) ) )
174	173	sumeq2dv 13484	. . . . . . 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 ) ) ) )
175	132, 139, 174	3eqtrd 2512	. . . . . 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 ) ) ) )
176	123, 6, 43	fsumcom 13549	. . . . . 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 ) ) ) )
177	175, 176	eqtrd 2508	. . . . 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 ) ) ) )
178	3	dchrabl 23257	. . . . . . . . . 10 |- ( N e. NN -> G e. Abel )
179		ablgrp 16599	. . . . . . . . . 10 |- ( G e. Abel -> G e. Grp )
180	4, 68	grpidcl 15879	. . . . . . . . . 10 |- ( G e. Grp -> .1. e. D )
181	2, 178, 179, 180	4syl 21	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> .1. e. D )
182	48	mulid1d 9609	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
183	182, 48	eqeltrd 2555	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) e. CC )
184		iftrue 3945	. . . . . . . . . . 11 |- ( f = .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = 1 )
185	184	oveq2d 6298	. . . . . . . . . 10 |- ( f = .1. -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. 1 ) )
186	185	sumsn 13522	. . . . . . . . 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 ) )
187	181, 183, 186	syl2anc 661	. . . . . . . 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 ) )
188		eldifsn 4152	. . . . . . . . . . 11 |- ( f e. ( D \ { .1. } ) <-> ( f e. D /\ f =/= .1. ) )
189		ifnefalse 3951	. . . . . . . . . . . . . . 15 |- ( f =/= .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
190	189	ad2antll 728	. . . . . . . . . . . . . 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 ) )
191		negeq 9808	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 1 -> -u if ( f e. W , 1 , 0 ) = -u 1 )
192		negeq 9808	. . . . . . . . . . . . . . . 16 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = -u 0 )
193		neg0 9861	. . . . . . . . . . . . . . . 16 |- -u 0 = 0
194	192, 193	syl6eq 2524	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = 0 )
195	191, 194	ifsb 3952	. . . . . . . . . . . . . 14 |- -u if ( f e. W , 1 , 0 ) = if ( f e. W , -u 1 , 0 )
196	190, 195	syl6eqr 2526	. . . . . . . . . . . . 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 ) )
197	196	oveq2d 6298	. . . . . . . . . . . 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 ) ) )
198	48	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( log ` x ) e. CC )
199	50, 52	keepel 4007	. . . . . . . . . . . . 13 |- if ( f e. W , 1 , 0 ) e. CC
200		mulneg2 9990	. . . . . . . . . . . . 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 ) ) )
201	198, 199, 200	sylancl 662	. . . . . . . . . . . 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 ) ) )
202	197, 201	eqtrd 2508	. . . . . . . . . . 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 ) ) )
203	188, 202	sylan2b 475	. . . . . . . . . 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 ) ) )
204	203	sumeq2dv 13484	. . . . . . . . 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 ) ) )
205		diffi 7747	. . . . . . . . . . 11 |- ( D e. Fin -> ( D \ { .1. } ) e. Fin )
206	6, 205	syl 16	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( D \ { .1. } ) e. Fin )
207	48	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( log ` x ) e. CC )
208		mulcl 9572	. . . . . . . . . . 11 |- ( ( ( log ` x ) e. CC /\ if ( f e. W , 1 , 0 ) e. CC ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
209	207, 199, 208	sylancl 662	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
210	206, 209	fsumneg 13561	. . . . . . . . 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 ) ) )
211	199	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> if ( f e. W , 1 , 0 ) e. CC )
212	206, 48, 211	fsummulc2 13558	. . . . . . . . . . 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 ) ) )
213		rpvmasum2.w	. . . . . . . . . . . . . . . . 17 |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
214		ssrab2 3585	. . . . . . . . . . . . . . . . 17 |- { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } C_ ( D \ { .1. } )
215	213, 214	eqsstri 3534	. . . . . . . . . . . . . . . 16 |- W C_ ( D \ { .1. } )
216		difss 3631	. . . . . . . . . . . . . . . 16 |- ( D \ { .1. } ) C_ D
217	215, 216	sstri 3513	. . . . . . . . . . . . . . 15 |- W C_ D
218		ssfi 7737	. . . . . . . . . . . . . . 15 |- ( ( D e. Fin /\ W C_ D ) -> W e. Fin )
219	6, 217, 218	sylancl 662	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W e. Fin )
220		fsumconst 13564	. . . . . . . . . . . . . 14 |- ( ( W e. Fin /\ 1 e. CC ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
221	219, 50, 220	sylancl 662	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
222	215	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W C_ ( D \ { .1. } ) )
223	50	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> 1 e. CC )
224	223	ralrimivw 2879	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> A. f e. W 1 e. CC )
225	206	olcd 393	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( ( D \ { .1. } ) C_ ( ZZ>= ` 1 ) \/ ( D \ { .1. } ) e. Fin ) )
226		sumss2 13507	. . . . . . . . . . . . . 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 ) )
227	222, 224, 225, 226	syl21anc 1227	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) )
228		hashcl 12392	. . . . . . . . . . . . . . . 16 |- ( W e. Fin -> ( # ` W ) e. NN0 )
229	219, 228	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. NN0 )
230	229	nn0cnd 10850	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. CC )
231	230	mulid1d 9609	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> ( ( # ` W ) x. 1 ) = ( # ` W ) )
232	221, 227, 231	3eqtr3d 2516	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) = ( # ` W ) )
233	232	oveq2d 6298	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
234	212, 233	eqtr3d 2510	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
235	234	negeqd 9810	. . . . . . . . 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 ) ) )
236	204, 210, 235	3eqtrd 2512	. . . . . . . 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 ) ) )
237	187, 236	oveq12d 6300	. . . . . . 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 ) ) ) )
238	48, 230	mulcld 9612	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( # ` W ) ) e. CC )
239	183, 238	negsubd 9932	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( ( ( log ` x ) x. 1 ) + -u ( ( log ` x ) x. ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
240	237, 239	eqtrd 2508	. . . . . 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 ) ) ) )
241		disjdif 3899	. . . . . . . 8 |- ( { .1. } i^i ( D \ { .1. } ) ) = (/)
242	241	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } i^i ( D \ { .1. } ) ) = (/) )
243		undif2 3903	. . . . . . . 8 |- ( { .1. } u. ( D \ { .1. } ) ) = ( { .1. } u. D )
244	181	snssd 4172	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> { .1. } C_ D )
245		ssequn1 3674	. . . . . . . . 9 |- ( { .1. } C_ D <-> ( { .1. } u. D ) = D )
246	244, 245	sylib 196	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } u. D ) = D )
247	243, 246	syl5req 2521	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> D = ( { .1. } u. ( D \ { .1. } ) ) )
248	242, 247, 6, 56	fsumsplit 13521	. . . . . 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 ) ) ) ) )
249	48, 223, 230	subdid 10008	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
250	240, 248, 249	3eqtr4rd 2519	. . . . 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 ) ) ) )
251	177, 250	oveq12d 6300	. . . 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 ) ) ) ) )
252	57, 122, 251	3eqtr4d 2518	. . 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 ) ) ) ) )
253	252	mpteq2dva 4533	. 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 ) ) ) ) ) )
254		rpssre 11226	. . . 4 |- RR+ C_ RR
255	254	a1i 11	. . 3 |- ( ph -> RR+ C_ RR )
256	1, 5	syl 16	. . 3 |- ( ph -> D e. Fin )
257	17	adantlr 714	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` A ) e. CC )
258	257	cjcld 12988	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
259	59, 56	subcld 9926	. . . . 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 )
260	258, 259	mulcld 9612	. . . 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 )
261	260	anasss 647	. . 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 )
262	18	adantr 465	. . . 4 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( * ` ( f ` A ) ) e. CC )
263	259	an32s 802	. . . 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 )
264		o1const 13401	. . . . 5 |- ( ( RR+ C_ RR /\ ( * ` ( f ` A ) ) e. CC ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O(1) )
265	254, 18, 264	sylancr 663	. . . 4 |- ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O(1) )
266		fveq1 5863	. . . . . . . . . . . 12 |- ( f = .1. -> ( f ` ( L ` n ) ) = ( .1. ` ( L ` n ) ) )
267	266	oveq1d 6297	. . . . . . . . . . 11 |- ( f = .1. -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) = ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) )
268	267	sumeq2sdv 13485	. . . . . . . . . 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 ) ) )
269	268, 185	oveq12d 6300	. . . . . . . . 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 ) ) )
270	269	adantl 466	. . . . . . . 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 ) ) )
271	46	recnd 9618	. . . . . . . . . 10 |- ( x e. RR+ -> ( log ` x ) e. CC )
272	271	mulid1d 9609	. . . . . . . . 9 |- ( x e. RR+ -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
273	272	oveq2d 6298	. . . . . . . 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 ) ) )
274	270, 273	sylan9eq 2528	. . . . . . 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 ) ) )
275	274	mpteq2dva 4533	. . . . . 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 ) ) ) )
276	8, 24, 1, 3, 4, 68	rpvmasumlem 23400	. . . . . . 7 |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
277	276	ad2antrr 725	. . . . . 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) )
278	275, 277	eqeltrd 2555	. . . . 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) )
279	189	oveq2d 6298	. . . . . . . . . 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 ) ) )
280	279	oveq2d 6298	. . . . . . . . 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 ) ) ) )
281	48	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
282		mulcom 9574	. . . . . . . . . . . . . . 15 |- ( ( ( log ` x ) e. CC /\ -u 1 e. CC ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
283	281, 51, 282	sylancl 662	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
284	281	mulm1d 10004	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( -u 1 x. ( log ` x ) ) = -u ( log ` x ) )
285	283, 284	eqtrd 2508	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = -u ( log ` x ) )
286	281	mul01d 9774	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. 0 ) = 0 )
287	285, 286	ifeq12d 3959	. . . . . . . . . . . 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 ) )
288		oveq2 6290	. . . . . . . . . . . . 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 ) )
289		oveq2 6290	. . . . . . . . . . . . 13 |- ( if ( f e. W , -u 1 , 0 ) = 0 -> ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = ( ( log ` x ) x. 0 ) )
290	288, 289	ifsb 3952	. . . . . . . . . . . 12 |- ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( log ` x ) x. -u 1 ) , ( ( log ` x ) x. 0 ) )
291		negeq 9808	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = ( log ` x ) -> -u if ( f e. W , ( log ` x ) , 0 ) = -u ( log ` x ) )
292		negeq 9808	. . . . . . . . . . . . . 14 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = -u 0 )
293	292, 193	syl6eq 2524	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = 0 )
294	291, 293	ifsb 3952	. . . . . . . . . . . 12 |- -u if ( f e. W , ( log ` x ) , 0 ) = if ( f e. W , -u ( log ` x ) , 0 )
295	287, 290, 294	3eqtr4g 2533	. . . . . . . . . . 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 ) )
296	295	oveq2d 6298	. . . . . . . . . 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 ) ) )
297	59	an32s 802	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
298		ifcl 3981	. . . . . . . . . . . 12 |- ( ( ( log ` x ) e. CC /\ 0 e. CC ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
299	281, 52, 298	sylancl 662	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
300	297, 299	subnegd 9933	. . . . . . . . . 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 ) ) )
301	296, 300	eqtrd 2508	. . . . . . . . 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 ) ) )
302	280, 301	sylan9eqr 2530	. . . . . . . 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 ) ) )
303	302	an32s 802	. . . . . . 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 ) ) )
304	303	mpteq2dva 4533	. . . . . 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 ) ) ) )
305	1	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> N e. NN )
306		simplr 754	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f e. D )
307		simpr 461	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f =/= .1. )
308		eqid 2467	. . . . . . . 8 |- ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) = ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) )
309	8, 24, 305, 3, 4, 68, 306, 307, 308	dchrmusumlema 23406	. . . . . . 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 ) ) )
310	1	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> N e. NN )
311	310	ad2antrr 725	. . . . . . . . . . . 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 ) ) ) ) -> N e. NN )
312	306	adantr 465	. . . . . . . . . . . 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. D )
313		simplr 754	. . . . . . . . . . . 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 =/= .1. )
314		simprl 755	. . . . . . . . . . . 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 ) ) ) ) -> c e. ( 0 [,) +oo ) )
315		simprrl 763	. . . . . . . . . . . 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 ) ) ) ) -> seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t )
316		simprrr 764	. . . . . . . . . . . 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 ) ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) )
317	8, 24, 311, 3, 4, 68, 312, 313, 308, 314, 315, 316, 213	dchrvmaeq0 23417	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
318		ifbi 3960	. . . . . . . . . . . . 13 |- ( ( f e. W <-> t = 0 ) -> if ( f e. W , ( log ` x ) , 0 ) = if ( t = 0 , ( log ` x ) , 0 ) )
319	318	oveq2d 6298	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
320	319	mpteq2dv 4534	. . . . . . . . . . 11 |- ( ( f e. W <-> t = 0 ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( t = 0 , ( log ` x ) , 0 ) ) ) )
321	317, 320	syl 16	. . . . . . . . . 10 |- ( ( ( ( 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