Metamath Proof Explorer

Theorem dchrisum0lem2

Description: Lemma for dchrisum0 . (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` 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 ) ) / ( sqrt ` 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 / ( sqrt ` y ) ) )
dchrisum0lem2.h 
|- H = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` 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 dchrisum0lem2 
|- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum2.g 
 |-  G = ( DChr ` N )
5 rpvmasum2.d 
 |-  D = ( Base ` G )
6 rpvmasum2.1 
 |-  .1. = ( 0g ` G )
7 rpvmasum2.w 
 |-  W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
8 dchrisum0.b 
 |-  ( ph -> X e. W )
9 dchrisum0lem1.f 
 |-  F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) )
10 dchrisum0.c 
 |-  ( ph -> C e. ( 0 [,) +oo ) )
11 dchrisum0.s 
 |-  ( ph -> seq 1 ( + , F ) ~~> S )
12 dchrisum0.1 
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqrt ` y ) ) )
13 dchrisum0lem2.h 
 |-  H = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) )
14 dchrisum0lem2.u 
 |-  ( ph -> H ~~>r U )
15 dchrisum0lem2.k 
 |-  K = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
16 dchrisum0lem2.e 
 |-  ( ph -> E e. ( 0 [,) +oo ) )
17 dchrisum0lem2.t 
 |-  ( ph -> seq 1 ( + , K ) ~~> T )
18 dchrisum0lem2.3 
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) )
19 2cnd 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
20 rpcn 
 |-  ( x e. RR+ -> x e. CC )
21 20 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
22 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
23 7 ssrab3 
 |-  W C_ ( D \ { .1. } )
24 23 8 sselid 
 |-  ( ph -> X e. ( D \ { .1. } ) )
25 24 eldifad 
 |-  ( ph -> X e. D )
26 25 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
27 elfzelz 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> m e. ZZ )
28 27 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. ZZ )
29 4 1 5 2 26 28 dchrzrhcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` m ) ) e. CC )
30 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> m e. NN )
31 30 nnrpd 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> m e. RR+ )
32 31 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. RR+ )
33 32 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. CC )
34 32 rpne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m =/= 0 )
35 29 33 34 divcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
36 22 35 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) e. CC )
37 21 36 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) e. CC )
38 rpssre 
 |-  RR+ C_ RR
39 2cn 
 |-  2 e. CC
40 o1const 
 |-  ( ( RR+ C_ RR /\ 2 e. CC ) -> ( x e. RR+ |-> 2 ) e. O(1) )
41 38 39 40 mp2an 
 |-  ( x e. RR+ |-> 2 ) e. O(1)
42 41 a1i 
 |-  ( ph -> ( x e. RR+ |-> 2 ) e. O(1) )
43 38 a1i 
 |-  ( ph -> RR+ C_ RR )
44 1red 
 |-  ( ph -> 1 e. RR )
45 elrege0 
 |-  ( E e. ( 0 [,) +oo ) <-> ( E e. RR /\ 0 <_ E ) )
46 45 simplbi 
 |-  ( E e. ( 0 [,) +oo ) -> E e. RR )
47 16 46 syl 
 |-  ( ph -> E e. RR )
48 21 36 absmuld 
 |-  ( ( 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 ) ) ) )
49 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
50 49 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) )
51 absid 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( abs ` x ) = x )
52 50 51 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` x ) = x )
53 52 oveq1d 
 |-  ( ( 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 ) ) ) )
54 48 53 eqtrd 
 |-  ( ( 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 ) ) ) )
55 54 adantrr 
 |-  ( ( 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 ) ) ) )
56 36 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) e. CC )
57 56 subid1d 
 |-  ( ( 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 ) )
58 30 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. NN )
59 2fveq3 
 |-  ( a = m -> ( X ` ( L ` a ) ) = ( X ` ( L ` m ) ) )
60 id 
 |-  ( a = m -> a = m )
61 59 60 oveq12d 
 |-  ( a = m -> ( ( X ` ( L ` a ) ) / a ) = ( ( X ` ( L ` m ) ) / m ) )
62 ovex 
 |-  ( ( X ` ( L ` a ) ) / a ) e. _V
63 61 15 62 fvmpt3i 
 |-  ( m e. NN -> ( K ` m ) = ( ( X ` ( L ` m ) ) / m ) )
64 58 63 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( K ` m ) = ( ( X ` ( L ` m ) ) / m ) )
65 64 adantlrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( K ` m ) = ( ( X ` ( L ` m ) ) / m ) )
66 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
67 66 ad2antrl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. RR /\ 0 < x ) )
68 67 simpld 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
69 simprr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
70 flge1nn 
 |-  ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
