Metamath Proof Explorer

Theorem dchrisum

Description: If n e. [ M , +oo ) |-> A ( n ) is a positive decreasing function approaching zero, then the infinite sum sum_ n , X ( n ) A ( n ) is convergent, with the partial sum sum_ n <_ x , X ( n ) A ( n ) within O ( A ( M ) ) of the limit T . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.g 
|- G = ( DChr ` N )
rpvmasum.d 
|- D = ( Base ` G )
rpvmasum.1 
|- .1. = ( 0g ` G )
dchrisum.b 
|- ( ph -> X e. D )
dchrisum.n1 
|- ( ph -> X =/= .1. )
dchrisum.2 
|- ( n = x -> A = B )
dchrisum.3 
|- ( ph -> M e. NN )
dchrisum.4 
|- ( ( ph /\ n e. RR+ ) -> A e. RR )
dchrisum.5 
|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
dchrisum.6 
|- ( ph -> ( n e. RR+ |-> A ) ~~>r 0 )
dchrisum.7 
|- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
Assertion dchrisum 
|- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )

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 rpvmasum.g 
 |-  G = ( DChr ` N )
5 rpvmasum.d 
 |-  D = ( Base ` G )
6 rpvmasum.1 
 |-  .1. = ( 0g ` G )
7 dchrisum.b 
 |-  ( ph -> X e. D )
8 dchrisum.n1 
 |-  ( ph -> X =/= .1. )
9 dchrisum.2 
 |-  ( n = x -> A = B )
10 dchrisum.3 
 |-  ( ph -> M e. NN )
11 dchrisum.4 
 |-  ( ( ph /\ n e. RR+ ) -> A e. RR )
12 dchrisum.5 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
13 dchrisum.6 
 |-  ( ph -> ( n e. RR+ |-> A ) ~~>r 0 )
14 dchrisum.7 
 |-  F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
15 fzofi 
 |-  ( 0 ..^ N ) e. Fin
16 fzofi 
 |-  ( 0 ..^ u ) e. Fin
17 16 a1i 
 |-  ( ph -> ( 0 ..^ u ) e. Fin )
18 7 adantr 
 |-  ( ( ph /\ m e. ( 0 ..^ u ) ) -> X e. D )
19 elfzoelz 
 |-  ( m e. ( 0 ..^ u ) -> m e. ZZ )
20 19 adantl 
 |-  ( ( ph /\ m e. ( 0 ..^ u ) ) -> m e. ZZ )
21 4 1 5 2 18 20 dchrzrhcl 
 |-  ( ( ph /\ m e. ( 0 ..^ u ) ) -> ( X ` ( L ` m ) ) e. CC )
22 17 21 fsumcl 
 |-  ( ph -> sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) e. CC )
23 22 abscld 
 |-  ( ph -> ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) e. RR )
24 23 ralrimivw 
 |-  ( ph -> A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) e. RR )
25 fimaxre3 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) e. RR ) -> E. r e. RR A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r )
26 15 24 25 sylancr 
 |-  ( ph -> E. r e. RR A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r )
27 3 adantr 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> N e. NN )
28 7 adantr 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> X e. D )
29 8 adantr 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> X =/= .1. )
30 10 adantr 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> M e. NN )
31 11 adantlr 
 |-  ( ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) /\ n e. RR+ ) -> A e. RR )
32 12 3adant1r 
 |-  ( ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
33 13 adantr 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> ( n e. RR+ |-> A ) ~~>r 0 )
34 simprl 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> r e. RR )
35 simprr 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r )
36 2fveq3 
 |-  ( m = n -> ( X ` ( L ` m ) ) = ( X ` ( L ` n ) ) )
37 36 cbvsumv 
 |-  sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) = sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) )
38 oveq2 
 |-  ( u = i -> ( 0 ..^ u ) = ( 0 ..^ i ) )
39 38 sumeq1d 
 |-  ( u = i -> sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) = sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) )
40 37 39 syl5eq 
 |-  ( u = i -> sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) = sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) )
41 40 fveq2d 
 |-  ( u = i -> ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) = ( abs ` sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) ) )
42 41 breq1d 
 |-  ( u = i -> ( ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r <-> ( abs ` sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) ) <_ r ) )
43 42 cbvralvw 
 |-  ( A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r <-> A. i e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) ) <_ r )
44 35 43 sylib 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> A. i e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) ) <_ r )
45 1 2 27 4 5 6 28 29 9 30 31 32 33 14 34 44 dchrisumlem3 
 |-  ( ( ph /\ ( r e. RR /\ A. u e. ( 0 ..^ N ) ( abs ` sum_ m e. ( 0 ..^ u ) ( X ` ( L ` m ) ) ) <_ r ) ) -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )
46 26 45 rexlimddv 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )