Metamath Proof Explorer

Theorem dchrisum0lema

Description: Lemma for dchrisum0 . Apply dchrisum for the function 1 / sqrt y . (Contributed by Mario Carneiro, 10-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 ) ) )
Assertion dchrisum0lema 
|- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) )

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 7 ssrab3 
 |-  W C_ ( D \ { .1. } )
11 10 8 sselid 
 |-  ( ph -> X e. ( D \ { .1. } ) )
12 11 eldifad 
 |-  ( ph -> X e. D )
13 eldifsni 
 |-  ( X e. ( D \ { .1. } ) -> X =/= .1. )
14 11 13 syl 
 |-  ( ph -> X =/= .1. )
15 fveq2 
 |-  ( n = x -> ( sqrt ` n ) = ( sqrt ` x ) )
16 15 oveq2d 
 |-  ( n = x -> ( 1 / ( sqrt ` n ) ) = ( 1 / ( sqrt ` x ) ) )
17 1nn 
 |-  1 e. NN
18 17 a1i 
 |-  ( ph -> 1 e. NN )
19 rpsqrtcl 
 |-  ( n e. RR+ -> ( sqrt ` n ) e. RR+ )
20 19 adantl 
 |-  ( ( ph /\ n e. RR+ ) -> ( sqrt ` n ) e. RR+ )
21 20 rprecred 
 |-  ( ( ph /\ n e. RR+ ) -> ( 1 / ( sqrt ` n ) ) e. RR )
22 simp3r 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> n <_ x )
23 simp2l 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> n e. RR+ )
24 23 rprege0d 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( n e. RR /\ 0 <_ n ) )
25 simp2r 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> x e. RR+ )
26 25 rprege0d 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( x e. RR /\ 0 <_ x ) )
27 sqrtle 
 |-  ( ( ( n e. RR /\ 0 <_ n ) /\ ( x e. RR /\ 0 <_ x ) ) -> ( n <_ x <-> ( sqrt ` n ) <_ ( sqrt ` x ) ) )
28 24 26 27 syl2anc 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( n <_ x <-> ( sqrt ` n ) <_ ( sqrt ` x ) ) )
29 22 28 mpbid 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( sqrt ` n ) <_ ( sqrt ` x ) )
30 23 rpsqrtcld 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( sqrt ` n ) e. RR+ )
31 25 rpsqrtcld 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( sqrt ` x ) e. RR+ )
32 30 31 lerecd 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( ( sqrt ` n ) <_ ( sqrt ` x ) <-> ( 1 / ( sqrt ` x ) ) <_ ( 1 / ( sqrt ` n ) ) ) )
33 29 32 mpbid 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( 1 / ( sqrt ` x ) ) <_ ( 1 / ( sqrt ` n ) ) )
34 sqrtlim 
 |-  ( n e. RR+ |-> ( 1 / ( sqrt ` n ) ) ) ~~>r 0
35 34 a1i 
 |-  ( ph -> ( n e. RR+ |-> ( 1 / ( sqrt ` n ) ) ) ~~>r 0 )
36 2fveq3 
 |-  ( a = n -> ( X ` ( L ` a ) ) = ( X ` ( L ` n ) ) )
37 fveq2 
 |-  ( a = n -> ( sqrt ` a ) = ( sqrt ` n ) )
38 37 oveq2d 
 |-  ( a = n -> ( 1 / ( sqrt ` a ) ) = ( 1 / ( sqrt ` n ) ) )
39 36 38 oveq12d 
 |-  ( a = n -> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) = ( ( X ` ( L ` n ) ) x. ( 1 / ( sqrt ` n ) ) ) )
40 39 cbvmptv 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. ( 1 / ( sqrt ` n ) ) ) )
41 1 2 3 4 5 6 12 14 16 18 21 33 35 40 dchrisum 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / ( sqrt ` x ) ) ) ) )
42 12 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. D )
43 nnz 
 |-  ( n e. NN -> n e. ZZ )
44 43 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. ZZ )
45 4 1 5 2 42 44 dchrzrhcl 
 |-  ( ( ph /\ n e. NN ) -> ( X ` ( L ` n ) ) e. CC )
46 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
47 46 nnrpd 
 |-  ( ( ph /\ n e. NN ) -> n e. RR+ )
