Theorem rpvmasum2 24350

Description: A partial result along the lines of rpvmasum 24364. 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 467	. . . . . 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 24183	. . . . . 6 |- ( N e. NN -> D e. Fin )
6	2, 5	syl 17	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> D e. Fin )
7		fzfid 12186	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
8		rpvmasum.z	. . . . . . . . . . . . 13 |- Z = (ℤ/nℤ ` N )
9		eqid 2451	. . . . . . . . . . . . 13 |- ( Base ` Z ) = ( Base ` Z )
10		simpr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> f e. D )
11	3, 8, 4, 9, 10	dchrf 24170	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> f : ( Base ` Z ) --> CC )
12		rpvmasum2.u	. . . . . . . . . . . . . . 15 |- U = (Unit ` Z )
13	9, 12	unitss 17888	. . . . . . . . . . . . . 14 |- U C_ ( Base ` Z )
14		rpvmasum2.b	. . . . . . . . . . . . . 14 |- ( ph -> A e. U )
15	13, 14	sseldi 3430	. . . . . . . . . . . . 13 |- ( ph -> A e. ( Base ` Z ) )
16	15	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> A e. ( Base ` Z ) )
17	11, 16	ffvelrnd 6023	. . . . . . . . . . 11 |- ( ( ph /\ f e. D ) -> ( f ` A ) e. CC )
18	17	cjcld 13259	. . . . . . . . . 10 |- ( ( ph /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
19	18	adantlr 721	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
20	19	adantrl 722	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( * ` ( f ` A ) ) e. CC )
21	11	adantlr 721	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
22	21	adantlr 721	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
23	1	nnnn0d 10925	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
24		rpvmasum.l	. . . . . . . . . . . . . . . 16 |- L = ( ZRHom ` Z )
25	8, 9, 24	znzrhfo 19118	. . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . 14 |- ( ph -> L : ZZ --> ( Base ` Z ) )
28	27	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L : ZZ --> ( Base ` Z ) )
29		elfzelz 11800	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
30		ffvelrn 6020	. . . . . . . . . . . . 13 |- ( ( L : ZZ --> ( Base ` Z ) /\ n e. ZZ ) -> ( L ` n ) e. ( Base ` Z ) )
31	28, 29, 30	syl2an 480	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` n ) e. ( Base ` Z ) )
32	31	adantr 467	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( L ` n ) e. ( Base ` Z ) )
33	22, 32	ffvelrnd 6023	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( f ` ( L ` n ) ) e. CC )
34	33	anasss 653	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( f ` ( L ` n ) ) e. CC )
35		elfznn 11828	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
36	35	adantl 468	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
37		vmacl 24045	. . . . . . . . . . . . 13 |- ( n e. NN -> (Λ ` n ) e. RR )
38	36, 37	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (Λ ` n ) e. RR )
39	38, 36	nndivred 10658	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. RR )
40	39	recnd 9669	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. CC )
41	40	adantrr 723	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( (Λ ` n ) / n ) e. CC )
42	34, 41	mulcld 9663	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
43	20, 42	mulcld 9663	. . . . . . 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 816	. . . . . 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 13799	. . . . 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 23525	. . . . . . . . 9 |- ( x e. RR+ -> ( log ` x ) e. RR )
47	46	adantl 468	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
48	47	recnd 9669	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
49	48	adantr 467	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( log ` x ) e. CC )
50		ax-1cn 9597	. . . . . . 7 |- 1 e. CC
51		neg1cn 10713	. . . . . . . 8 |- -u 1 e. CC
52		0cn 9635	. . . . . . . 8 |- 0 e. CC
53	51, 52	keepel 3948	. . . . . . 7 |- if ( f e. W , -u 1 , 0 ) e. CC
54	50, 53	keepel 3948	. . . . . 6 |- if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC
55		mulcl 9623	. . . . . 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 668	. . . . 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 13849	. . . 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 816	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
59	7, 58	fsumcl 13799	. . . . . . 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 10074	. . . . . 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 13845	. . . . . . 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 9842	. . . . . . . 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		ovif2 6374	. . . . . . . . . 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 ) ) )
65		fveq1 5864	. . . . . . . . . . . . . . . . 17 |- ( f = .1. -> ( f ` A ) = ( .1. ` A ) )
66		rpvmasum2.1	. . . . . . . . . . . . . . . . . 18 |- .1. = ( 0g ` G )
67	1	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> N e. NN )
68	14	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> A e. U )
69	3, 8, 66, 12, 67, 68	dchr1 24185	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( .1. ` A ) = 1 )
70	65, 69	sylan9eqr 2507	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( f ` A ) = 1 )
71	70	fveq2d 5869	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
72		1re 9642	. . . . . . . . . . . . . . . 16 |- 1 e. RR
73		cjre 13202	. . . . . . . . . . . . . . . 16 |- ( 1 e. RR -> ( * ` 1 ) = 1 )
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( * ` 1 ) = 1
75	71, 74	syl6eq 2501	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = 1 )
76	75	oveq1d 6305	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = ( 1 x. 1 ) )
77		1t1e1 10757	. . . . . . . . . . . . 13 |- ( 1 x. 1 ) = 1
78	76, 77	syl6eq 2501	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = 1 )
79	78	ifeq1da 3911	. . . . . . . . . . 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 ) ) ) )
80		df-ne 2624	. . . . . . . . . . . . 13 |- ( f =/= .1. <-> -. f = .1. )
81		ovif2 6374	. . . . . . . . . . . . . 14 |- ( ( * ` ( f ` A ) ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( * ` ( f ` A ) ) x. -u 1 ) , ( ( * ` ( f ` A ) ) x. 0 ) )
82		simplll 768	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ph )
83		rpvmasum2.z1	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ f e. W ) -> A = ( 1r ` Z ) )
84	83	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
85	82, 84	sylan 474	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
86	3, 8, 4	dchrmhm 24169	. . . . . . . . . . . . . . . . . . . . . . . 24 |- D C_ ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) )
87		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. D )
88	86, 87	sseldi 3430	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) )
89		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` Z ) = (mulGrp ` Z )
90		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1r ` Z ) = ( 1r ` Z )
91	89, 90	ringidval 17737	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1r ` Z ) = ( 0g ` (mulGrp ` Z ) )
92		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` ℂfld ) = (mulGrp ` ℂfld )
93		cnfld1 18993	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 = ( 1r ` ℂfld )
94	92, 93	ringidval 17737	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 = ( 0g ` (mulGrp ` ℂfld ) )
95	91, 94	mhm0 16590	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) -> ( f ` ( 1r ` Z ) ) = 1 )
96	88, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` ( 1r ` Z ) ) = 1 )
97	96	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` ( 1r ` Z ) ) = 1 )
98	85, 97	eqtrd 2485	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = 1 )
99	98	fveq2d 5869	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
100	99, 74	syl6eq 2501	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = 1 )
101	100	oveq1d 6305	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = ( 1 x. -u 1 ) )
102	51	mulid2i 9646	. . . . . . . . . . . . . . . . 17 |- ( 1 x. -u 1 ) = -u 1
103	101, 102	syl6eq 2501	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = -u 1 )
104	103	ifeq1da 3911	. . . . . . . . . . . . . . 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 ) ) )
105	19	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( * ` ( f ` A ) ) e. CC )
106	105	mul01d 9832	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( ( * ` ( f ` A ) ) x. 0 ) = 0 )
107	106	ifeq2d 3900	. . . . . . . . . . . . . . 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 ) )
108	104, 107	eqtrd 2485	. . . . . . . . . . . . . 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 ) )
109	81, 108	syl5eq 2497	. . . . . . . . . . . . 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 ) )
110	80, 109	sylan2br 479	. . . . . . . . . . . 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 ) )
111	110	ifeq2da 3912	. . . . . . . . . . 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 ) ) )
112	79, 111	eqtrd 2485	. . . . . . . . . 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 ) ) )
113	64, 112	syl5eq 2497	. . . . . . . . 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 ) ) )
114	113	oveq2d 6306	. . . . . . . 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 ) ) ) )
115	63, 114	eqtrd 2485	. . . . . . 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 ) ) ) )
116	61, 115	oveq12d 6308	. . . . . 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 ) ) ) ) )
117	60, 116	eqtrd 2485	. . . . 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 ) ) ) ) )
118	117	sumeq2dv 13769	. . . 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 ) ) ) ) )
119		fzfid 12186	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
120		inss1 3652	. . . . . . . . 9 |- ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) )
121		ssfi 7792	. . . . . . . . 9 |- ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
122	119, 120, 121	sylancl 668	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
123	2	phicld 14720	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. NN )
124	123	nncnd 10625	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. CC )
125	120	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) )
126	125	sselda 3432	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
127	126, 40	syldan 473	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( (Λ ` n ) / n ) e. CC )
128	122, 124, 127	fsummulc2 13845	. . . . . . 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 ) ) )
129	124	adantr 467	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( phi ` N ) e. CC )
130	129, 40	mulcld 9663	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
131	126, 130	syldan 473	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
132	131	ralrimiva 2802	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> A. n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
133	119	olcd 395	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` x ) ) e. Fin ) )
134		sumss2 13792	. . . . . . . 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 ) )
135	125, 132, 133, 134	syl21anc 1267	. . . . . . 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 ) )
136		elin 3617	. . . . . . . . . . . . 13 |- ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> ( n e. ( 1 ... ( |_ ` x ) ) /\ n e. T ) )
137	136	baib 914	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( |_ ` x ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
138	137	adantl 468	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
139		rpvmasum2.t	. . . . . . . . . . . . 13 |- T = ( `' L " { A } )
140	139	eleq2i 2521	. . . . . . . . . . . 12 |- ( n e. T <-> n e. ( `' L " { A } ) )
141		ffn 5728	. . . . . . . . . . . . . 14 |- ( L : ZZ --> ( Base ` Z ) -> L Fn ZZ )
142	28, 141	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L Fn ZZ )
143		fniniseg 6003	. . . . . . . . . . . . . 14 |- ( L Fn ZZ -> ( n e. ( `' L " { A } ) <-> ( n e. ZZ /\ ( L ` n ) = A ) ) )
144	143	baibd 920	. . . . . . . . . . . . 13 |- ( ( L Fn ZZ /\ n e. ZZ ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
145	142, 29, 144	syl2an 480	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
146	140, 145	syl5bb 261	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. T <-> ( L ` n ) = A ) )
147	138, 146	bitr2d 258	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( L ` n ) = A <-> n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) )
148	40	mul02d 9831	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 x. ( (Λ ` n ) / n ) ) = 0 )
149	147, 148	ifbieq2d 3906	. . . . . . . . 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 ) )
150		ovif 6373	. . . . . . . . . 10 |- ( if ( ( L ` n ) = A , ( phi ` N ) , 0 ) x. ( (Λ ` n ) / n ) ) = if ( ( L ` n ) = A , ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) , ( 0 x. ( (Λ ` n ) / n ) ) )
151	1	ad2antrr 732	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> N e. NN )
152	151, 5	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> D e. Fin )
153	19	adantlr 721	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
154	33, 153	mulcld 9663	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( ( f ` ( L ` n ) ) x. ( * ` ( f ` A ) ) ) e. CC )
155	152, 40, 154	fsummulc1 13846	. . . . . . . . . . 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 ) ) )
156	14	ad2antrr 732	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. U )
157	3, 4, 8, 9, 12, 151, 31, 156	sum2dchr 24202	. . . . . . . . . . . 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 ) )
158	157	oveq1d 6305	. . . . . . . . . . 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 ) ) )
159	40	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( (Λ ` n ) / n ) e. CC )
160		mulass 9627	. . . . . . . . . . . . . 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 ) ) ) )
161		mul12 9799	. . . . . . . . . . . . . 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 ) ) ) )
162	160, 161	eqtrd 2485	. . . . . . . . . . . . 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 ) ) ) )
163	33, 153, 159, 162	syl3anc 1268	. . . . . . . . . . . 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 ) ) ) )
164	163	sumeq2dv 13769	. . . . . . . . . . 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 ) ) ) )
165	155, 158, 164	3eqtr3d 2493	. . . . . . . . . 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 ) ) ) )
166	150, 165	syl5eqr 2499	. . . . . . . . 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 ) ) ) )
167	149, 166	eqtr3d 2487	. . . . . . . 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 ) ) ) )
168	167	sumeq2dv 13769	. . . . . . 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 ) ) ) )
169	128, 135, 168	3eqtrd 2489	. . . . . 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 ) ) ) )
170	119, 6, 43	fsumcom 13836	. . . . . 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 ) ) ) )
171	169, 170	eqtrd 2485	. . . . 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 ) ) ) )
172	3	dchrabl 24182	. . . . . . . . . 10 |- ( N e. NN -> G e. Abel )
173		ablgrp 17435	. . . . . . . . . 10 |- ( G e. Abel -> G e. Grp )
174	4, 66	grpidcl 16694	. . . . . . . . . 10 |- ( G e. Grp -> .1. e. D )
175	2, 172, 173, 174	4syl 19	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> .1. e. D )
176	48	mulid1d 9660	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
177	176, 48	eqeltrd 2529	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) e. CC )
178		iftrue 3887	. . . . . . . . . . 11 |- ( f = .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = 1 )
179	178	oveq2d 6306	. . . . . . . . . 10 |- ( f = .1. -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. 1 ) )
180	179	sumsn 13807	. . . . . . . . 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 ) )
181	175, 177, 180	syl2anc 667	. . . . . . . 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 ) )
182		eldifsn 4097	. . . . . . . . . . 11 |- ( f e. ( D \ { .1. } ) <-> ( f e. D /\ f =/= .1. ) )
183		ifnefalse 3893	. . . . . . . . . . . . . . 15 |- ( f =/= .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
184	183	ad2antll 735	. . . . . . . . . . . . . 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 ) )
185		negeq 9867	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 1 -> -u if ( f e. W , 1 , 0 ) = -u 1 )
186		negeq 9867	. . . . . . . . . . . . . . . 16 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = -u 0 )
187		neg0 9920	. . . . . . . . . . . . . . . 16 |- -u 0 = 0
188	186, 187	syl6eq 2501	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = 0 )
189	185, 188	ifsb 3894	. . . . . . . . . . . . . 14 |- -u if ( f e. W , 1 , 0 ) = if ( f e. W , -u 1 , 0 )
190	184, 189	syl6eqr 2503	. . . . . . . . . . . . 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 ) )
191	190	oveq2d 6306	. . . . . . . . . . . 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 ) ) )
192	48	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( log ` x ) e. CC )
193	50, 52	keepel 3948	. . . . . . . . . . . . 13 |- if ( f e. W , 1 , 0 ) e. CC
194		mulneg2 10056	. . . . . . . . . . . . 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 ) ) )
195	192, 193, 194	sylancl 668	. . . . . . . . . . . 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 ) ) )
196	191, 195	eqtrd 2485	. . . . . . . . . . 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 ) ) )
197	182, 196	sylan2b 478	. . . . . . . . . 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 ) ) )
198	197	sumeq2dv 13769	. . . . . . . . 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 ) ) )
199		diffi 7803	. . . . . . . . . . 11 |- ( D e. Fin -> ( D \ { .1. } ) e. Fin )
200	6, 199	syl 17	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( D \ { .1. } ) e. Fin )
201	48	adantr 467	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( log ` x ) e. CC )
202		mulcl 9623	. . . . . . . . . . 11 |- ( ( ( log ` x ) e. CC /\ if ( f e. W , 1 , 0 ) e. CC ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
203	201, 193, 202	sylancl 668	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
204	200, 203	fsumneg 13848	. . . . . . . . 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 ) ) )
205	193	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> if ( f e. W , 1 , 0 ) e. CC )
206	200, 48, 205	fsummulc2 13845	. . . . . . . . . . 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 ) ) )
207		rpvmasum2.w	. . . . . . . . . . . . . . . . 17 |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
208		ssrab2 3514	. . . . . . . . . . . . . . . . 17 |- { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } C_ ( D \ { .1. } )
209	207, 208	eqsstri 3462	. . . . . . . . . . . . . . . 16 |- W C_ ( D \ { .1. } )
210		difss 3560	. . . . . . . . . . . . . . . 16 |- ( D \ { .1. } ) C_ D
211	209, 210	sstri 3441	. . . . . . . . . . . . . . 15 |- W C_ D
212		ssfi 7792	. . . . . . . . . . . . . . 15 |- ( ( D e. Fin /\ W C_ D ) -> W e. Fin )
213	6, 211, 212	sylancl 668	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W e. Fin )
214		fsumconst 13851	. . . . . . . . . . . . . 14 |- ( ( W e. Fin /\ 1 e. CC ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
215	213, 50, 214	sylancl 668	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
216	209	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W C_ ( D \ { .1. } ) )
217	50	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> 1 e. CC )
218	217	ralrimivw 2803	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> A. f e. W 1 e. CC )
219	200	olcd 395	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( ( D \ { .1. } ) C_ ( ZZ>= ` 1 ) \/ ( D \ { .1. } ) e. Fin ) )
220		sumss2 13792	. . . . . . . . . . . . . 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 ) )
221	216, 218, 219, 220	syl21anc 1267	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) )
222		hashcl 12538	. . . . . . . . . . . . . . . 16 |- ( W e. Fin -> ( # ` W ) e. NN0 )
223	213, 222	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. NN0 )
224	223	nn0cnd 10927	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. CC )
225	224	mulid1d 9660	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> ( ( # ` W ) x. 1 ) = ( # ` W ) )
226	215, 221, 225	3eqtr3d 2493	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) = ( # ` W ) )
227	226	oveq2d 6306	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
228	206, 227	eqtr3d 2487	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) = ( ( log ` x ) x. ( # ` W ) ) )
229	228	negeqd 9869	. . . . . . . . 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 ) ) )
230	198, 204, 229	3eqtrd 2489	. . . . . . . 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 ) ) )
231	181, 230	oveq12d 6308	. . . . . . 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 ) ) ) )
232	48, 224	mulcld 9663	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( # ` W ) ) e. CC )
233	177, 232	negsubd 9992	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( ( ( log ` x ) x. 1 ) + -u ( ( log ` x ) x. ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
234	231, 233	eqtrd 2485	. . . . . 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 ) ) ) )
235		disjdif 3839	. . . . . . . 8 |- ( { .1. } i^i ( D \ { .1. } ) ) = (/)
236	235	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } i^i ( D \ { .1. } ) ) = (/) )
237		undif2 3843	. . . . . . . 8 |- ( { .1. } u. ( D \ { .1. } ) ) = ( { .1. } u. D )
238	175	snssd 4117	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> { .1. } C_ D )
239		ssequn1 3604	. . . . . . . . 9 |- ( { .1. } C_ D <-> ( { .1. } u. D ) = D )
240	238, 239	sylib 200	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } u. D ) = D )
241	237, 240	syl5req 2498	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> D = ( { .1. } u. ( D \ { .1. } ) ) )
242	236, 241, 6, 56	fsumsplit 13806	. . . . . 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 ) ) ) ) )
243	48, 217, 224	subdid 10074	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
244	234, 242, 243	3eqtr4rd 2496	. . . . 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 ) ) ) )
245	171, 244	oveq12d 6308	. . . 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 ) ) ) ) )
246	57, 118, 245	3eqtr4d 2495	. . 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 ) ) ) ) )
247	246	mpteq2dva 4489	. 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 ) ) ) ) ) )
248		rpssre 11312	. . . 4 |- RR+ C_ RR
249	248	a1i 11	. . 3 |- ( ph -> RR+ C_ RR )
250	1, 5	syl 17	. . 3 |- ( ph -> D e. Fin )
251	17	adantlr 721	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` A ) e. CC )
252	251	cjcld 13259	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
253	59, 56	subcld 9986	. . . . 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 )
254	252, 253	mulcld 9663	. . . 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 )
255	254	anasss 653	. . 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 )
256	18	adantr 467	. . . 4 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( * ` ( f ` A ) ) e. CC )
257	253	an32s 813	. . . 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 )
258		o1const 13683	. . . . 5 |- ( ( RR+ C_ RR /\ ( * ` ( f ` A ) ) e. CC ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O(1) )
259	248, 18, 258	sylancr 669	. . . 4 |- ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O(1) )
260		fveq1 5864	. . . . . . . . . . . 12 |- ( f = .1. -> ( f ` ( L ` n ) ) = ( .1. ` ( L ` n ) ) )
261	260	oveq1d 6305	. . . . . . . . . . 11 |- ( f = .1. -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) = ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) )
262	261	sumeq2sdv 13770	. . . . . . . . . 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 ) ) )
263	262, 179	oveq12d 6308	. . . . . . . . 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 ) ) )
264	263	adantl 468	. . . . . . . 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 ) ) )
265	46	recnd 9669	. . . . . . . . . 10 |- ( x e. RR+ -> ( log ` x ) e. CC )
266	265	mulid1d 9660	. . . . . . . . 9 |- ( x e. RR+ -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
267	266	oveq2d 6306	. . . . . . . 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 ) ) )
268	264, 267	sylan9eq 2505	. . . . . . 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 ) ) )
269	268	mpteq2dva 4489	. . . . . 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 ) ) ) )
270	8, 24, 1, 3, 4, 66	rpvmasumlem 24325	. . . . . . 7 |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
271	270	ad2antrr 732	. . . . . 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) )
272	269, 271	eqeltrd 2529	. . . . 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) )
273	183	oveq2d 6306	. . . . . . . . . 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 ) ) )
274	273	oveq2d 6306	. . . . . . . . 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 ) ) ) )
275	48	adantlr 721	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
276		mulcom 9625	. . . . . . . . . . . . . . 15 |- ( ( ( log ` x ) e. CC /\ -u 1 e. CC ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
277	275, 51, 276	sylancl 668	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
278	275	mulm1d 10070	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( -u 1 x. ( log ` x ) ) = -u ( log ` x ) )
279	277, 278	eqtrd 2485	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = -u ( log ` x ) )
280	275	mul01d 9832	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. 0 ) = 0 )
281	279, 280	ifeq12d 3901	. . . . . . . . . . . 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 ) )
282		ovif2 6374	. . . . . . . . . . . 12 |- ( ( log ` x ) x. if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , ( ( log ` x ) x. -u 1 ) , ( ( log ` x ) x. 0 ) )
283		negeq 9867	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = ( log ` x ) -> -u if ( f e. W , ( log ` x ) , 0 ) = -u ( log ` x ) )
284		negeq 9867	. . . . . . . . . . . . . 14 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = -u 0 )
285	284, 187	syl6eq 2501	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = 0 )
286	283, 285	ifsb 3894	. . . . . . . . . . . 12 |- -u if ( f e. W , ( log ` x ) , 0 ) = if ( f e. W , -u ( log ` x ) , 0 )
287	281, 282, 286	3eqtr4g 2510	. . . . . . . . . . 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 ) )
288	287	oveq2d 6306	. . . . . . . . . 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 ) ) )
289	59	an32s 813	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
290		ifcl 3923	. . . . . . . . . . . 12 |- ( ( ( log ` x ) e. CC /\ 0 e. CC ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
291	275, 52, 290	sylancl 668	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
292	289, 291	subnegd 9993	. . . . . . . . . 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 ) ) )
293	288, 292	eqtrd 2485	. . . . . . . . 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 ) ) )
294	274, 293	sylan9eqr 2507	. . . . . . . 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 ) ) )
295	294	an32s 813	. . . . . . 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 ) ) )
296	295	mpteq2dva 4489	. . . . . 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 ) ) ) )
297	1	ad2antrr 732	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> N e. NN )
298		simplr 762	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f e. D )
299		simpr 463	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f =/= .1. )
300		eqid 2451	. . . . . . . 8 |- ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) = ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) )
301	8, 24, 297, 3, 4, 66, 298, 299, 300	dchrmusumlema 24331	. . . . . . 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 ) ) )
302	1	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> N e. NN )
303	302	ad2antrr 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 ) ) ) ) -> N e. NN )
304	298	adantr 467	. . . . . . . . . . . 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 )
305		simplr 762	. . . . . . . . . . . 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. )
306		simprl 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 ) ) ) ) -> c e. ( 0 [,) +oo ) )
307		simprrl 774	. . . . . . . . . . . 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 )
308		simprrr 775	. . . . . . . . . . . 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 ) )
309	8, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308, 207	dchrvmaeq0 24342	. . . . . . . . . . 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 ) )
310		ifbi 3902	. . . . . . . . . . . . 13 |- ( ( f e. W <-> t = 0 ) -> if ( f e. W , ( log ` x ) , 0 ) = if ( t = 0 , ( log ` x ) , 0 ) )
311	310	oveq2d 6306	. . . . . . . . . . . 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 ) ) )
312	311	mpteq2dv 4490	. . . . . . . . . . 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 ) ) ) )
313	309, 312	syl 17	. . . . . . . . . 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 |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( 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 ) ) ) )
314	8, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308	dchrvmasumif 24341	. . . . . . . . . 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 |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( t = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )
315	313, 314	eqeltrd 2529	. . . . . . . . 9 |- ( ( ( ( ph /\ f e. D ) /\ f =/= .1. ) /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) e. O(1) )
316	315	rexlimdvaa 2880	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( E. c e. ( 0 [,) +oo ) (