Metamath Proof Explorer

Theorem dchrmusumlema

Description: Lemma for dchrmusum and dchrisumn0 . Apply dchrisum for the function 1 / y . (Contributed by Mario Carneiro, 4-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. )
dchrisumn0.f 
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
Assertion dchrmusumlema 
|- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / 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 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 dchrisumn0.f 
 |-  F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
10 oveq2 
 |-  ( n = x -> ( 1 / n ) = ( 1 / x ) )
11 1nn 
 |-  1 e. NN
12 11 a1i 
 |-  ( ph -> 1 e. NN )
13 rpreccl 
 |-  ( n e. RR+ -> ( 1 / n ) e. RR+ )
14 13 adantl 
 |-  ( ( ph /\ n e. RR+ ) -> ( 1 / n ) e. RR+ )
15 14 rpred 
 |-  ( ( ph /\ n e. RR+ ) -> ( 1 / n ) e. RR )
16 simp3r 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> n <_ x )
17 rpregt0 
 |-  ( n e. RR+ -> ( n e. RR /\ 0 < n ) )
18 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
19 lerec 
 |-  ( ( ( n e. RR /\ 0 < n ) /\ ( x e. RR /\ 0 < x ) ) -> ( n <_ x <-> ( 1 / x ) <_ ( 1 / n ) ) )
20 17 18 19 syl2an 
 |-  ( ( n e. RR+ /\ x e. RR+ ) -> ( n <_ x <-> ( 1 / x ) <_ ( 1 / n ) ) )
21 20 3ad2ant2 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( n <_ x <-> ( 1 / x ) <_ ( 1 / n ) ) )
22 16 21 mpbid 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( 1 / x ) <_ ( 1 / n ) )
23 ax-1cn 
 |-  1 e. CC
24 divrcnv 
 |-  ( 1 e. CC -> ( n e. RR+ |-> ( 1 / n ) ) ~~>r 0 )
25 23 24 mp1i 
 |-  ( ph -> ( n e. RR+ |-> ( 1 / n ) ) ~~>r 0 )
26 2fveq3 
 |-  ( a = n -> ( X ` ( L ` a ) ) = ( X ` ( L ` n ) ) )
27 oveq2 
 |-  ( a = n -> ( 1 / a ) = ( 1 / n ) )
28 26 27 oveq12d 
 |-  ( a = n -> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) = ( ( X ` ( L ` n ) ) x. ( 1 / n ) ) )
29 28 cbvmptv 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. ( 1 / n ) ) )
30 1 2 3 4 5 6 7 8 10 12 15 22 25 29 dchrisum 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) )
31 7 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. D )
32 nnz 
 |-  ( n e. NN -> n e. ZZ )
33 32 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. ZZ )
34 4 1 5 2 31 33 dchrzrhcl 
 |-  ( ( ph /\ n e. NN ) -> ( X ` ( L ` n ) ) e. CC )
35 nncn 
 |-  ( n e. NN -> n e. CC )
36 35 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. CC )
37 nnne0 
 |-  ( n e. NN -> n =/= 0 )
38 37 adantl 
 |-  ( ( ph /\ n e. NN ) -> n =/= 0 )
39 34 36 38 divrecd 
 |-  ( ( ph /\ n e. NN ) -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` n ) ) x. ( 1 / n ) ) )
40 39 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> ( ( X ` ( L ` n ) ) / n ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. ( 1 / n ) ) ) )
41 id 
 |-  ( a = n -> a = n )
42 26 41 oveq12d 
 |-  ( a = n -> ( ( X ` ( L ` a ) ) / a ) = ( ( X ` ( L ` n ) ) / n ) )
43 42 cbvmptv 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) / n ) )
44 9 43 eqtri 
 |-  F = ( n e. NN |-> ( ( X ` ( L ` n ) ) / n ) )
45 40 44 29 3eqtr4g 
 |-  ( ph -> F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) )
46 45 adantr 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) )
47 46 seqeq3d 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> seq 1 ( + , F ) = seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) )
48 47 breq1d 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( seq 1 ( + , F ) ~~> t <-> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t ) )
49 2fveq3 
 |-  ( y = x -> ( seq 1 ( + , F ) ` ( |_ ` y ) ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) )
50 49 fvoveq1d 
 |-  ( y = x -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) )
51 oveq2 
 |-  ( y = x -> ( c / y ) = ( c / x ) )
52 50 51 breq12d 
 |-  ( y = x -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / x ) ) )
53 52 cbvralvw 
 |-  ( A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / x ) )
54 45 seqeq3d 
 |-  ( ph -> seq 1 ( + , F ) = seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) )
55 54 fveq1d 
 |-  ( ph -> ( seq 1 ( + , F ) ` ( |_ ` x ) ) = ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) )
56 55 fvoveq1d 
 |-  ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) )
57 56 ad2antrr 
 |-  ( ( ( 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 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) )
58 elrege0 
 |-  ( c e. ( 0 [,) +oo ) <-> ( c e. RR /\ 0 <_ c ) )
59 58 simplbi 
 |-  ( c e. ( 0 [,) +oo ) -> c e. RR )
60 59 recnd 
 |-  ( c e. ( 0 [,) +oo ) -> c e. CC )
61 60 ad2antlr 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> c e. CC )
62 1re 
 |-  1 e. RR
63 elicopnf 
 |-  ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
64 62 63 ax-mp 
 |-  ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) )
65 64 simplbi 
 |-  ( x e. ( 1 [,) +oo ) -> x e. RR )
66 65 adantl 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> x e. RR )
67 66 recnd 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> x e. CC )
68 0red 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 e. RR )
69 1red 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 1 e. RR )
70 0lt1 
 |-  0 < 1
71 70 a1i 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 < 1 )
72 64 simprbi 
 |-  ( x e. ( 1 [,) +oo ) -> 1 <_ x )
73 72 adantl 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 1 <_ x )
74 68 69 66 71 73 ltletrd 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 < x )
75 74 gt0ne0d 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> x =/= 0 )
76 61 67 75 divrecd 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( c / x ) = ( c x. ( 1 / x ) ) )
77 57 76 breq12d 
 |-  ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / x ) <-> ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) )
78 77 ralbidva 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / x ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) )
79 53 78 syl5bb 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) )
80 48 79 anbi12d 
 |-  ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) <-> ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) )
81 80 rexbidva 
 |-  ( ph -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) <-> E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) )
82 81 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 / y ) ) <-> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) )
83 30 82 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 / y ) ) )