Theorem rpvmasum2 25201

Description: A partial result along the lines of rpvmasum 25215. 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 481	. . . . . 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 24980	. . . . . 6 |- ( N e. NN -> D e. Fin )
6	2, 5	syl 17	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> D e. Fin )
7		fzfid 12772	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
8		rpvmasum.z	. . . . . . . . . . . . 13 |- Z = (ℤ/nℤ ` N )
9		eqid 2622	. . . . . . . . . . . . 13 |- ( Base ` Z ) = ( Base ` Z )
10		simpr 477	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> f e. D )
11	3, 8, 4, 9, 10	dchrf 24967	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> f : ( Base ` Z ) --> CC )
12		rpvmasum2.u	. . . . . . . . . . . . . . 15 |- U = (Unit ` Z )
13	9, 12	unitss 18660	. . . . . . . . . . . . . 14 |- U C_ ( Base ` Z )
14		rpvmasum2.b	. . . . . . . . . . . . . 14 |- ( ph -> A e. U )
15	13, 14	sseldi 3601	. . . . . . . . . . . . 13 |- ( ph -> A e. ( Base ` Z ) )
16	15	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ f e. D ) -> A e. ( Base ` Z ) )
17	11, 16	ffvelrnd 6360	. . . . . . . . . . 11 |- ( ( ph /\ f e. D ) -> ( f ` A ) e. CC )
18	17	cjcld 13936	. . . . . . . . . 10 |- ( ( ph /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
19	18	adantlr 751	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
20	19	adantrl 752	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( * ` ( f ` A ) ) e. CC )
21	11	adantlr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
22	21	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> f : ( Base ` Z ) --> CC )
23	1	nnnn0d 11351	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
24		rpvmasum.l	. . . . . . . . . . . . . . . 16 |- L = ( ZRHom ` Z )
25	8, 9, 24	znzrhfo 19896	. . . . . . . . . . . . . . 15 |- ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
26		fof 6115	. . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L : ZZ --> ( Base ` Z ) )
29		elfzelz 12342	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
30		ffvelrn 6357	. . . . . . . . . . . . 13 |- ( ( L : ZZ --> ( Base ` Z ) /\ n e. ZZ ) -> ( L ` n ) e. ( Base ` Z ) )
31	28, 29, 30	syl2an 494	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` n ) e. ( Base ` Z ) )
32	31	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( L ` n ) e. ( Base ` Z ) )
33	22, 32	ffvelrnd 6360	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( f ` ( L ` n ) ) e. CC )
34	33	anasss 679	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( f ` ( L ` n ) ) e. CC )
35		elfznn 12370	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
36	35	adantl 482	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
37		vmacl 24844	. . . . . . . . . . . . 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 11069	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. RR )
40	39	recnd 10068	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. CC )
41	40	adantrr 753	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( (Λ ` n ) / n ) e. CC )
42	34, 41	mulcld 10060	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ f e. D ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
43	20, 42	mulcld 10060	. . . . . . 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 849	. . . . . 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 14464	. . . . 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 24322	. . . . . . . . 9 |- ( x e. RR+ -> ( log ` x ) e. RR )
47	46	adantl 482	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
48	47	recnd 10068	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
49	48	adantr 481	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( log ` x ) e. CC )
50		ax-1cn 9994	. . . . . . 7 |- 1 e. CC
51		neg1cn 11124	. . . . . . . 8 |- -u 1 e. CC
52		0cn 10032	. . . . . . . 8 |- 0 e. CC
53	51, 52	keepel 4155	. . . . . . 7 |- if ( f e. W , -u 1 , 0 ) e. CC
54	50, 53	keepel 4155	. . . . . 6 |- if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) e. CC
55		mulcl 10020	. . . . . 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 694	. . . . 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 14520	. . . 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 849	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
59	7, 58	fsumcl 14464	. . . . . . 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 10486	. . . . . 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 14516	. . . . . . 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 10245	. . . . . . . 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 6738	. . . . . . . . . 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 6190	. . . . . . . . . . . . . . . . 17 |- ( f = .1. -> ( f ` A ) = ( .1. ` A ) )
66		rpvmasum2.1	. . . . . . . . . . . . . . . . . 18 |- .1. = ( 0g ` G )
67	1	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> N e. NN )
68	14	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> A e. U )
69	3, 8, 66, 12, 67, 68	dchr1 24982	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( .1. ` A ) = 1 )
70	65, 69	sylan9eqr 2678	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( f ` A ) = 1 )
71	70	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
72		1re 10039	. . . . . . . . . . . . . . . 16 |- 1 e. RR
73		cjre 13879	. . . . . . . . . . . . . . . 16 |- ( 1 e. RR -> ( * ` 1 ) = 1 )
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( * ` 1 ) = 1
75	71, 74	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( * ` ( f ` A ) ) = 1 )
76	75	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = ( 1 x. 1 ) )
77		1t1e1 11175	. . . . . . . . . . . . 13 |- ( 1 x. 1 ) = 1
78	76, 77	syl6eq 2672	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f = .1. ) -> ( ( * ` ( f ` A ) ) x. 1 ) = 1 )
79	78	ifeq1da 4116	. . . . . . . . . . 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 2795	. . . . . . . . . . . . 13 |- ( f =/= .1. <-> -. f = .1. )
81		ovif2 6738	. . . . . . . . . . . . . 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 798	. . . . . . . . . . . . . . . . . . . . . 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 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
85	82, 84	sylan 488	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = ( f ` ( 1r ` Z ) ) )
86	3, 8, 4	dchrmhm 24966	. . . . . . . . . . . . . . . . . . . . . . . 24 |- D C_ ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) )
87		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. D )
88	86, 87	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> f e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) )
89		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` Z ) = (mulGrp ` Z )
90		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1r ` Z ) = ( 1r ` Z )
91	89, 90	ringidval 18503	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1r ` Z ) = ( 0g ` (mulGrp ` Z ) )
92		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (mulGrp ` ℂfld ) = (mulGrp ` ℂfld )
93		cnfld1 19771	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 = ( 1r ` ℂfld )
94	92, 93	ringidval 18503	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 = ( 0g ` (mulGrp ` ℂfld ) )
95	91, 94	mhm0 17343	. . . . . . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` ( 1r ` Z ) ) = 1 )
98	85, 97	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( f ` A ) = 1 )
99	98	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = ( * ` 1 ) )
100	99, 74	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( * ` ( f ` A ) ) = 1 )
101	100	oveq1d 6665	. . . . . . . . . . . . . . . . 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 10043	. . . . . . . . . . . . . . . . 17 |- ( 1 x. -u 1 ) = -u 1
103	101, 102	syl6eq 2672	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) /\ f e. W ) -> ( ( * ` ( f ` A ) ) x. -u 1 ) = -u 1 )
104	103	ifeq1da 4116	. . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( * ` ( f ` A ) ) e. CC )
106	105	mul01d 10235	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. RR+ ) /\ f e. D ) /\ f =/= .1. ) -> ( ( * ` ( f ` A ) ) x. 0 ) = 0 )
107	106	ifeq2d 4105	. . . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . . 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 2668	. . . . . . . . . . . . 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 493	. . . . . . . . . . . 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 4117	. . . . . . . . . . 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 2656	. . . . . . . . . 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 2668	. . . . . . . . 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 6666	. . . . . . . 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 2656	. . . . . . 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 6668	. . . . . 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 2656	. . . . 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 14433	. . . 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 12772	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
120		inss1 3833	. . . . . . . . 9 |- ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) )
121		ssfi 8180	. . . . . . . . 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 694	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
123	2	phicld 15477	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. NN )
124	123	nncnd 11036	. . . . . . . 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 3603	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
127	126, 40	syldan 487	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( (Λ ` n ) / n ) e. CC )
128	122, 124, 127	fsummulc2 14516	. . . . . . 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 481	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( phi ` N ) e. CC )
130	129, 40	mulcld 10060	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
131	126, 130	syldan 487	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
132	131	ralrimiva 2966	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> A. n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( phi ` N ) x. ( (Λ ` n ) / n ) ) e. CC )
133	119	olcd 408	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( |_ ` x ) ) e. Fin ) )
134		sumss2 14457	. . . . . . . 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 1325	. . . . . . 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 3796	. . . . . . . . . . . . 13 |- ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> ( n e. ( 1 ... ( |_ ` x ) ) /\ n e. T ) )
137	136	baib 944	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( |_ ` x ) ) -> ( n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) <-> n e. T ) )
138	137	adantl 482	. . . . . . . . . . 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 2693	. . . . . . . . . . . 12 |- ( n e. T <-> n e. ( `' L " { A } ) )
141		ffn 6045	. . . . . . . . . . . . . 14 |- ( L : ZZ --> ( Base ` Z ) -> L Fn ZZ )
142	28, 141	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> L Fn ZZ )
143		fniniseg 6338	. . . . . . . . . . . . . 14 |- ( L Fn ZZ -> ( n e. ( `' L " { A } ) <-> ( n e. ZZ /\ ( L ` n ) = A ) ) )
144	143	baibd 948	. . . . . . . . . . . . 13 |- ( ( L Fn ZZ /\ n e. ZZ ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
145	142, 29, 144	syl2an 494	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. ( `' L " { A } ) <-> ( L ` n ) = A ) )
146	140, 145	syl5bb 272	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. T <-> ( L ` n ) = A ) )
147	138, 146	bitr2d 269	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( L ` n ) = A <-> n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) )
148	40	mul02d 10234	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 x. ( (Λ ` n ) / n ) ) = 0 )
149	147, 148	ifbieq2d 4111	. . . . . . . . 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 6737	. . . . . . . . . 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 762	. . . . . . . . . . . . 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 751	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
154	33, 153	mulcld 10060	. . . . . . . . . . . 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 14517	. . . . . . . . . . 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 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. U )
157	3, 4, 8, 9, 12, 151, 31, 156	sum2dchr 24999	. . . . . . . . . . . 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 6665	. . . . . . . . . . 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 481	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ f e. D ) -> ( (Λ ` n ) / n ) e. CC )
160		mulass 10024	. . . . . . . . . . . . . 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 10202	. . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . 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 1326	. . . . . . . . . . . 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 14433	. . . . . . . . . . 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 2664	. . . . . . . . . 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 2670	. . . . . . . . 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 2658	. . . . . . . 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 14433	. . . . . . 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 2660	. . . . . 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 14507	. . . . . 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 2656	. . . . 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 24979	. . . . . . . . . 10 |- ( N e. NN -> G e. Abel )
173		ablgrp 18198	. . . . . . . . . 10 |- ( G e. Abel -> G e. Grp )
174	4, 66	grpidcl 17450	. . . . . . . . . 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 10057	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
177	176, 48	eqeltrd 2701	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) e. CC )
178		iftrue 4092	. . . . . . . . . . 11 |- ( f = .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = 1 )
179	178	oveq2d 6666	. . . . . . . . . 10 |- ( f = .1. -> ( ( log ` x ) x. if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) ) = ( ( log ` x ) x. 1 ) )
180	179	sumsn 14475	. . . . . . . . 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 693	. . . . . . . 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 4317	. . . . . . . . . . 11 |- ( f e. ( D \ { .1. } ) <-> ( f e. D /\ f =/= .1. ) )
183		ifnefalse 4098	. . . . . . . . . . . . . . 15 |- ( f =/= .1. -> if ( f = .1. , 1 , if ( f e. W , -u 1 , 0 ) ) = if ( f e. W , -u 1 , 0 ) )
184	183	ad2antll 765	. . . . . . . . . . . . . 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 10273	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 1 -> -u if ( f e. W , 1 , 0 ) = -u 1 )
186		negeq 10273	. . . . . . . . . . . . . . . 16 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = -u 0 )
187		neg0 10327	. . . . . . . . . . . . . . . 16 |- -u 0 = 0
188	186, 187	syl6eq 2672	. . . . . . . . . . . . . . 15 |- ( if ( f e. W , 1 , 0 ) = 0 -> -u if ( f e. W , 1 , 0 ) = 0 )
189	185, 188	ifsb 4099	. . . . . . . . . . . . . 14 |- -u if ( f e. W , 1 , 0 ) = if ( f e. W , -u 1 , 0 )
190	184, 189	syl6eqr 2674	. . . . . . . . . . . . 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 6666	. . . . . . . . . . . 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 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ ( f e. D /\ f =/= .1. ) ) -> ( log ` x ) e. CC )
193	50, 52	keepel 4155	. . . . . . . . . . . . 13 |- if ( f e. W , 1 , 0 ) e. CC
194		mulneg2 10467	. . . . . . . . . . . . 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 694	. . . . . . . . . . . 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 2656	. . . . . . . . . . 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 492	. . . . . . . . . 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 14433	. . . . . . . . 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 8192	. . . . . . . . . . 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 481	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( log ` x ) e. CC )
202		mulcl 10020	. . . . . . . . . . 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 694	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ f e. ( D \ { .1. } ) ) -> ( ( log ` x ) x. if ( f e. W , 1 , 0 ) ) e. CC )
204	200, 203	fsumneg 14519	. . . . . . . . 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 14516	. . . . . . . . . . 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 3687	. . . . . . . . . . . . . . . . 17 |- { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } C_ ( D \ { .1. } )
209	207, 208	eqsstri 3635	. . . . . . . . . . . . . . . 16 |- W C_ ( D \ { .1. } )
210		difss 3737	. . . . . . . . . . . . . . . 16 |- ( D \ { .1. } ) C_ D
211	209, 210	sstri 3612	. . . . . . . . . . . . . . 15 |- W C_ D
212		ssfi 8180	. . . . . . . . . . . . . . 15 |- ( ( D e. Fin /\ W C_ D ) -> W e. Fin )
213	6, 211, 212	sylancl 694	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> W e. Fin )
214		fsumconst 14522	. . . . . . . . . . . . . 14 |- ( ( W e. Fin /\ 1 e. CC ) -> sum_ f e. W 1 = ( ( # ` W ) x. 1 ) )
215	213, 50, 214	sylancl 694	. . . . . . . . . . . . 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 2967	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> A. f e. W 1 e. CC )
219	200	olcd 408	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( ( D \ { .1. } ) C_ ( ZZ>= ` 1 ) \/ ( D \ { .1. } ) e. Fin ) )
220		sumss2 14457	. . . . . . . . . . . . . 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 1325	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. W 1 = sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) )
222		hashcl 13147	. . . . . . . . . . . . . . . 16 |- ( W e. Fin -> ( # ` W ) e. NN0 )
223	213, 222	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. NN0 )
224	223	nn0cnd 11353	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> ( # ` W ) e. CC )
225	224	mulid1d 10057	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> ( ( # ` W ) x. 1 ) = ( # ` W ) )
226	215, 221, 225	3eqtr3d 2664	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR+ ) -> sum_ f e. ( D \ { .1. } ) if ( f e. W , 1 , 0 ) = ( # ` W ) )
227	226	oveq2d 6666	. . . . . . . . . . 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 2658	. . . . . . . . . 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 10275	. . . . . . . . 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 2660	. . . . . . . 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 6668	. . . . . . 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 10060	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( # ` W ) ) e. CC )
233	177, 232	negsubd 10398	. . . . . . 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 2656	. . . . . 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 4040	. . . . . . . 8 |- ( { .1. } i^i ( D \ { .1. } ) ) = (/)
236	235	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } i^i ( D \ { .1. } ) ) = (/) )
237		undif2 4044	. . . . . . . 8 |- ( { .1. } u. ( D \ { .1. } ) ) = ( { .1. } u. D )
238	175	snssd 4340	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> { .1. } C_ D )
239		ssequn1 3783	. . . . . . . . 9 |- ( { .1. } C_ D <-> ( { .1. } u. D ) = D )
240	238, 239	sylib 208	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( { .1. } u. D ) = D )
241	237, 240	syl5req 2669	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> D = ( { .1. } u. ( D \ { .1. } ) ) )
242	236, 241, 6, 56	fsumsplit 14471	. . . . . 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 10486	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) = ( ( ( log ` x ) x. 1 ) - ( ( log ` x ) x. ( # ` W ) ) ) )
244	234, 242, 243	3eqtr4rd 2667	. . . . 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 6668	. . . 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 2666	. . 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 4744	. 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 11843	. . . 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 751	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( f ` A ) e. CC )
252	251	cjcld 13936	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ f e. D ) -> ( * ` ( f ` A ) ) e. CC )
253	59, 56	subcld 10392	. . . . 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 10060	. . . 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 679	. . 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 481	. . . 4 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( * ` ( f ` A ) ) e. CC )
257	253	an32s 846	. . . 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 14350	. . . . 5 |- ( ( RR+ C_ RR /\ ( * ` ( f ` A ) ) e. CC ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O(1) )
259	248, 18, 258	sylancr 695	. . . 4 |- ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( * ` ( f ` A ) ) ) e. O(1) )
260		fveq1 6190	. . . . . . . . . . . 12 |- ( f = .1. -> ( f ` ( L ` n ) ) = ( .1. ` ( L ` n ) ) )
261	260	oveq1d 6665	. . . . . . . . . . 11 |- ( f = .1. -> ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) = ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) )
262	261	sumeq2sdv 14435	. . . . . . . . . 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 6668	. . . . . . . . 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 482	. . . . . . . 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 10068	. . . . . . . . . 10 |- ( x e. RR+ -> ( log ` x ) e. CC )
266	265	mulid1d 10057	. . . . . . . . 9 |- ( x e. RR+ -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
267	266	oveq2d 6666	. . . . . . . 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 2676	. . . . . . 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 4744	. . . . . 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 25176	. . . . . . 7 |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
271	270	ad2antrr 762	. . . . . 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 2701	. . . . 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 6666	. . . . . . . . . 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 6666	. . . . . . . . 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 751	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
276		mulcom 10022	. . . . . . . . . . . . . . 15 |- ( ( ( log ` x ) e. CC /\ -u 1 e. CC ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
277	275, 51, 276	sylancl 694	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = ( -u 1 x. ( log ` x ) ) )
278	275	mulm1d 10482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( -u 1 x. ( log ` x ) ) = -u ( log ` x ) )
279	277, 278	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. -u 1 ) = -u ( log ` x ) )
280	275	mul01d 10235	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> ( ( log ` x ) x. 0 ) = 0 )
281	279, 280	ifeq12d 4106	. . . . . . . . . . . 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 6738	. . . . . . . . . . . 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 10273	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = ( log ` x ) -> -u if ( f e. W , ( log ` x ) , 0 ) = -u ( log ` x ) )
284		negeq 10273	. . . . . . . . . . . . . 14 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = -u 0 )
285	284, 187	syl6eq 2672	. . . . . . . . . . . . 13 |- ( if ( f e. W , ( log ` x ) , 0 ) = 0 -> -u if ( f e. W , ( log ` x ) , 0 ) = 0 )
286	283, 285	ifsb 4099	. . . . . . . . . . . 12 |- -u if ( f e. W , ( log ` x ) , 0 ) = if ( f e. W , -u ( log ` x ) , 0 )
287	281, 282, 286	3eqtr4g 2681	. . . . . . . . . . 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 6666	. . . . . . . . . 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 846	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) e. CC )
290		ifcl 4130	. . . . . . . . . . . 12 |- ( ( ( log ` x ) e. CC /\ 0 e. CC ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
291	275, 52, 290	sylancl 694	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. D ) /\ x e. RR+ ) -> if ( f e. W , ( log ` x ) , 0 ) e. CC )
292	289, 291	subnegd 10399	. . . . . . . . . 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 2656	. . . . . . . . 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 2678	. . . . . . . 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 846	. . . . . . 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 4744	. . . . . 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 762	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> N e. NN )
298		simplr 792	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f e. D )
299		simpr 477	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> f =/= .1. )
300		eqid 2622	. . . . . . . 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 25182	. . . . . . 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 481	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. D ) -> N e. NN )
303	302	ad2antrr 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 ) ) ) ) -> N e. NN )
304	298	adantr 481	. . . . . . . . . . . 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 792	. . . . . . . . . . . 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 794	. . . . . . . . . . . 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 804	. . . . . . . . . . . 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 805	. . . . . . . . . . . 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 25193	. . . . . . . . . . 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 4107	. . . . . . . . . . . . 13 |- ( ( f e. W <-> t = 0 ) -> if ( f e. W , ( log ` x ) , 0 ) = if ( t = 0 , ( log ` x ) , 0 ) )
311	310	oveq2d 6666	. . . . . . . . . . . 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 4745	. . . . . . . . . . 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 25192	. . . . . . . . . 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 2701	. . . . . . . . 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 3032	. . . . . . . 8 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( f ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) e. O(1) ) )
317	316	exlimdv 1861	. . . . . . 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 ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) e. O(1) ) )
318	301, 317	mpd 15	. . . . . 6 |- ( ( ( ph /\ f e. D ) /\ f =/= .1. ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( f ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( f e. W , ( log ` x ) , 0 ) ) ) e. O(1) )
319	296, 318	eqeltrd 2701	. . . . 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) )
320	272, 319	pm2.61dane 2881	. . . 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. O(1) )
321	256, 257, 259, 320	o1mul2 14355	. . 3 |- ( ( ph /\ f e. D ) -> ( x e. RR+ |-> ( ( * ` ( 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. O(1) )
322	249, 250, 255, 321	fsumo1 14544	. 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 ) ) ) ) ) ) e. O(1) )
323	247, 322	eqeltrrd 2702	1 |- ( 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) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   "cima 5117   Fn wfn 5883   -->wf 5884   -onto->wfo 5886   ` cfv 5888  (class class class)co 6650   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   [,)cico 12177   ...cfz 12326   |_cfl 12591   seqcseq 12801   #chash 13117   *ccj 13836   abscabs 13974   ~~> cli 14215   O(1)co1 14217   sum_csu 14416   phicphi 15469   Basecbs 15857   0gc0g 16100   MndHom cmhm 17333   Grpcgrp 17422   Abelcabl 18194  mulGrpcmgp 18489   1rcur 18501  Unitcui 18639  ℂ_fldccnfld 19746   ZRHomczrh 19848  ℤ/nℤczn 19851   logclog 24301  Λcvma 24818  DChrcdchr 24957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-rpss 6937  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-er 7742  df-ec 7744  df-qs 7748  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-word 13299  df-concat 13301  df-s1 13302  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-o1 14221  df-lo1 14222  df-sum 14417  df-ef 14798  df-e 14799  df-sin 14800  df-cos 14801  df-pi 14803  df-dvds 14984  df-gcd 15217  df-prm 15386  df-phi 15471  df-pc 15542  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-qus 16169  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-nsg 17592  df-eqg 17593  df-ghm 17658  df-gim 17701  df-ga 17723  df-cntz 17750  df-oppg 17776  df-od 17948  df-gex 17949  df-pgp 17950  df-lsm 18051  df-pj1 18052  df-cmn 18195  df-abl 18196  df-cyg 18280  df-dprd 18394  df-dpj 18395  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-dvr 18683  df-rnghom 18715  df-drng 18749  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lsp 18972  df-sra 19172  df-rgmod 19173  df-lidl 19174  df-rsp 19175  df-2idl 19232  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-zring 19819  df-zrh 19852  df-zn 19855  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-0p 23437  df-limc 23630  df-dv 23631  df-ply 23944  df-idp 23945  df-coe 23946  df-dgr 23947  df-quot 24046  df-log 24303  df-cxp 24304  df-em 24719  df-cht 24823  df-vma 24824  df-chp 24825  df-ppi 24826  df-mu 24827  df-dchr 24958

This theorem is referenced by:  dchrisum0re  25202  rpvmasum  25215