Theorem rpvmasum2 21159

Description: A partial result along the lines of rpvmasum 21173. 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 452	. . . . . 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 20992	. . . . . 6 |- ( N e. NN -> D e. Fin )
6	2, 5	syl 16	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> D e. Fin )
7		fzfid 11267	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
8		rpvmasum.z	. . . . . . . . . . . . 13 |- Z = (ℤ/nℤ ` N )
9		eqid 2404	. . . . . . . . . . . . 13 |- ( Base ` Z ) = ( Base ` Z )
10		simpr 448	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> f e. D )
11	3, 8, 4, 9, 10	dchrf 20979	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> f : ( Base ` Z ) --> CC )
12		rpvmasum2.u	. . . . . . . . . . . . . . 15 |- U = (Unit ` Z )
13	9, 12	unitss 15720	. . . . . . . . . . . . . 14 |- U C_ ( Base ` Z )
14		rpvmasum2.b	. . . . . . . . . . . . . 14 |- ( ph -> A e. U )
15	13, 14	sseldi 3306	. . . . . . . . . . . . 13 |- ( ph -> A e. ( Base ` Z ) )
16	15	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> A e. ( Base ` Z ) )
17	11, 16	ffvelrnd 5830	. . . . . . . . . . 11 |- ( ( ph /\ f e. D ) -> ( f ` A ) e. CC )
18	17	cjcld 11956	. . . . . . . . . 10 |- ( ( ph /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
19	18	adantlr 696	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
20	19	adantrl 697	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( * ` ( f ` A ) ) e. CC )
21	11	adantlr 696	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
22	21	adantlr 696	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
23	1	nnnn0d 10230	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
24		rpvmasum.l	. . . . . . . . . . . . . . . 16 |- L = ( ZRHom ` Z )
25	8, 9, 24	znzrhfo 16783	. . . . . . . . . . . . . . 15 |- ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
26		fof 5612	. . . . . . . . . . . . . . 15 |- ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
27	23, 25, 26	3syl 19	. . . . . . . . . . . . . 14 |- ( ph -> L : ZZ --> ( Base ` Z ) )
28	27	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L : ZZ --> ( Base ` Z ) )
29		elfzelz 11015	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
30		ffvelrn 5827	. . . . . . . . . . . . 13 |- ( ( L : ZZ --> ( Base ` Z ) /\ n e. ZZ ) -> ( L ` n ) e. ( Base ` Z ) )
31	28, 29, 30	syl2an 464	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` n ) e. ( Base ` Z ) )
32	31	adantr 452	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( L ` n ) e. ( Base ` Z ) )
33	22, 32	ffvelrnd 5830	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( f ` ( L ` n ) ) e. CC )
34	33	anasss 629	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( f ` ( L ` n ) ) e. CC )
35		elfznn 11036	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
36	35	adantl 453	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
37		vmacl 20854	. . . . . . . . . . . . 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 10004	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. RR )
40	39	recnd 9070	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. CC )
41	40	adantrr 698	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( (Λ ` n ) / n ) e. CC )
42	34, 41	mulcld 9064	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
43	20, 42	mulcld 9064	. . . . . . 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 783	. . . . . 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 12482	. . . . 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 20426	. . . . . . . . 9 |- ( x e. RR+ -> ( log ` x ) e. RR )
47	46	adantl 453	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
48	47	recnd 9070	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
49	48	adantr 452	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( log ` x ) e. CC )
50		ax-1cn 9004	. . . . . . 7 |- 1 e. CC
51		neg1cn 10023	. . . . . . . 8 |- -u 1 e. CC
52		0cn 9040	. . . . . . . 8 |- 0 e. CC
53	51, 52	keepel 3756	. . . . . . 7 |- if ( f e. W , -u 1 , 0 ) e. CC
54	50, 53	keepel 3756	. . . . . 6 |- if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC
55		mulcl 9030	. . . . . 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 644	. . . . 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 12526	. . . 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 783	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
59	7, 58	fsumcl 12482	. . . . . . 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 9445	. . . . . 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 12522	. . . . . . 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 9231	. . . . . . . 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 6048	. . . . . . . . . . 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 6048	. . . . . . . . . . 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 3708	. . . . . . . . . 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 5686	. . . . . . . . . . . . . . . . 17 |- ( f = .1. -> ( f ` A ) = ( .1. ` A ) )
68		rpvmasum2.1	. . . . . . . . . . . . . . . . . 18 |- .1. = ( 0g ` G )
69	1	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> N e. NN )
70	14	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> A e. U )
71	3, 8, 68, 12, 69, 70	dchr1 20994	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( .1. ` A ) = 1 )
72	67, 71	sylan9eqr 2458	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( f ` A ) = 1 )
73	72	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
74		1re 9046	. . . . . . . . . . . . . . . 16 |- 1 e. RR
75		cjre 11899	. . . . . . . . . . . . . . . 16 |- ( 1 e. RR -> ( * ` 1 ) = 1 )
76	74, 75	ax-mp 8	. . . . . . . . . . . . . . 15 |- ( * ` 1 ) = 1
77	73, 76	syl6eq 2452	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = 1 )
78	77	oveq1d 6055	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = ( 1 x. 1 ) )
79		1t1e1 10082	. . . . . . . . . . . . 13 |- ( 1 x. 1 ) = 1
80	78, 79	syl6eq 2452	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = 1 )
81	80	ifeq1da 3724	. . . . . . . . . . 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 2569	. . . . . . . . . . . . 13 |- ( f =/= .1. <-> -. f = .1. )
83		oveq2 6048	. . . . . . . . . . . . . . 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 6048	. . . . . . . . . . . . . . 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 3708	. . . . . . . . . . . . . 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 735	. . . . . . . . . . . . . . . . . . . . . 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 5691	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
89	86, 88	sylan 458	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
90	3, 8, 4	dchrmhm 20978	. . . . . . . . . . . . . . . . . . . . . . . 24 |- D C_ ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) )
91		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. D )
92	90, 91	sseldi 3306	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) )
93		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` Z ) = (mulGrp ` Z )
94		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1r ` Z ) = ( 1r ` Z )
95	93, 94	rngidval 15621	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1r ` Z ) = ( 0g ` (mulGrp ` Z ) )
96		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` ℂfld ) = (mulGrp ` ℂfld )
97		cnfld1 16681	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 = ( 1r ` ℂfld )
98	96, 97	rngidval 15621	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 = ( 0g ` (mulGrp ` ℂfld ) )
99	95, 98	mhm0 14701	. . . . . . . . . . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` ( 1r ` Z ) ) = 1 )
102	89, 101	eqtrd 2436	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = 1 )
103	102	fveq2d 5691	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
104	103, 76	syl6eq 2452	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = 1 )
105	104	oveq1d 6055	. . . . . . . . . . . . . . . . 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 9049	. . . . . . . . . . . . . . . . 17 |- ( 1 x. -u 1 ) = -u 1
107	105, 106	syl6eq 2452	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = -u 1 )
108	107	ifeq1da 3724	. . . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( * ` ( f ` A ) ) e. CC )
110	109	mul01d 9221	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( ( * ` ( f ` A ) ) x. 0 ) = 0 )
111	110	ifeq2d 3714	. . . . . . . . . . . . . . 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 2436	. . . . . . . . . . . . . 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 2448	. . . . . . . . . . . . 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 463	. . . . . . . . . . . 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 3725	. . . . . . . . . . 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 2436	. . . . . . . . . 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 2448	. . . . . . . . 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 6056	. . . . . . . 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 2436	. . . . . . 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 6058	. . . . . 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 2436	. . . . 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 12452	. . . 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 11267	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
124		inss1 3521	. . . . . . . . 9 |- ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) )
125		ssfi 7288	. . . . . . . . 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 644	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
127	2	phicld 13116	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. NN )
128	127	nncnd 9972	. . . . . . . 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 3308	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
131	130, 40	syldan 457	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( (Λ ` n ) / n ) e. CC )
132	126, 128, 131	fsummulc2 12522	. . . . . . 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 452	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( phi ` N ) e. CC )
134	133, 40	mulcld 9064	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
135	130, 134	syldan 457	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
136	135	ralrimiva 2749	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> A. n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
137	123	olcd 383	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` x ) ) e. Fin ) )
138		sumss2 12475	. . . . . . . 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 1183	. . . . . . 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 3490	. . . . . . . . . . . . 13 |- ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> ( n e. ( 1 ... ( |_ ` x ) ) /\ n e. T ) )
141	140	baib 872	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( |_ ` x ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
142	141	adantl 453	. . . . . . . . . . 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 2468	. . . . . . . . . . . 12 |- ( n e. T <-> n e. ( `' L " { A } ) )
145		ffn 5550	. . . . . . . . . . . . . 14 |- ( L : ZZ --> ( Base ` Z ) -> L Fn ZZ )
146	28, 145	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L Fn ZZ )
147		fniniseg 5810	. . . . . . . . . . . . . 14 |- ( L Fn ZZ -> ( n e. ( `' L " { A } ) <-> ( n e. ZZ /\ ( L ` n ) = A ) ) )
148	147	baibd 876	. . . . . . . . . . . . 13 |- ( ( L Fn ZZ /\ n e. ZZ ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
149	146, 29, 148	syl2an 464	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
150	144, 149	syl5bb 249	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. T <-> ( L ` n ) = A ) )
151	142, 150	bitr2d 246	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( L ` n ) = A <-> n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) )
152	40	mul02d 9220	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 x. ( (Λ ` n ) / n ) ) = 0 )
153	151, 152	ifbieq2d 3719	. . . . . . . . 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 6047	. . . . . . . . . . 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 6047	. . . . . . . . . . 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 3708	. . . . . . . . . 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 707	. . . . . . . . . . . . 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 696	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
160	33, 159	mulcld 9064	. . . . . . . . . . . 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 12523	. . . . . . . . . . 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 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. U )
163	3, 4, 8, 9, 12, 157, 31, 162	sum2dchr 21011	. . . . . . . . . . . 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 6055	. . . . . . . . . . 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 452	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( (Λ ` n ) / n ) e. CC )
166		mulass 9034	. . . . . . . . . . . . . 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 9188	. . . . . . . . . . . . . 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 2436	. . . . . . . . . . . . 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 1184	. . . . . . . . . . . 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 12452	. . . . . . . . . . 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 2444	. . . . . . . . . 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 2450	. . . . . . . . 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 2438	. . . . . . . 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 12452	. . . . . . 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 2440	. . . . . 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 12514	. . . . . 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 2436	. . . . 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 20991	. . . . . . . . . . 11 |- ( N e. NN -> G e. Abel )
179		ablgrp 15372	. . . . . . . . . . 11 |- ( G e. Abel -> G e. Grp )
180	2, 178, 179	3syl 19	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> G e. Grp )
181	4, 68	grpidcl 14788	. . . . . . . . . 10 |- ( G e. Grp -> .1. e. D )
182	180, 181	syl 16	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> .1. e. D )
183	48	mulid1d 9061	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
184	183, 48	eqeltrd 2478	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) e. CC )
185		iftrue 3705	. . . . . . . . . . 11 |- ( f = .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = 1 )
186	185	oveq2d 6056	. . . . . . . . . 10 |- ( f = .1. -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. 1 ) )
187	186	sumsn 12489	. . . . . . . . 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 ) )
188	182, 184, 187	syl2anc 643	. . . . . . . 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 ) )
189		eldifsn 3887	. . . . . . . . . . 11 |- ( f e. ( D \ { .1. } ) <-> ( f e. D /\ f =/= .1. ) )
190		ifnefalse 3707	. . . . . . . . . . . . . . 15 |- ( f =/= .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
191	190	ad2antll 710	. . . . . . . . . . . . . 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 ) )
192		negeq 9254	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 1 -> -u if ( f e. W , 1 , 0 ) = -u 1 )
193		negeq 9254	. . . . . . . . . . . . . . . 16 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = -u 0 )
194		neg0 9303	. . . . . . . . . . . . . . . 16 |- -u 0 = 0
195	193, 194	syl6eq 2452	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = 0 )
196	192, 195	ifsb 3708	. . . . . . . . . . . . . 14 |- -u if ( f e. W , 1 , 0 ) = if ( f e. W , -u 1 , 0 )
197	191, 196	syl6eqr 2454	. . . . . . . . . . . . 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 ) )
198	197	oveq2d 6056	. . . . . . . . . . . 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 ) ) )
199	48	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( log ` x ) e. CC )
200	50, 52	keepel 3756	. . . . . . . . . . . . 13 |- if ( f e. W , 1 , 0 ) e. CC
201		mulneg2 9427	. . . . . . . . . . . . 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 ) ) )
202	199, 200, 201	sylancl 644	. . . . . . . . . . . 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 ) ) )
203	198, 202	eqtrd 2436	. . . . . . . . . . 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 ) ) )
204	189, 203	sylan2b 462	. . . . . . . . . 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 ) ) )
205	204	sumeq2dv 12452	. . . . . . . . 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 ) ) )
206		diffi 7298	. . . . . . . . . . 11 |- ( D e. Fin -> ( D \ { .1. } ) e. Fin )
207	6, 206	syl 16	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( D \ { .1. } ) e. Fin )
208	48	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( log ` x ) e. CC )
209		mulcl 9030	. . . . . . . . . . 11 |- ( ( ( log ` x ) e. CC /\ if ( f e. W , 1 , 0 ) e. CC ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
210	208, 200, 209	sylancl 644	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
211	207, 210	fsumneg 12525	. . . . . . . . 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 ) ) )
212	200	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> if ( f e. W , 1 , 0 ) e. CC )
213	207, 48, 212	fsummulc2 12522	. . . . . . . . . . 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 ) ) )
214		rpvmasum2.w	. . . . . . . . . . . . . . . . 17 |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
215		ssrab2 3388	. . . . . . . . . . . . . . . . 17 |- { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } C_ ( D \ { .1. } )
216	214, 215	eqsstri 3338	. . . . . . . . . . . . . . . 16 |- W C_ ( D \ { .1. } )
217		difss 3434	. . . . . . . . . . . . . . . 16 |- ( D \ { .1. } ) C_ D
218	216, 217	sstri 3317	. . . . . . . . . . . . . . 15 |- W C_ D
219		ssfi 7288	. . . . . . . . . . . . . . 15 |- ( ( D e. Fin /\ W C_ D ) -> W e. Fin )
220	6, 218, 219	sylancl 644	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W e. Fin )
221		fsumconst 12528	. . . . . . . . . . . . . 14 |- ( ( W e. Fin /\ 1 e. CC ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
222	220, 50, 221	sylancl 644	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
223	216	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W C_ ( D \ { .1. } ) )
224	50	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> 1 e. CC )
225	224	ralrimivw 2750	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> A. f e. W 1 e. CC )
226	207	olcd 383	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( ( D \ { .1. } ) C_ ( ZZ>= ` 1 ) \/ ( D \ { .1. } ) e. Fin ) )
227		sumss2 12475	. . . . . . . . . . . . . 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 ) )
228	223, 225, 226, 227	syl21anc 1183	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) )
229		hashcl 11594	. . . . . . . . . . . . . . . 16 |- ( W e. Fin -> ( # ` W ) e. NN0 )
230	220, 229	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. NN0 )
231	230	nn0cnd 10232	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. CC )
232	231	mulid1d 9061	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> ( ( # ` W ) x. 1 ) = ( # ` W ) )
233	222, 228, 232	3eqtr3d 2444	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) = ( # ` W ) )
234	233	oveq2d 6056	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
235	213, 234	eqtr3d 2438	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
236	235	negeqd 9256	. . . . . . . . 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 ) ) )
237	205, 211, 236	3eqtrd 2440	. . . . . . . 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 ) ) )
238	188, 237	oveq12d 6058	. . . . . . 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 ) ) ) )
239	48, 231	mulcld 9064	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( # ` W ) ) e. CC )
240	184, 239	negsubd 9373	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( ( ( log ` x ) x. 1 ) + -u ( ( log ` x ) x. ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
241	238, 240	eqtrd 2436	. . . . . 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 ) ) ) )
242		disjdif 3660	. . . . . . . 8 |- ( { .1. } i^i ( D \ { .1. } ) ) = (/)
243	242	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } i^i ( D \ { .1. } ) ) = (/) )
244		undif2 3664	. . . . . . . 8 |- ( { .1. } u. ( D \ { .1. } ) ) = ( { .1. } u. D )
245	182	snssd 3903	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> { .1. } C_ D )
246		ssequn1 3477	. . . . . . . . 9 |- ( { .1. } C_ D <-> ( { .1. } u. D ) = D )
247	245, 246	sylib 189	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } u. D ) = D )
248	244, 247	syl5req 2449	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> D = ( { .1. } u. ( D \ { .1. } ) ) )
249	243, 248, 6, 56	fsumsplit 12488	. . . . . 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 ) ) ) ) )
250	48, 224, 231	subdid 9445	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
251	241, 249, 250	3eqtr4rd 2447	. . . . 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 ) ) ) )
252	177, 251	oveq12d 6058	. . . 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 ) ) ) ) )
253	57, 122, 252	3eqtr4d 2446	. . 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 ) ) ) ) )
254	253	mpteq2dva 4255	. 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 ) ) ) ) ) )
255		rpssre 10578	. . . 4 |- RR+ C_ RR
256	255	a1i 11	. . 3 |- ( ph -> RR+ C_ RR )
257	1, 5	syl 16	. . 3 |- ( ph -> D e. Fin )
258	17	adantlr 696	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` A ) e. CC )
259	258	cjcld 11956	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
260	59, 56	subcld 9367	. . . . 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 )
261	259, 260	mulcld 9064	. . . 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 )
262	261	anasss 629	. . 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 )
263	18	adantr 452	. . . 4 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( * ` ( f ` A ) ) e. CC )
264	260	an32s 780	. . . 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 )
265		o1const 12368	. . . . 5 |- ( ( RR+ C_ RR /\ ( * ` ( f ` A ) ) e. CC ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O ( 1 ) )
266	255, 18, 265	sylancr 645	. . . 4 |- ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O ( 1 ) )
267		fveq1 5686	. . . . . . . . . . . 12 |- ( f = .1. -> ( f ` ( L ` n ) ) = ( .1. ` ( L ` n ) ) )
268	267	oveq1d 6055	. . . . . . . . . . 11 |- ( f = .1. -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) = ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) )
269	268	sumeq2sdv 12453	. . . . . . . . . 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 ) ) )
270	269, 186	oveq12d 6058	. . . . . . . . 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 ) ) )
271	270	adantl 453	. . . . . . . 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 ) ) )
272	46	recnd 9070	. . . . . . . . . 10 |- ( x e. RR+ -> ( log ` x ) e. CC )
273	272	mulid1d 9061	. . . . . . . . 9 |- ( x e. RR+ -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
274	273	oveq2d 6056	. . . . . . . 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 ) ) )
275	271, 274	sylan9eq 2456	. . . . . . 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 ) ) )
276	275	mpteq2dva 4255	. . . . . 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 ) ) ) )
277	8, 24, 1, 3, 4, 68	rpvmasumlem 21134	. . . . . . 7 |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) e. O ( 1 ) )
278	277	ad2antrr 707	. . . . . 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 ) )
279	276, 278	eqeltrd 2478	. . . . 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 ) )
280	190	oveq2d 6056	. . . . . . . . . 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 ) ) )
281	280	oveq2d 6056	. . . . . . . . 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 ) ) ) )
282	48	adantlr 696	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
283		mulcom 9032	. . . . . . . . . . . . . . 15 |- ( ( ( log ` x ) e. CC /\ -u 1 e. CC ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
284	282, 51, 283	sylancl 644	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
285	282	mulm1d 9441	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( -u 1 x. ( log ` x ) ) = -u ( log ` x ) )
286	284, 285	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = -u ( log ` x ) )
287	282	mul01d 9221	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. 0 ) = 0 )
288	286, 287	ifeq12d 3715	. . . . . . . . . . . 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 ) )
289		oveq2 6048	. . . . . . . . . . . . 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 ) )
290		oveq2 6048	. . . . . . . . . . . . 13 |- ( if ( f e. W , -u 1 , 0 ) = 0 -> ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = ( ( log ` x ) x. 0 ) )
291	289, 290	ifsb 3708	. . . . . . . . . . . 12 |- ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( log ` x ) x. -u 1 ) , ( ( log ` x ) x. 0 ) )
292		negeq 9254	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = ( log ` x ) -> -u if ( f e. W , ( log ` x ) , 0 ) = -u ( log ` x ) )
293		negeq 9254	. . . . . . . . . . . . . 14 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = -u 0 )
294	293, 194	syl6eq 2452	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = 0 )
295	292, 294	ifsb 3708	. . . . . . . . . . . 12 |- -u if ( f e. W , ( log ` x ) , 0 ) = if ( f e. W , -u ( log ` x ) , 0 )
296	288, 291, 295	3eqtr4g 2461	. . . . . . . . . . 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 ) )
297	296	oveq2d 6056	. . . . . . . . . 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 ) ) )
298	59	an32s 780	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
299		ifcl 3735	. . . . . . . . . . . 12 |- ( ( ( log ` x ) e. CC /\ 0 e. CC ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
300	282, 52, 299	sylancl 644	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
301	298, 300	subnegd 9374	. . . . . . . . . 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 ) ) )
302	297, 301	eqtrd 2436	. . . . . . . . 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 ) ) )
303	281, 302	sylan9eqr 2458	. . . . . . . 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 ) ) )
304	303	an32s 780	. . . . . . 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 ) ) )
305	304	mpteq2dva 4255	. . . . . 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 ) ) ) )
306	1	ad2antrr 707	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> N e. NN )
307		simplr 732	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f e. D )
308		simpr 448	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f =/= .1. )
309		eqid 2404	. . . . . . . 8 |- ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) = ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) )
310	8, 24, 306, 3, 4, 68, 307, 308, 309	dchrmusumlema 21140	. . . . . . 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 ) ) )
311	1	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> N e. NN )
312	311	ad2antrr 707	. . . . . . . . . . . 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 )
313	307	adantr 452	. . . . . . . . . . . 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 )
314		simplr 732	. . . . . . . . . . . 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. )
315		simprl 733	. . . . . . . . . . . 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 ) )
316		simprrl 741	. . . . . . . . . . . 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 )
317		simprrr 742	. . . . . . . . . . . 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 ) )
318	8, 24, 312, 3, 4, 68, 313, 314, 309, 315, 316, 317, 214	dchrvmaeq0 21151	. . . . . . . . . . 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 ) )
319		ifbi 3716	. . . . . . . . . . . . 13 |- ( ( f e. W <-> t = 0 ) -> if ( f e. W , ( log ` x ) , 0 ) = if ( t = 0 , ( log ` x ) , 0 ) )
320	319	oveq2d 6056	. . . . . . . . . . . 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 ) ) )
321	320	mpteq2dv 4256	. . . . . . . . . . 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 ) ) ) )
322	318, 321	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. (