48 47 rpsqrtcld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` n ) e. RR+ )
49 48 rpcnd 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` n ) e. CC )
50 48 rpne0d 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` n ) =/= 0 )
51 45 49 50 divrecd 
 |-  ( ( ph /\ n e. NN ) -> ( ( X ` ( L ` n ) ) / ( sqrt ` n ) ) = ( ( X ` ( L ` n ) ) x. ( 1 / ( sqrt ` n ) ) ) )
52 51 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> ( ( X ` ( L ` n ) ) / ( sqrt ` n ) ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. ( 1 / ( sqrt ` n ) ) ) ) )
53 36 37 oveq12d 
 |-  ( a = n -> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) = ( ( X ` ( L ` n ) ) / ( sqrt ` n ) ) )
54 53 cbvmptv 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) / ( sqrt ` n ) ) )
55 9 54 eqtri 
 |-  F = ( n e. NN |-> ( ( X ` ( L ` n ) ) / ( sqrt ` n ) ) )
56 52 55 40 3eqtr4g 
 |-  ( ph -> F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) )
57 56 seqeq3d 
 |-  ( ph -> seq 1 ( + , F ) = seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) )
58 57 breq1d 
 |-  ( ph -> ( seq 1 ( + , F ) ~~> t <-> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ~~> t ) )
59 58 adantr 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( seq 1 ( + , F ) ~~> t <-> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ~~> t ) )
60 2fveq3 
 |-  ( y = x -> ( seq 1 ( + , F ) ` ( |_ ` y ) ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) )
61 60 fvoveq1d 
 |-  ( y = x -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) )
62 fveq2 
 |-  ( y = x -> ( sqrt ` y ) = ( sqrt ` x ) )
63 62 oveq2d 
 |-  ( y = x -> ( c / ( sqrt ` y ) ) = ( c / ( sqrt ` x ) ) )
64 61 63 breq12d 
 |-  ( y = x -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / ( sqrt ` x ) ) ) )
65 64 cbvralvw 
 |-  ( A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / ( sqrt ` x ) ) )
66 56 ad2antrr 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) )
67 66 seqeq3d 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> seq 1 ( + , F ) = seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) )
68 67 fveq1d 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( seq 1 ( + , F ) ` ( |_ ` x ) ) = ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) )
69 68 fvoveq1d 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) - t ) ) )
70 elrege0 
 |-  ( c e. ( 0 [,) +oo ) <-> ( c e. RR /\ 0 <_ c ) )
71 70 simplbi 
 |-  ( c e. ( 0 [,) +oo ) -> c e. RR )
72 71 ad2antlr 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> c e. RR )
73 72 recnd 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> c e. CC )
74 1re 
 |-  1 e. RR
75 elicopnf 
 |-  ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
76 74 75 ax-mp 
 |-  ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) )
77 76 simplbi 
 |-  ( x e. ( 1 [,) +oo ) -> x e. RR )
78 77 adantl 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> x e. RR )
79 0red 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 e. RR )
80 1red 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 1 e. RR )
81 0lt1 
 |-  0 < 1
82 81 a1i 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 < 1 )
83 76 simprbi 
 |-  ( x e. ( 1 [,) +oo ) -> 1 <_ x )
84 83 adantl 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 1 <_ x )
85 79 80 78 82 84 ltletrd 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 < x )
86 78 85 elrpd 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> x e. RR+ )
87 86 rpsqrtcld 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( sqrt ` x ) e. RR+ )
88 87 rpcnd 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( sqrt ` x ) e. CC )
89 87 rpne0d 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( sqrt ` x ) =/= 0 )
90 73 88 89 divrecd 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( c / ( sqrt ` x ) ) = ( c x. ( 1 / ( sqrt ` x ) ) ) )
91 69 90 breq12d 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / ( sqrt ` x ) ) <-> ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / ( sqrt ` x ) ) ) ) )
92 91 ralbidva 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / ( sqrt ` x ) ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / ( sqrt ` x ) ) ) ) )
93 65 92 bitrid 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / ( sqrt ` x ) ) ) ) )
94 59 93 anbi12d 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) <-> ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / ( sqrt ` x ) ) ) ) ) )
95 94 rexbidva 
 |-  ( ph -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) <-> E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / ( sqrt ` x ) ) ) ) ) )
96 95 exbidv 
 |-  ( ph -> ( E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) <-> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / ( sqrt ` a ) ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / ( sqrt ` x ) ) ) ) ) )
97 41 96 mpbird 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqrt ` y ) ) ) )