71 68 69 70 syl2anc 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. NN )
72 nnuz 
 |-  NN = ( ZZ>= ` 1 )
73 71 72 eleqtrdi 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) )
74 35 adantlrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
75 65 73 74 fsumser 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) = ( seq 1 ( + , K ) ` ( |_ ` x ) ) )
76 eldifsni 
 |-  ( X e. ( D \ { .1. } ) -> X =/= .1. )
77 24 76 syl 
 |-  ( ph -> X =/= .1. )
78 1 2 3 4 5 6 25 77 15 16 17 18 7 dchrvmaeq0 
 |-  ( ph -> ( X e. W <-> T = 0 ) )
79 8 78 mpbid 
 |-  ( ph -> T = 0 )
80 79 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> T = 0 )
81 80 eqcomd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 = T )
82 75 81 oveq12d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) - 0 ) = ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) )
83 57 82 eqtr3d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) = ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) )
84 83 fveq2d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) = ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) )
85 2fveq3 
 |-  ( y = x -> ( seq 1 ( + , K ) ` ( |_ ` y ) ) = ( seq 1 ( + , K ) ` ( |_ ` x ) ) )
86 85 fvoveq1d 
 |-  ( y = x -> ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) = ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) )
87 oveq2 
 |-  ( y = x -> ( E / y ) = ( E / x ) )
88 86 87 breq12d 
 |-  ( y = x -> ( ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) <-> ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) <_ ( E / x ) ) )
89 18 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) )
90 1re 
 |-  1 e. RR
91 elicopnf 
 |-  ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
92 90 91 ax-mp 
 |-  ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) )
93 68 69 92 sylanbrc 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. ( 1 [,) +oo ) )
94 88 89 93 rspcdva 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` x ) ) - T ) ) <_ ( E / x ) )
95 84 94 eqbrtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) <_ ( E / x ) )
96 56 abscld 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) e. RR )
97 47 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> E e. RR )
98 lemuldiv2 
 |-  ( ( ( 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 ) ) )
99 96 97 67 98 syl3anc 
 |-  ( ( 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 ) ) )
100 95 99 mpbird 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x x. ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) <_ E )
101 55 100 eqbrtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) <_ E )
102 43 37 44 47 101 elo1d 
 |-  ( ph -> ( x e. RR+ |-> ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) e. O(1) )
103 19 37 42 102 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) e. O(1) )
104 fzfid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) e. Fin )
105 32 rpsqrtcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` m ) e. RR+ )
106 105 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` m ) e. CC )
107 105 rpne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` m ) =/= 0 )
108 29 106 107 divcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
109 108 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
110 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) -> d e. NN )
111 110 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> d e. NN )
112 111 nnrpd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> d e. RR+ )
113 112 rpsqrtcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` d ) e. RR+ )
114 113 rpcnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` d ) e. CC )
115 113 rpne0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` d ) =/= 0 )
116 109 114 115 divcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
117 104 116 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
118 22 117 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
119 mulcl 
 |-  ( ( 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 )
120 39 37 119 sylancr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) e. CC )
121 2re 
 |-  2 e. RR
122 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
123 2z 
 |-  2 e. ZZ
124 rpexpcl 
 |-  ( ( x e. RR+ /\ 2 e. ZZ ) -> ( x ^ 2 ) e. RR+ )
125 122 123 124 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR+ )
126 rpdivcl 
 |-  ( ( ( x ^ 2 ) e. RR+ /\ m e. RR+ ) -> ( ( x ^ 2 ) / m ) e. RR+ )
127 125 31 126 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x ^ 2 ) / m ) e. RR+ )
128 127 rpsqrtcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( ( x ^ 2 ) / m ) ) e. RR+ )
129 128 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( ( x ^ 2 ) / m ) ) e. RR )
130 remulcl 
 |-  ( ( 2 e. RR /\ ( sqrt ` ( ( x ^ 2 ) / m ) ) e. RR ) -> ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) e. RR )
131 121 129 130 sylancr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) e. RR )
132 131 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) e. CC )
133 108 132 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) e. CC )
134 22 117 133 fsumsub 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) )
135 113 rpcnne0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( sqrt ` d ) e. CC /\ ( sqrt ` d ) =/= 0 ) )
136 reccl 
 |-  ( ( ( sqrt ` d ) e. CC /\ ( sqrt ` d ) =/= 0 ) -> ( 1 / ( sqrt ` d ) ) e. CC )
137 135 136 syl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( 1 / ( sqrt ` d ) ) e. CC )
138 104 137 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) e. CC )
139 108 138 132 subdid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) = ( ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) )
140 fveq2 
 |-  ( y = ( ( x ^ 2 ) / m ) -> ( |_ ` y ) = ( |_ ` ( ( x ^ 2 ) / m ) ) )
141 140 oveq2d 
 |-  ( y = ( ( x ^ 2 ) / m ) -> ( 1 ... ( |_ ` y ) ) = ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) )
142 141 sumeq1d 
 |-  ( y = ( ( x ^ 2 ) / m ) -> sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) )
143 fveq2 
 |-  ( y = ( ( x ^ 2 ) / m ) -> ( sqrt ` y ) = ( sqrt ` ( ( x ^ 2 ) / m ) ) )
