Metamath Proof Explorer

Theorem dchrvmasumlema

Description: Lemma for dchrvmasum and dchrvmasumif . Apply dchrisum for the function log ( y ) / y , which is decreasing above _e (or above 3, the nearest integer bound). (Contributed by Mario Carneiro, 5-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. )
dchrvmasumlema.f 
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) )
Assertion dchrvmasumlema 
|- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / 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 dchrvmasumlema.f 
 |-  F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) )
10 fveq2 
 |-  ( n = x -> ( log ` n ) = ( log ` x ) )
11 id 
 |-  ( n = x -> n = x )
12 10 11 oveq12d 
 |-  ( n = x -> ( ( log ` n ) / n ) = ( ( log ` x ) / x ) )
13 3nn 
 |-  3 e. NN
14 13 a1i 
 |-  ( ph -> 3 e. NN )
15 relogcl 
 |-  ( n e. RR+ -> ( log ` n ) e. RR )
16 rerpdivcl 
 |-  ( ( ( log ` n ) e. RR /\ n e. RR+ ) -> ( ( log ` n ) / n ) e. RR )
17 15 16 mpancom 
 |-  ( n e. RR+ -> ( ( log ` n ) / n ) e. RR )
18 17 adantl 
 |-  ( ( ph /\ n e. RR+ ) -> ( ( log ` n ) / n ) e. RR )
19 simp3r 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> n <_ x )
20 simp2l 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> n e. RR+ )
21 20 rpred 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> n e. RR )
22 ere 
 |-  _e e. RR
23 22 a1i 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> _e e. RR )
24 3re 
 |-  3 e. RR
25 24 a1i 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> 3 e. RR )
26 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
27 26 simpri 
 |-  _e < 3
28 22 24 27 ltleii 
 |-  _e <_ 3
29 28 a1i 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> _e <_ 3 )
30 simp3l 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> 3 <_ n )
31 23 25 21 29 30 letrd 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> _e <_ n )
32 simp2r 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> x e. RR+ )
33 32 rpred 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> x e. RR )
34 23 21 33 31 19 letrd 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> _e <_ x )
35 logdivle 
 |-  ( ( ( n e. RR /\ _e <_ n ) /\ ( x e. RR /\ _e <_ x ) ) -> ( n <_ x <-> ( ( log ` x ) / x ) <_ ( ( log ` n ) / n ) ) )
36 21 31 33 34 35 syl22anc 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> ( n <_ x <-> ( ( log ` x ) / x ) <_ ( ( log ` n ) / n ) ) )
37 19 36 mpbid 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 3 <_ n /\ n <_ x ) ) -> ( ( log ` x ) / x ) <_ ( ( log ` n ) / n ) )
38 rpcn 
 |-  ( n e. RR+ -> n e. CC )
39 38 cxp1d 
 |-  ( n e. RR+ -> ( n ^c 1 ) = n )
40 39 oveq2d 
 |-  ( n e. RR+ -> ( ( log ` n ) / ( n ^c 1 ) ) = ( ( log ` n ) / n ) )
41 40 mpteq2ia 
 |-  ( n e. RR+ |-> ( ( log ` n ) / ( n ^c 1 ) ) ) = ( n e. RR+ |-> ( ( log ` n ) / n ) )
42 1rp 
 |-  1 e. RR+
43 cxploglim 
 |-  ( 1 e. RR+ -> ( n e. RR+ |-> ( ( log ` n ) / ( n ^c 1 ) ) ) ~~>r 0 )
44 42 43 mp1i 
 |-  ( ph -> ( n e. RR+ |-> ( ( log ` n ) / ( n ^c 1 ) ) ) ~~>r 0 )
45 41 44 eqbrtrrid 
 |-  ( ph -> ( n e. RR+ |-> ( ( log ` n ) / n ) ) ~~>r 0 )
46 2fveq3 
 |-  ( a = n -> ( X ` ( L ` a ) ) = ( X ` ( L ` n ) ) )
47 fveq2 
 |-  ( a = n -> ( log ` a ) = ( log ` n ) )
48 id 
 |-  ( a = n -> a = n )
49 47 48 oveq12d 
 |-  ( a = n -> ( ( log ` a ) / a ) = ( ( log ` n ) / n ) )
50 46 49 oveq12d 
 |-  ( a = n -> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) = ( ( X ` ( L ` n ) ) x. ( ( log ` n ) / n ) ) )
51 50 cbvmptv 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. ( ( log ` n ) / n ) ) )
52 9 51 eqtri 
 |-  F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. ( ( log ` n ) / n ) ) )
53 1 2 3 4 5 6 7 8 12 14 18 37 45 52 dchrisum 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( ( log ` x ) / x ) ) ) )
54 2fveq3 
 |-  ( x = y -> ( seq 1 ( + , F ) ` ( |_ ` x ) ) = ( seq 1 ( + , F ) ` ( |_ ` y ) ) )
55 54 fvoveq1d 
 |-  ( x = y -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) )
56 fveq2 
 |-  ( x = y -> ( log ` x ) = ( log ` y ) )
57 id 
 |-  ( x = y -> x = y )
58 56 57 oveq12d 
 |-  ( x = y -> ( ( log ` x ) / x ) = ( ( log ` y ) / y ) )
59 58 oveq2d 
 |-  ( x = y -> ( c x. ( ( log ` x ) / x ) ) = ( c x. ( ( log ` y ) / y ) ) )
60 55 59 breq12d 
 |-  ( x = y -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( ( log ` x ) / x ) ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) )
61 60 cbvralvw 
 |-  ( A. x e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( ( log ` x ) / x ) ) <-> A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) )
62 61 anbi2i 
 |-  ( ( seq 1 ( + , F ) ~~> t /\ A. x e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( ( log ` x ) / x ) ) ) <-> ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) )
63 62 rexbii 
 |-  ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( ( log ` x ) / x ) ) ) <-> E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) )
64 63 exbii 
 |-  ( E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( ( log ` x ) / x ) ) ) <-> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) )
65 53 64 sylib 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) )