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