Metamath Proof Explorer

Theorem dchrvmasumif

Description: An asymptotic approximation for the sum of X ( n ) Lam ( n ) / n conditional on the value of the infinite sum S . (We will later show that the case S = 0 is impossible, and hence establish dchrvmasum .) (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. )
dchrvmasumif.f 
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
dchrvmasumif.c 
|- ( ph -> C e. ( 0 [,) +oo ) )
dchrvmasumif.s 
|- ( ph -> seq 1 ( + , F ) ~~> S )
dchrvmasumif.1 
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )
Assertion dchrvmasumif 
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )

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 dchrvmasumif.f 
 |-  F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
10 dchrvmasumif.c 
 |-  ( ph -> C e. ( 0 [,) +oo ) )
11 dchrvmasumif.s 
 |-  ( ph -> seq 1 ( + , F ) ~~> S )
12 dchrvmasumif.1 
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )
13 eqid 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) )
14 1 2 3 4 5 6 7 8 13 dchrvmasumlema 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) )
15 3 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> N e. NN )
16 7 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> X e. D )
17 8 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> X =/= .1. )
18 10 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> C e. ( 0 [,) +oo ) )
19 11 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> seq 1 ( + , F ) ~~> S )
20 12 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )
21 simprl 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> c e. ( 0 [,) +oo ) )
22 simprrl 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t )
23 simprrr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) )
24 1 2 15 4 5 6 16 17 9 18 19 20 13 21 22 23 dchrvmasumiflem2 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )
25 24 rexlimdvaa 
 |-  ( ph -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. O(1) ) )
26 25 exlimdv 
 |-  ( ph -> ( E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. O(1) ) )
27 14 26 mpd 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )