Theorem dchrisum0lem2 22726

Description: Lemma for dchrisum0 22728. (Contributed by Mario Carneiro, 12-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 }
dchrisum0.b	|- ( ph -> X e. W )
dchrisum0lem1.f	|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqr ` a ) ) )
dchrisum0.c	|- ( ph -> C e. ( 0 [,) +oo ) )
dchrisum0.s	|- ( ph -> seq 1 ( + , F ) ~~> S )
dchrisum0.1	|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqr ` y ) ) )
dchrisum0lem2.h	|- H = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` y ) ) ) )
dchrisum0lem2.u	|- ( ph -> H ~~> r U )
dchrisum0lem2.k	|- K = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
dchrisum0lem2.e	|- ( ph -> E e. ( 0 [,) +oo ) )
dchrisum0lem2.t	|- ( ph -> seq 1 ( + , K ) ~~> T )
dchrisum0lem2.3	|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) )

Assertion

Ref	Expression
dchrisum0lem2	|- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) ) e. O(1) )

Distinct variable groups:   x, m, y, .1.   m, d, x, y, C   F, d, x, y   a, d, m, x, y   E, d, m, x, y   m, K, y   m, N, x, y   ph, d, m, x   T, d, m, x, y   S, d, m, x, y   U, m, x   x, W   m, Z, x, y   D, m, x, y   L, a, d, m, x, y   X, a, d, m, x, y   m, F

Allowed substitution hints:   ph( y, a)   C( a)   D( a, d)   S( a)   T( a)   U( y, a, d)   .1. ( a, d)   E( a)   F( a)   G( x, y, m, a, d)   H( x, y, m, a, d)   K( x, a, d)   N( a, d)   W( y, m, a, d)   Z( a, d)

Proof of Theorem dchrisum0lem2

Step	Hyp	Ref	Expression
1		2cnd 10390	. . 3 |- ( ( ph /\ x e. RR+ ) -> 2 e. CC )
2		rpcn 10995	. . . . 5 |- ( x e. RR+ -> x e. CC )
3	2	adantl 463	. . . 4 |- ( ( ph /\ x e. RR+ ) -> x e. CC )
4		fzfid 11791	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
5		rpvmasum2.g	. . . . . . 7 |- G = (DChr ` N )
6		rpvmasum.z	. . . . . . 7 |- Z = (ℤ/nℤ ` N )
7		rpvmasum2.d	. . . . . . 7 |- D = ( Base ` G )
8		rpvmasum.l	. . . . . . 7 |- L = ( ZRHom ` Z )
9		rpvmasum2.w	. . . . . . . . . . 11 |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
10		ssrab2 3434	. . . . . . . . . . 11 |- { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } C_ ( D \ { .1. } )
11	9, 10	eqsstri 3383	. . . . . . . . . 10 |- W C_ ( D \ { .1. } )
12		dchrisum0.b	. . . . . . . . . 10 |- ( ph -> X e. W )
13	11, 12	sseldi 3351	. . . . . . . . 9 |- ( ph -> X e. ( D \ { .1. } ) )
14	13	eldifad 3337	. . . . . . . 8 |- ( ph -> X e. D )
15	14	ad2antrr 720	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
16		elfzelz 11449	. . . . . . . 8 |- ( m e. ( 1 ... ( |_ ` x ) ) -> m e. ZZ )
17	16	adantl 463	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. ZZ )
18	5, 6, 7, 8, 15, 17	dchrzrhcl 22543	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` m ) ) e. CC )
19		elfznn 11474	. . . . . . . . 9 |- ( m e. ( 1 ... ( |_ ` x ) ) -> m e. NN )
20	19	nnrpd 11022	. . . . . . . 8 |- ( m e. ( 1 ... ( |_ ` x ) ) -> m e. RR+ )
21	20	adantl 463	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. RR+ )
22	21	rpcnd 11025	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. CC )
23	21	rpne0d 11028	. . . . . 6 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m =/= 0 )
24	18, 22, 23	divcld 10103	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
25	4, 24	fsumcl 13206	. . . 4 |- ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) e. CC )
26	3, 25	mulcld 9402	. . 3 |- ( ( ph /\ x e. RR+ ) -> ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) e. CC )
27		rpssre 10997	. . . . 5 |- RR+ C_ RR
28		2cn 10388	. . . . 5 |- 2 e. CC
29		o1const 13093	. . . . 5 |- ( ( RR+ C_ RR /\ 2 e. CC ) -> ( x e. RR+ |-> 2 ) e. O(1) )
30	27, 28, 29	mp2an 667	. . . 4 |- ( x e. RR+ |-> 2 ) e. O(1)
31	30	a1i 11	. . 3 |- ( ph -> ( x e. RR+ |-> 2 ) e. O(1) )
32	27	a1i 11	. . . 4 |- ( ph -> RR+ C_ RR )
33		1red 9397	. . . 4 |- ( ph -> 1 e. RR )
34		dchrisum0lem2.e	. . . . 5 |- ( ph -> E e. ( 0 [,) +oo ) )
35		elrege0 11388	. . . . . 6 |- ( E e. ( 0 [,) +oo ) <-> ( E e. RR /\ 0 <_ E ) )
36	35	simplbi 457	. . . . 5 |- ( E e. ( 0 [,) +oo ) -> E e. RR )
37	34, 36	syl 16	. . . 4 |- ( ph -> E e. RR )
38	3, 25	absmuld 12936	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( abs ` ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) = ( ( abs ` x ) x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) )
39		rprege0 11001	. . . . . . . . . 10 |- ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
40	39	adantl 463	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) )
41		absid 12781	. . . . . . . . 9 |- ( ( x e. RR /\ 0 <_ x ) -> ( abs ` x ) = x )
42	40, 41	syl 16	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( abs ` x ) = x )
43	42	oveq1d 6105	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( ( abs ` x ) x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) = ( x x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) )
44	38, 43	eqtrd 2473	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> ( abs ` ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) = ( x x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) )
45	44	adantrr 711	. . . . 5 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) = ( x x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) )
46	25	adantrr 711	. . . . . . . . . 10 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) e. CC )
47	46	subid1d 9704	. . . . . . . . 9 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) - 0 ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) )
48	19	adantl 463	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. NN )
49		fveq2 5688	. . . . . . . . . . . . . . . 16 |- ( a = m -> ( L ` a ) = ( L ` m ) )
50	49	fveq2d 5692	. . . . . . . . . . . . . . 15 |- ( a = m -> ( X ` ( L ` a ) ) = ( X ` ( L ` m ) ) )
51		id 22	. . . . . . . . . . . . . . 15 |- ( a = m -> a = m )
52	50, 51	oveq12d 6108	. . . . . . . . . . . . . 14 |- ( a = m -> ( ( X ` ( L ` a ) ) / a ) = ( ( X ` ( L ` m ) ) / m ) )
53		dchrisum0lem2.k	. . . . . . . . . . . . . 14 |- K = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
54		ovex 6115	. . . . . . . . . . . . . 14 |- ( ( X ` ( L ` a ) ) / a ) e. _V
55	52, 53, 54	fvmpt3i 5775	. . . . . . . . . . . . 13 |- ( m e. NN -> ( K ` m ) = ( ( X ` ( L ` m ) ) / m ) )
56	48, 55	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( K ` m ) = ( ( X ` ( L ` m ) ) / m ) )
57	56	adantlrr 715	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( K ` m ) = ( ( X ` ( L ` m ) ) / m ) )
58		rpregt0 11000	. . . . . . . . . . . . . . 15 |- ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
59	58	ad2antrl 722	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. RR /\ 0 < x ) )
60	59	simpld 456	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
61		simprr 751	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
62		flge1nn 11663	. . . . . . . . . . . . 13 |- ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
63	60, 61, 62	syl2anc 656	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. NN )
64		nnuz 10892	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
65	63, 64	syl6eleq 2531	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) )
66	24	adantlrr 715	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
67	57, 65, 66	fsumser 13203	. . . . . . . . . 10 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) = ( seq 1 ( + , K ) ` ( |_ ` x ) ) )
68		rpvmasum.a	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN )
69		rpvmasum2.1	. . . . . . . . . . . . . 14 |- .1. = ( 0g ` G )
70		eldifsni 3998	. . . . . . . . . . . . . . 15 |- ( X e. ( D \ { .1. } ) -> X =/= .1. )
71	13, 70	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> X =/= .1. )
72		dchrisum0lem2.t	. . . . . . . . . . . . . 14 |- ( ph -> seq 1 ( + , K ) ~~> T )
73		dchrisum0lem2.3	. . . . . . . . . . . . . 14 |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) )
74	6, 8, 68, 5, 7, 69, 14, 71, 53, 34, 72, 73, 9	dchrvmaeq0 22712	. . . . . . . . . . . . 13 |- ( ph -> ( X e. W <-> T = 0 ) )
75	12, 74	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> T = 0 )
76	75	adantr 462	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> T = 0 )
77	76	eqcomd 2446	. . . . . . . . . 10 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 = T )
78	67, 77	oveq12d 6108	. . . . . . . . 9 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) - 0 ) = ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) )
79	47, 78	eqtr3d 2475	. . . . . . . 8 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) = ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) )
80	79	fveq2d 5692	. . . . . . 7 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) = ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) )
81		1re 9381	. . . . . . . . . 10 |- 1 e. RR
82		elicopnf 11381	. . . . . . . . . 10 |- ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
83	81, 82	ax-mp 5	. . . . . . . . 9 |- ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) )
84	60, 61, 83	sylanbrc 659	. . . . . . . 8 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. ( 1 [,) +oo ) )
85	73	adantr 462	. . . . . . . 8 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) )
86		fveq2 5688	. . . . . . . . . . . . 13 |- ( y = x -> ( |_ ` y ) = ( |_ ` x ) )
87	86	fveq2d 5692	. . . . . . . . . . . 12 |- ( y = x -> ( seq 1 ( + , K ) ` ( |_ ` y ) ) = ( seq 1 ( + , K ) ` ( |_ ` x ) ) )
88	87	oveq1d 6105	. . . . . . . . . . 11 |- ( y = x -> ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) = ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) )
89	88	fveq2d 5692	. . . . . . . . . 10 |- ( y = x -> ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) = ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) )
90		oveq2 6098	. . . . . . . . . 10 |- ( y = x -> ( E / y ) = ( E / x ) )
91	89, 90	breq12d 4302	. . . . . . . . 9 |- ( y = x -> ( ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) <-> ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) <_ ( E / x ) ) )
92	91	rspcv 3066	. . . . . . . 8 |- ( x e. ( 1 [,) +oo ) -> ( A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) -> ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) <_ ( E / x ) ) )
93	84, 85, 92	sylc 60	. . . . . . 7 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) <_ ( E / x ) )
94	80, 93	eqbrtrd 4309	. . . . . 6 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) <_ ( E / x ) )
95	46	abscld 12918	. . . . . . 7 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) e. RR )
96	37	adantr 462	. . . . . . 7 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> E e. RR )
97		lemuldiv2 10208	. . . . . . 7 |- ( ( ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) e. RR /\ E e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( ( x x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) <_ E <-> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) <_ ( E / x ) ) )
98	95, 96, 59, 97	syl3anc 1213	. . . . . 6 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( x x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) <_ E <-> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) <_ ( E / x ) ) )
99	94, 98	mpbird 232	. . . . 5 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) <_ E )
100	45, 99	eqbrtrd 4309	. . . 4 |- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) <_ E )
101	32, 26, 33, 37, 100	elo1d 13010	. . 3 |- ( ph -> ( x e. RR+ |-> ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) e. O(1) )
102	1, 26, 31, 101	o1mul2 13098	. 2 |- ( ph -> ( x e. RR+ |-> ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) e. O(1) )
103		fzfid 11791	. . . . 5 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) e. Fin )
104	21	rpsqrcld 12894	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqr ` m ) e. RR+ )
105	104	rpcnd 11025	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqr ` m ) e. CC )
106	104	rpne0d 11028	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqr ` m ) =/= 0 )
107	18, 105, 106	divcld 10103	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) e. CC )
108	107	adantr 462	. . . . . 6 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) e. CC )
109		elfznn 11474	. . . . . . . . . 10 |- ( d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) -> d e. NN )
110	109	adantl 463	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> d e. NN )
111	110	nnrpd 11022	. . . . . . . 8 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> d e. RR+ )
112	111	rpsqrcld 12894	. . . . . . 7 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqr ` d ) e. RR+ )
113	112	rpcnd 11025	. . . . . 6 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqr ` d ) e. CC )
114	112	rpne0d 11028	. . . . . 6 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqr ` d ) =/= 0 )
115	108, 113, 114	divcld 10103	. . . . 5 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) e. CC )
116	103, 115	fsumcl 13206	. . . 4 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) e. CC )
117	4, 116	fsumcl 13206	. . 3 |- ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) e. CC )
118		mulcl 9362	. . . 4 |- ( ( 2 e. CC /\ ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) e. CC ) -> ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) e. CC )
119	28, 26, 118	sylancr 658	. . 3 |- ( ( ph /\ x e. RR+ ) -> ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) e. CC )
120		2re 10387	. . . . . . . . . 10 |- 2 e. RR
121		simpr 458	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR+ ) -> x e. RR+ )
122		2z 10674	. . . . . . . . . . . . . 14 |- 2 e. ZZ
123		rpexpcl 11880	. . . . . . . . . . . . . 14 |- ( ( x e. RR+ /\ 2 e. ZZ ) -> ( x ^ 2 ) e. RR+ )
124	121, 122, 123	sylancl 657	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR+ )
125		rpdivcl 11009	. . . . . . . . . . . . 13 |- ( ( ( x ^ 2 ) e. RR+ /\ m e. RR+ ) -> ( ( x ^ 2 ) / m ) e. RR+ )
126	124, 20, 125	syl2an 474	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x ^ 2 ) / m ) e. RR+ )
127	126	rpsqrcld 12894	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqr ` ( ( x ^ 2 ) / m ) ) e. RR+ )
128	127	rpred 11023	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqr ` ( ( x ^ 2 ) / m ) ) e. RR )
129		remulcl 9363	. . . . . . . . . 10 |- ( ( 2 e. RR /\ ( sqr ` ( ( x ^ 2 ) / m ) ) e. RR ) -> ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) e. RR )
130	120, 128, 129	sylancr 658	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) e. RR )
131	130	recnd 9408	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) e. CC )
132	107, 131	mulcld 9402	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) e. CC )
133	4, 116, 132	fsumsub 13251	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) )
134	112	rpcnne0d 11032	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( sqr ` d ) e. CC /\ ( sqr ` d ) =/= 0 ) )
135		reccl 9997	. . . . . . . . . . 11 |- ( ( ( sqr ` d ) e. CC /\ ( sqr ` d ) =/= 0 ) -> ( 1 / ( sqr ` d ) ) e. CC )
136	134, 135	syl 16	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( 1 / ( sqr ` d ) ) e. CC )
137	103, 136	fsumcl 13206	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) e. CC )
138	107, 137, 131	subdid 9796	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) = ( ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) ) - ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) )
139		fveq2 5688	. . . . . . . . . . . . . 14 |- ( y = ( ( x ^ 2 ) / m ) -> ( |_ ` y ) = ( |_ ` ( ( x ^ 2 ) / m ) ) )
140	139	oveq2d 6106	. . . . . . . . . . . . 13 |- ( y = ( ( x ^ 2 ) / m ) -> ( 1 ... ( |_ ` y ) ) = ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) )
141	140	sumeq1d 13174	. . . . . . . . . . . 12 |- ( y = ( ( x ^ 2 ) / m ) -> sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqr ` d ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) )
142		fveq2 5688	. . . . . . . . . . . . 13 |- ( y = ( ( x ^ 2 ) / m ) -> ( sqr ` y ) = ( sqr ` ( ( x ^ 2 ) / m ) ) )
143	142	oveq2d 6106	. . . . . . . . . . . 12 |- ( y = ( ( x ^ 2 ) / m ) -> ( 2 x. ( sqr ` y ) ) = ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) )
144	141, 143	oveq12d 6108	. . . . . . . . . . 11 |- ( y = ( ( x ^ 2 ) / m ) -> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` y ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) )
145		dchrisum0lem2.h	. . . . . . . . . . 11 |- H = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` y ) ) ) )
146		ovex 6115	. . . . . . . . . . 11 |- ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` y ) ) ) e. _V
147	144, 145, 146	fvmpt3i 5775	. . . . . . . . . 10 |- ( ( ( x ^ 2 ) / m ) e. RR+ -> ( H ` ( ( x ^ 2 ) / m ) ) = ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) )
148	126, 147	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( H ` ( ( x ^ 2 ) / m ) ) = ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) )
149	148	oveq2d 6106	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) = ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) )
150	108, 113, 114	divrecd 10106	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) = ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 1 / ( sqr ` d ) ) ) )
151	150	sumeq2dv 13176	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 1 / ( sqr ` d ) ) ) )
152	103, 107, 136	fsummulc2 13247	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 1 / ( sqr ` d ) ) ) )
153	151, 152	eqtr4d 2476	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) = ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) ) )
154	153	oveq1d 6105	. . . . . . . 8 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) = ( ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqr ` d ) ) ) - ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) )
155	138, 149, 154	3eqtr4d 2483	. . . . . . 7 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) )
156	155	sumeq2dv 13176	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) )
157		mulcl 9362	. . . . . . . . . 10 |- ( ( 2 e. CC /\ x e. CC ) -> ( 2 x. x ) e. CC )
158	28, 3, 157	sylancr 658	. . . . . . . . 9 |- ( ( ph /\ x e. RR+ ) -> ( 2 x. x ) e. CC )
159	4, 158, 24	fsummulc2 13247	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 2 x. x ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( 2 x. x ) x. ( ( X ` ( L ` m ) ) / m ) ) )
160	1, 3, 25	mulassd 9405	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> ( ( 2 x. x ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) = ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) )
161	158	adantr 462	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. x ) e. CC )
162	161, 107, 105, 106	div12d 10139	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. x ) x. ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` m ) ) ) = ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( ( 2 x. x ) / ( sqr ` m ) ) ) )
163	104	rpcnne0d 11032	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqr ` m ) e. CC /\ ( sqr ` m ) =/= 0 ) )
164		divdiv1 10038	. . . . . . . . . . . . 13 |- ( ( ( X ` ( L ` m ) ) e. CC /\ ( ( sqr ` m ) e. CC /\ ( sqr ` m ) =/= 0 ) /\ ( ( sqr ` m ) e. CC /\ ( sqr ` m ) =/= 0 ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` m ) ) = ( ( X ` ( L ` m ) ) / ( ( sqr ` m ) x. ( sqr ` m ) ) ) )
165	18, 163, 163, 164	syl3anc 1213	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` m ) ) = ( ( X ` ( L ` m ) ) / ( ( sqr ` m ) x. ( sqr ` m ) ) ) )
166	21	rprege0d 11030	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( m e. RR /\ 0 <_ m ) )
167		remsqsqr 12742	. . . . . . . . . . . . . 14 |- ( ( m e. RR /\ 0 <_ m ) -> ( ( sqr ` m ) x. ( sqr ` m ) ) = m )
168	166, 167	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqr ` m ) x. ( sqr ` m ) ) = m )
169	168	oveq2d 6106	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / ( ( sqr ` m ) x. ( sqr ` m ) ) ) = ( ( X ` ( L ` m ) ) / m ) )
170	165, 169	eqtr2d 2474	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / m ) = ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` m ) ) )
171	170	oveq2d 6106	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. x ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( 2 x. x ) x. ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` m ) ) ) )
172	124	adantr 462	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( x ^ 2 ) e. RR+ )
173	172	rprege0d 11030	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x ^ 2 ) e. RR /\ 0 <_ ( x ^ 2 ) ) )
174		sqrdiv 12751	. . . . . . . . . . . . . . 15 |- ( ( ( ( x ^ 2 ) e. RR /\ 0 <_ ( x ^ 2 ) ) /\ m e. RR+ ) -> ( sqr ` ( ( x ^ 2 ) / m ) ) = ( ( sqr ` ( x ^ 2 ) ) / ( sqr ` m ) ) )
175	173, 21, 174	syl2anc 656	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqr ` ( ( x ^ 2 ) / m ) ) = ( ( sqr ` ( x ^ 2 ) ) / ( sqr ` m ) ) )
176	39	ad2antlr 721	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. RR /\ 0 <_ x ) )
177		sqrsq 12755	. . . . . . . . . . . . . . . 16 |- ( ( x e. RR /\ 0 <_ x ) -> ( sqr ` ( x ^ 2 ) ) = x )
178	176, 177	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqr ` ( x ^ 2 ) ) = x )
179	178	oveq1d 6105	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqr ` ( x ^ 2 ) ) / ( sqr ` m ) ) = ( x / ( sqr ` m ) ) )
180	175, 179	eqtrd 2473	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqr ` ( ( x ^ 2 ) / m ) ) = ( x / ( sqr ` m ) ) )
181	180	oveq2d 6106	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) = ( 2 x. ( x / ( sqr ` m ) ) ) )
182		2cnd 10390	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
183	3	adantr 462	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
184		divass 10008	. . . . . . . . . . . . 13 |- ( ( 2 e. CC /\ x e. CC /\ ( ( sqr ` m ) e. CC /\ ( sqr ` m ) =/= 0 ) ) -> ( ( 2 x. x ) / ( sqr ` m ) ) = ( 2 x. ( x / ( sqr ` m ) ) ) )
185	182, 183, 163, 184	syl3anc 1213	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. x ) / ( sqr ` m ) ) = ( 2 x. ( x / ( sqr ` m ) ) ) )
186	181, 185	eqtr4d 2476	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) = ( ( 2 x. x ) / ( sqr ` m ) ) )
187	186	oveq2d 6106	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) = ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( ( 2 x. x ) / ( sqr ` m ) ) ) )
188	162, 171, 187	3eqtr4d 2483	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. x ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) )
189	188	sumeq2dv 13176	. . . . . . . 8 |- ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( 2 x. x ) x. ( ( X ` ( L ` m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) )
190	159, 160, 189	3eqtr3d 2481	. . . . . . 7 |- ( ( ph /\ x e. RR+ ) -> ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) )
191	190	oveq2d 6106	. . . . . 6 |- ( ( ph /\ x e. RR+ ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( 2 x. ( sqr ` ( ( x ^ 2 ) / m ) ) ) ) ) )
192	133, 156, 191	3eqtr4d 2483	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) )
193	192	mpteq2dva 4375	. . . 4 |- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) ) = ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) ) )
194		dchrisum0lem1.f	. . . . 5 |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqr ` a ) ) )
195		dchrisum0.c	. . . . 5 |- ( ph -> C e. ( 0 [,) +oo ) )
196		dchrisum0.s	. . . . 5 |- ( ph -> seq 1 ( + , F ) ~~> S )
197		dchrisum0.1	. . . . 5 |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqr ` y ) ) )
198		dchrisum0lem2.u	. . . . 5 |- ( ph -> H ~~> r U )
199	6, 8, 68, 5, 7, 69, 9, 12, 194, 195, 196, 197, 145, 198	dchrisum0lem2a 22725	. . . 4 |- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) ) e. O(1) )
200	193, 199	eqeltrrd 2516	. . 3 |- ( ph -> ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) - ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) ) e. O(1) )
201	117, 119, 200	o1dif 13103	. 2 |- ( ph -> ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) ) e. O(1) <-> ( x e. RR+ |-> ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) e. O(1) ) )
202	102, 201	mpbird 232	1 |- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) ) e. O(1) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1364   e. wcel 1761   =/= wne 2604   A.wral 2713   {crab 2717   \ cdif 3322   C_ wss 3325   {csn 3874   class class class wbr 4289   e. cmpt 4347   ` cfv 5415  (class class class)co 6090   CCcc 9276   RRcr 9277   0cc0 9278   1c1 9279   + caddc 9281   x. cmul 9283   +oocpnf 9411   < clt 9414   <_ cle 9415   - cmin 9591   / cdiv 9989   NNcn 10318   2c2 10367   ZZcz 10642   ZZ>=cuz 10857   RR+crp 10987   [,)cico 11298   ...cfz 11433   |_cfl 11636   seqcseq 11802   ^cexp 11861   sqrcsqr 12718   abscabs 12719   ~~> cli 12958   ~~> r crli 12959   O(1)co1 12960   sum_csu 13159   Basecbs 14170   0gc0g 14374   ZRHomczrh 17890  ℤ/nℤczn 17893  DChrcdchr 22530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355  ax-pre-sup 9356  ax-addf 9357  ax-mulf 9358

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-iin 4171  df-disj 4260  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-of 6319  df-om 6476  df-1st 6576  df-2nd 6577  df-supp 6690  df-tpos 6744  df-recs 6828  df-rdg 6862  df-1o 6916  df-2o 6917  df-oadd 6920  df-omul 6921  df-er 7097  df-ec 7099  df-qs 7103  df-map 7212  df-pm 7213  df-ixp 7260  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-fsupp 7617  df-fi 7657  df-sup 7687  df-oi 7720  df-card 8105  df-acn 8108  df-cda 8333  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-nn 10319  df-2 10376  df-3 10377  df-4 10378  df-5 10379  df-6 10380  df-7 10381  df-8 10382  df-9 10383  df-10 10384  df-n0 10576  df-z 10643  df-dec 10752  df-uz 10858  df-q 10950  df-rp 10988  df-xneg 11085  df-xadd 11086  df-xmul 11087  df-ioo 11300  df-ioc 11301  df-ico 11302  df-icc 11303  df-fz 11434  df-fzo 11545  df-fl 11638  df-mod 11705  df-seq 11803  df-exp 11862  df-fac 12048  df-bc 12075  df-hash 12100  df-shft 12552  df-cj 12584  df-re 12585  df-im 12586  df-sqr 12720  df-abs 12721  df-limsup 12945  df-clim 12962  df-rlim 12963  df-o1 12964  df-lo1 12965  df-sum 13160  df-ef 13349  df-sin 13351  df-cos 13352  df-pi 13354  df-dvds 13532  df-struct 14172  df-ndx 14173  df-slot 14174  df-base 14175  df-sets 14176  df-ress 14177  df-plusg 14247  df-mulr 14248  df-starv 14249  df-sca 14250  df-vsca 14251  df-ip 14252  df-tset 14253  df-ple 14254  df-ds 14256  df-unif 14257  df-hom 14258  df-cco 14259  df-rest 14357  df-topn 14358  df-0g 14376  df-gsum 14377  df-topgen 14378  df-pt 14379  df-prds 14382  df-xrs 14436  df-qtop 14441  df-imas 14442  df-divs 14443  df-xps 14444  df-mre 14520  df-mrc 14521  df-acs 14523  df-mnd 15411  df-mhm 15460  df-submnd 15461  df-grp 15538  df-minusg 15539  df-sbg 15540  df-mulg 15541  df-subg 15671  df-nsg 15672  df-eqg 15673  df-ghm 15738  df-cntz 15828  df-od 16025  df-cmn 16272  df-abl 16273  df-mgp 16582  df-ur 16594  df-rng 16637  df-cring 16638  df-oppr 16705  df-dvdsr 16723  df-unit 16724  df-invr 16754  df-dvr 16765  df-rnghom 16796  df-drng 16814  df-subrg 16843  df-lmod 16930  df-lss 16992  df-lsp 17031  df-sra 17231  df-rgmod 17232  df-lidl 17233  df-rsp 17234  df-2idl 17292  df-psmet 17768  df-xmet 17769  df-met 17770  df-bl 17771  df-mopn 17772  df-fbas 17773  df-fg 17774  df-cnfld 17778  df-zring 17843  df-zrh 17894  df-zn 17897  df-top 18462  df-bases 18464  df-topon 18465  df-topsp 18466  df-cld 18582  df-ntr 18583  df-cls 18584  df-nei 18661  df-lp 18699  df-perf 18700  df-cn 18790  df-cnp 18791  df-haus 18878  df-cmp 18949  df-tx 19094  df-hmeo 19287  df-fil 19378  df-fm 19470  df-flim 19471  df-flf 19472  df-xms 19854  df-ms 19855  df-tms 19856  df-cncf 20413  df-limc 21300  df-dv 21301  df-log 21967  df-cxp 21968  df-dchr 22531

This theorem is referenced by:  dchrisum0lem3  22727