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 ) ) )