Metamath Proof Explorer

Theorem dchrisum0

Description: The sum sum_ n e. NN , X ( n ) / n is nonzero for all non-principal Dirichlet characters (i.e. the assumption X e. W is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 and dchrvmasumif . Lemma 9.4.4 of Shapiro, p. 382. (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 )
Assertion dchrisum0 
|- -. ph

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 eqid 
 |-  ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) = ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) )
10 7 ssrab3 
 |-  W C_ ( D \ { .1. } )
11 difss 
 |-  ( D \ { .1. } ) C_ D
12 10 11 sstri 
 |-  W C_ D
13 12 8 sselid 
 |-  ( ph -> X e. D )
14 1 2 3 4 5 6 7 8 dchrisum0re 
 |-  ( ph -> X : ( Base ` Z ) --> RR )
15 fveq2 
 |-  ( k = ( m x. d ) -> ( sqrt ` k ) = ( sqrt ` ( m x. d ) ) )
16 15 oveq2d 
 |-  ( k = ( m x. d ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` k ) ) = ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
17 rpre 
 |-  ( x e. RR+ -> x e. RR )
18 17 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
19 13 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { i e. NN | i || k } ) -> X e. D )
20 elrabi 
 |-  ( m e. { i e. NN | i || k } -> m e. NN )
21 20 nnzd 
 |-  ( m e. { i e. NN | i || k } -> m e. ZZ )
22 21 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { i e. NN | i || k } ) -> m e. ZZ )
23 4 1 5 2 19 22 dchrzrhcl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { i e. NN | i || k } ) -> ( X ` ( L ` m ) ) e. CC )
24 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` x ) ) -> k e. NN )
25 24 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. NN )
26 25 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. RR+ )
27 26 rpsqrtcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` k ) e. RR+ )
28 27 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` k ) e. CC )
29 28 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { i e. NN | i || k } ) -> ( sqrt ` k ) e. CC )
30 27 rpne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` k ) =/= 0 )
31 30 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { i e. NN | i || k } ) -> ( sqrt ` k ) =/= 0 )
32 23 29 31 divcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { i e. NN | i || k } ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` k ) ) e. CC )
33 32 anasss 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ m e. { i e. NN | i || k } ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` k ) ) e. CC )
34 16 18 33 dvdsflsumcom 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ m e. { i e. NN | i || k } ( ( X ` ( L ` m ) ) / ( sqrt ` k ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
35 1 2 3 4 5 6 9 dchrisum0fval 
 |-  ( k e. NN -> ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) = sum_ m e. { i e. NN | i || k } ( X ` ( L ` m ) ) )
36 25 35 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) = sum_ m e. { i e. NN | i || k } ( X ` ( L ` m ) ) )
37 36 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) / ( sqrt ` k ) ) = ( sum_ m e. { i e. NN | i || k } ( X ` ( L ` m ) ) / ( sqrt ` k ) ) )
38 fzfid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... k ) e. Fin )
39 dvdsssfz1 
 |-  ( k e. NN -> { i e. NN | i || k } C_ ( 1 ... k ) )
40 25 39 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { i e. NN | i || k } C_ ( 1 ... k ) )
41 38 40 ssfid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { i e. NN | i || k } e. Fin )
42 41 28 23 30 fsumdivc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. { i e. NN | i || k } ( X ` ( L ` m ) ) / ( sqrt ` k ) ) = sum_ m e. { i e. NN | i || k } ( ( X ` ( L ` m ) ) / ( sqrt ` k ) ) )
43 37 42 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) / ( sqrt ` k ) ) = sum_ m e. { i e. NN | i || k } ( ( X ` ( L ` m ) ) / ( sqrt ` k ) ) )
44 43 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) / ( sqrt ` k ) ) = sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ m e. { i e. NN | i || k } ( ( X ` ( L ` m ) ) / ( sqrt ` k ) ) )
45 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
46 45 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) )
47 resqrtth 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( ( sqrt ` x ) ^ 2 ) = x )
48 46 47 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sqrt ` x ) ^ 2 ) = x )
49 48 fveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) = ( |_ ` x ) )
50 49 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) ) = ( 1 ... ( |_ ` x ) ) )
51 48 fvoveq1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) = ( |_ ` ( x / m ) ) )
52 51 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) = ( 1 ... ( |_ ` ( x / m ) ) ) )
53 52 sumeq1d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ d e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
54 53 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ d e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
55 50 54 sumeq12dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
56 34 44 55 3eqtr4d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) / ( sqrt ` k ) ) = sum_ m e. ( 1 ... ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
57 56 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) / ( sqrt ` k ) ) ) = ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) )
58 rpsqrtcl 
 |-  ( x e. RR+ -> ( sqrt ` x ) e. RR+ )
