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