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.u |
|- U = ( Unit ` Z ) |
5 |
|
rpvmasum.b |
|- ( ph -> A e. U ) |
6 |
|
rpvmasum.t |
|- T = ( `' L " { A } ) |
7 |
3
|
adantr |
|- ( ( ph /\ f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) -> N e. NN ) |
8 |
|
eqid |
|- ( DChr ` N ) = ( DChr ` N ) |
9 |
|
eqid |
|- ( Base ` ( DChr ` N ) ) = ( Base ` ( DChr ` N ) ) |
10 |
|
eqid |
|- ( 0g ` ( DChr ` N ) ) = ( 0g ` ( DChr ` N ) ) |
11 |
|
2fveq3 |
|- ( m = n -> ( y ` ( L ` m ) ) = ( y ` ( L ` n ) ) ) |
12 |
|
id |
|- ( m = n -> m = n ) |
13 |
11 12
|
oveq12d |
|- ( m = n -> ( ( y ` ( L ` m ) ) / m ) = ( ( y ` ( L ` n ) ) / n ) ) |
14 |
13
|
cbvsumv |
|- sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = sum_ n e. NN ( ( y ` ( L ` n ) ) / n ) |
15 |
14
|
eqeq1i |
|- ( sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 <-> sum_ n e. NN ( ( y ` ( L ` n ) ) / n ) = 0 ) |
16 |
15
|
rabbii |
|- { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } = { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ n e. NN ( ( y ` ( L ` n ) ) / n ) = 0 } |
17 |
|
simpr |
|- ( ( ph /\ f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) -> f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) |
18 |
1 2 7 8 9 10 16 17
|
dchrisum0 |
|- -. ( ph /\ f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) |
19 |
18
|
imnani |
|- ( ph -> -. f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) |
20 |
19
|
eq0rdv |
|- ( ph -> { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } = (/) ) |
21 |
20
|
fveq2d |
|- ( ph -> ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) = ( # ` (/) ) ) |
22 |
|
hash0 |
|- ( # ` (/) ) = 0 |
23 |
21 22
|
eqtrdi |
|- ( ph -> ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) = 0 ) |
24 |
23
|
oveq2d |
|- ( ph -> ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) = ( 1 - 0 ) ) |
25 |
|
1m0e1 |
|- ( 1 - 0 ) = 1 |
26 |
24 25
|
eqtrdi |
|- ( ph -> ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) = 1 ) |
27 |
26
|
adantr |
|- ( ( ph /\ x e. RR+ ) -> ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) = 1 ) |
28 |
27
|
oveq2d |
|- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) = ( ( log ` x ) x. 1 ) ) |
29 |
|
relogcl |
|- ( x e. RR+ -> ( log ` x ) e. RR ) |
30 |
29
|
adantl |
|- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR ) |
31 |
30
|
recnd |
|- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC ) |
32 |
31
|
mulid1d |
|- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) ) |
33 |
28 32
|
eqtrd |
|- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) = ( log ` x ) ) |
34 |
33
|
oveq2d |
|- ( ( ph /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) ) = ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) |
35 |
34
|
mpteq2dva |
|- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) ) ) = ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) ) |
36 |
|
eqid |
|- { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } = { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } |
37 |
18
|
pm2.21i |
|- ( ( ph /\ f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) -> A = ( 1r ` Z ) ) |
38 |
1 2 3 8 9 10 36 4 5 6 37
|
rpvmasum2 |
|- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) ) ) e. O(1) ) |
39 |
35 38
|
eqeltrrd |
|- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) ) |