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