59 58 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) e. RR+ )
60 eqidd 
 |-  ( ph -> ( x e. RR+ |-> ( sqrt ` x ) ) = ( x e. RR+ |-> ( sqrt ` x ) ) )
61 eqidd 
 |-  ( ph -> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) = ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) )
62 oveq1 
 |-  ( z = ( sqrt ` x ) -> ( z ^ 2 ) = ( ( sqrt ` x ) ^ 2 ) )
63 62 fveq2d 
 |-  ( z = ( sqrt ` x ) -> ( |_ ` ( z ^ 2 ) ) = ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) )
64 63 oveq2d 
 |-  ( z = ( sqrt ` x ) -> ( 1 ... ( |_ ` ( z ^ 2 ) ) ) = ( 1 ... ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) ) )
65 62 fvoveq1d 
 |-  ( z = ( sqrt ` x ) -> ( |_ ` ( ( z ^ 2 ) / m ) ) = ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) )
66 65 oveq2d 
 |-  ( z = ( sqrt ` x ) -> ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) = ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) )
67 66 sumeq1d 
 |-  ( z = ( sqrt ` x ) -> sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
68 67 adantr 
 |-  ( ( z = ( sqrt ` x ) /\ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
69 64 68 sumeq12dv 
 |-  ( z = ( sqrt ` x ) -> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
70 59 60 61 69 fmptco 
 |-  ( ph -> ( ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) o. ( x e. RR+ |-> ( sqrt ` x ) ) ) = ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( ( sqrt ` x ) ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( ( sqrt ` x ) ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) )
71 57 70 eqtr4d 
 |-  ( ph -> ( x e. RR+ |-> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) / ( sqrt ` k ) ) ) = ( ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) o. ( x e. RR+ |-> ( sqrt ` x ) ) ) )
72 eqid 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) )
73 1 2 3 4 5 6 7 8 72 dchrisum0lema 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) )
74 3 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) ) ) -> N e. NN )
75 8 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) ) ) -> X e. W )
76 simprl 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) ) ) -> c e. ( 0 [,) +oo ) )
77 simprrl 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) ) ) -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t )
78 simprrr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) )
79 1 2 74 4 5 6 7 75 72 76 77 78 dchrisum0lem3 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) ) ) -> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. O(1) )
80 79 rexlimdvaa 
 |-  ( ph -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) -> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. O(1) ) )
81 80 exlimdv 
 |-  ( ph -> ( E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) -> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. O(1) ) )
82 73 81 mpd 
 |-  ( ph -> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. O(1) )
83 o1f 
 |-  ( ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. O(1) -> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) : dom ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) --> CC )
84 82 83 syl 
 |-  ( ph -> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) : dom ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) --> CC )
85 sumex 
 |-  sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) e. _V
86 eqid 
 |-  ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) = ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) )
87 85 86 dmmpti 
 |-  dom ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) = RR+
88 87 feq2i 
 |-  ( ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) : dom ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) --> CC <-> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) : RR+ --> CC )
89 84 88 sylib 
 |-  ( ph -> ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) : RR+ --> CC )
90 rpssre 
 |-  RR+ C_ RR
91 90 a1i 
 |-  ( ph -> RR+ C_ RR )
92 resqcl 
 |-  ( t e. RR -> ( t ^ 2 ) e. RR )
93 0red 
 |-  ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) -> 0 e. RR )
94 simplr 
 |-  ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) -> t e. RR )
95 simplrr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> ( t ^ 2 ) <_ x )
96 45 ad2antrl 
 |-  ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) -> ( x e. RR /\ 0 <_ x ) )
97 96 adantr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> ( x e. RR /\ 0 <_ x ) )
98 97 47 syl 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> ( ( sqrt ` x ) ^ 2 ) = x )
99 95 98 breqtrrd 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> ( t ^ 2 ) <_ ( ( sqrt ` x ) ^ 2 ) )
100 94 adantr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> t e. RR )
101 59 rpred 
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) e. RR )
102 101 ad2ant2r 
 |-  ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) -> ( sqrt ` x ) e. RR )
103 102 adantr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> ( sqrt ` x ) e. RR )
104 simpr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> 0 <_ t )
105 sqrtge0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> 0 <_ ( sqrt ` x ) )
106 96 105 syl 
 |-  ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) -> 0 <_ ( sqrt ` x ) )
107 106 adantr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> 0 <_ ( sqrt ` x ) )
108 100 103 104 107 le2sqd 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> ( t <_ ( sqrt ` x ) <-> ( t ^ 2 ) <_ ( ( sqrt ` x ) ^ 2 ) ) )
109 99 108 mpbird 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ 0 <_ t ) -> t <_ ( sqrt ` x ) )
110 94 adantr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ t <_ 0 ) -> t e. RR )
111 0red 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ t <_ 0 ) -> 0 e. RR )
112 102 adantr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ t <_ 0 ) -> ( sqrt ` x ) e. RR )
113 simpr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ t <_ 0 ) -> t <_ 0 )
114 106 adantr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ t <_ 0 ) -> 0 <_ ( sqrt ` x ) )
115 110 111 112 113 114 letrd 
 |-  ( ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) /\ t <_ 0 ) -> t <_ ( sqrt ` x ) )