144 143 oveq2d 
 |-  ( y = ( ( x ^ 2 ) / m ) -> ( 2 x. ( sqrt ` y ) ) = ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) )
145 142 144 oveq12d 
 |-  ( y = ( ( x ^ 2 ) / m ) -> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) )
146 ovex 
 |-  ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) e. _V
147 145 13 146 fvmpt3i 
 |-  ( ( ( x ^ 2 ) / m ) e. RR+ -> ( H ` ( ( x ^ 2 ) / m ) ) = ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) )
148 127 147 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( H ` ( ( x ^ 2 ) / m ) ) = ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) )
149 148 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) = ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) )
150 109 114 115 divrecd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) = ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 1 / ( sqrt ` d ) ) ) )
151 150 sumeq2dv 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 1 / ( sqrt ` d ) ) ) )
152 104 108 137 fsummulc2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 1 / ( sqrt ` d ) ) ) )
153 151 152 eqtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) = ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) ) )
154 153 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) = ( ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( 1 / ( sqrt ` d ) ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) )
155 139 149 154 3eqtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) )
156 155 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) )
157 mulcl 
 |-  ( ( 2 e. CC /\ x e. CC ) -> ( 2 x. x ) e. CC )
158 39 21 157 sylancr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. x ) e. CC )
159 22 158 35 fsummulc2 
 |-  ( ( 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 19 21 36 mulassd 
 |-  ( ( 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 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. x ) e. CC )
162 161 108 106 107 div12d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. x ) x. ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` m ) ) ) = ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( 2 x. x ) / ( sqrt ` m ) ) ) )
163 105 rpcnne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) )
164 divdiv1 
 |-  ( ( ( X ` ( L ` m ) ) e. CC /\ ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) /\ ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` m ) ) = ( ( X ` ( L ` m ) ) / ( ( sqrt ` m ) x. ( sqrt ` m ) ) ) )
165 29 163 163 164 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` m ) ) = ( ( X ` ( L ` m ) ) / ( ( sqrt ` m ) x. ( sqrt ` m ) ) ) )
166 32 rprege0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( m e. RR /\ 0 <_ m ) )
167 remsqsqrt 
 |-  ( ( m e. RR /\ 0 <_ m ) -> ( ( sqrt ` m ) x. ( sqrt ` m ) ) = m )
168 166 167 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` m ) x. ( sqrt ` m ) ) = m )
169 168 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / ( ( sqrt ` m ) x. ( sqrt ` m ) ) ) = ( ( X ` ( L ` m ) ) / m ) )
170 165 169 eqtr2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / m ) = ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` m ) ) )
171 170 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. x ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( 2 x. x ) x. ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` m ) ) ) )
172 125 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( x ^ 2 ) e. RR+ )
173 172 rprege0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x ^ 2 ) e. RR /\ 0 <_ ( x ^ 2 ) ) )
174 sqrtdiv 
 |-  ( ( ( ( x ^ 2 ) e. RR /\ 0 <_ ( x ^ 2 ) ) /\ m e. RR+ ) -> ( sqrt ` ( ( x ^ 2 ) / m ) ) = ( ( sqrt ` ( x ^ 2 ) ) / ( sqrt ` m ) ) )
175 173 32 174 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( ( x ^ 2 ) / m ) ) = ( ( sqrt ` ( x ^ 2 ) ) / ( sqrt ` m ) ) )
176 49 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. RR /\ 0 <_ x ) )
177 sqrtsq 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( sqrt ` ( x ^ 2 ) ) = x )
178 176 177 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( x ^ 2 ) ) = x )
179 178 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` ( x ^ 2 ) ) / ( sqrt ` m ) ) = ( x / ( sqrt ` m ) ) )
180 175 179 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( ( x ^ 2 ) / m ) ) = ( x / ( sqrt ` m ) ) )
181 180 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) = ( 2 x. ( x / ( sqrt ` m ) ) ) )
182 2cnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
183 21 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
184 divass 
 |-  ( ( 2 e. CC /\ x e. CC /\ ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) ) -> ( ( 2 x. x ) / ( sqrt ` m ) ) = ( 2 x. ( x / ( sqrt ` m ) ) ) )
185 182 183 163 184 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. x ) / ( sqrt ` m ) ) = ( 2 x. ( x / ( sqrt ` m ) ) ) )
186 181 185 eqtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) = ( ( 2 x. x ) / ( sqrt ` m ) ) )
187 186 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) = ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( 2 x. x ) / ( sqrt ` m ) ) ) )
188 162 171 187 3eqtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. x ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) )
189 188 sumeq2dv 
 |-  ( ( 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 ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) )
190 159 160 189 3eqtr3d 
 |-  ( ( 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 ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) )
191 190 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` 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 ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( 2 x. ( sqrt ` ( ( x ^ 2 ) / m ) ) ) ) ) )
192 134 156 191 3eqtr4d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) )
193 192 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) ) = ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) ) )
194 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dchrisum0lem2a 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) ) e. O(1) )
195 193 194 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) - ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) ) e. O(1) )
196 118 120 195 o1dif 
 |-  ( ph -> ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) <-> ( x e. RR+ |-> ( 2 x. ( x x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / m ) ) ) ) e. O(1) ) )
197 103 196 mpbird 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) )