116 93 94 109 115 lecasei 
 |-  ( ( ( ph /\ t e. RR ) /\ ( x e. RR+ /\ ( t ^ 2 ) <_ x ) ) -> t <_ ( sqrt ` x ) )
117 116 expr 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. RR+ ) -> ( ( t ^ 2 ) <_ x -> t <_ ( sqrt ` x ) ) )
118 117 ralrimiva 
 |-  ( ( ph /\ t e. RR ) -> A. x e. RR+ ( ( t ^ 2 ) <_ x -> t <_ ( sqrt ` x ) ) )
119 breq1 
 |-  ( c = ( t ^ 2 ) -> ( c <_ x <-> ( t ^ 2 ) <_ x ) )
120 119 rspceaimv 
 |-  ( ( ( t ^ 2 ) e. RR /\ A. x e. RR+ ( ( t ^ 2 ) <_ x -> t <_ ( sqrt ` x ) ) ) -> E. c e. RR A. x e. RR+ ( c <_ x -> t <_ ( sqrt ` x ) ) )
121 92 118 120 syl2an2 
 |-  ( ( ph /\ t e. RR ) -> E. c e. RR A. x e. RR+ ( c <_ x -> t <_ ( sqrt ` x ) ) )
122 89 82 59 91 121 o1compt 
 |-  ( ph -> ( ( z e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( z ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( z ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) o. ( x e. RR+ |-> ( sqrt ` x ) ) ) e. O(1) )
123 71 122 eqeltrd 
 |-  ( ph -> ( x e. RR+ |-> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( ( b e. NN |-> sum_ y e. { i e. NN | i || b } ( X ` ( L ` y ) ) ) ` k ) / ( sqrt ` k ) ) ) e. O(1) )
124 1 2 3 4 5 6 9 13 14 123 dchrisum0fno1 
 |-  -. ph