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 |
|
dchrvmasum.a |
|- ( ph -> A e. RR+ ) |
10 |
|
dchrvmasum2.2 |
|- ( ph -> 1 <_ A ) |
11 |
|
fzfid |
|- ( ph -> ( 1 ... ( |_ ` A ) ) e. Fin ) |
12 |
7
|
adantr |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> X e. D ) |
13 |
|
elfzelz |
|- ( d e. ( 1 ... ( |_ ` A ) ) -> d e. ZZ ) |
14 |
13
|
adantl |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. ZZ ) |
15 |
4 1 5 2 12 14
|
dchrzrhcl |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( X ` ( L ` d ) ) e. CC ) |
16 |
|
elfznn |
|- ( d e. ( 1 ... ( |_ ` A ) ) -> d e. NN ) |
17 |
16
|
adantl |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. NN ) |
18 |
|
mucl |
|- ( d e. NN -> ( mmu ` d ) e. ZZ ) |
19 |
18
|
zred |
|- ( d e. NN -> ( mmu ` d ) e. RR ) |
20 |
|
nndivre |
|- ( ( ( mmu ` d ) e. RR /\ d e. NN ) -> ( ( mmu ` d ) / d ) e. RR ) |
21 |
19 20
|
mpancom |
|- ( d e. NN -> ( ( mmu ` d ) / d ) e. RR ) |
22 |
17 21
|
syl |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( mmu ` d ) / d ) e. RR ) |
23 |
22
|
recnd |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( mmu ` d ) / d ) e. CC ) |
24 |
15 23
|
mulcld |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC ) |
25 |
|
fzfid |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... ( |_ ` ( A / d ) ) ) e. Fin ) |
26 |
12
|
adantr |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> X e. D ) |
27 |
|
elfzelz |
|- ( m e. ( 1 ... ( |_ ` ( A / d ) ) ) -> m e. ZZ ) |
28 |
27
|
adantl |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. ZZ ) |
29 |
4 1 5 2 26 28
|
dchrzrhcl |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( X ` ( L ` m ) ) e. CC ) |
30 |
|
elfznn |
|- ( m e. ( 1 ... ( |_ ` ( A / d ) ) ) -> m e. NN ) |
31 |
30
|
adantl |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. NN ) |
32 |
31
|
nnrpd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. RR+ ) |
33 |
32
|
relogcld |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` m ) e. RR ) |
34 |
33 31
|
nndivred |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` m ) / m ) e. RR ) |
35 |
34
|
recnd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` m ) / m ) e. CC ) |
36 |
29 35
|
mulcld |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) e. CC ) |
37 |
25 36
|
fsumcl |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) e. CC ) |
38 |
24 37
|
mulcld |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) e. CC ) |
39 |
16
|
nnrpd |
|- ( d e. ( 1 ... ( |_ ` A ) ) -> d e. RR+ ) |
40 |
|
rpdivcl |
|- ( ( A e. RR+ /\ d e. RR+ ) -> ( A / d ) e. RR+ ) |
41 |
9 39 40
|
syl2an |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A / d ) e. RR+ ) |
42 |
41
|
adantr |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( A / d ) e. RR+ ) |
43 |
42 32
|
rpdivcld |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( A / d ) / m ) e. RR+ ) |
44 |
43
|
relogcld |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( ( A / d ) / m ) ) e. RR ) |
45 |
44 31
|
nndivred |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` ( ( A / d ) / m ) ) / m ) e. RR ) |
46 |
45
|
recnd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` ( ( A / d ) / m ) ) / m ) e. CC ) |
47 |
29 46
|
mulcld |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) e. CC ) |
48 |
25 47
|
fsumcl |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) e. CC ) |
49 |
24 48
|
mulcld |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) e. CC ) |
50 |
11 38 49
|
fsumadd |
|- ( ph -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) + ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) + sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) ) |
51 |
42 32
|
relogdivd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( ( A / d ) / m ) ) = ( ( log ` ( A / d ) ) - ( log ` m ) ) ) |
52 |
51
|
oveq2d |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` m ) + ( log ` ( ( A / d ) / m ) ) ) = ( ( log ` m ) + ( ( log ` ( A / d ) ) - ( log ` m ) ) ) ) |
53 |
33
|
recnd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` m ) e. CC ) |
54 |
41
|
relogcld |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` ( A / d ) ) e. RR ) |
55 |
54
|
recnd |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` ( A / d ) ) e. CC ) |
56 |
55
|
adantr |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( A / d ) ) e. CC ) |
57 |
53 56
|
pncan3d |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` m ) + ( ( log ` ( A / d ) ) - ( log ` m ) ) ) = ( log ` ( A / d ) ) ) |
58 |
52 57
|
eqtr2d |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( A / d ) ) = ( ( log ` m ) + ( log ` ( ( A / d ) / m ) ) ) ) |
59 |
58
|
oveq1d |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` ( A / d ) ) / m ) = ( ( ( log ` m ) + ( log ` ( ( A / d ) / m ) ) ) / m ) ) |
60 |
44
|
recnd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( ( A / d ) / m ) ) e. CC ) |
61 |
31
|
nncnd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. CC ) |
62 |
31
|
nnne0d |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m =/= 0 ) |
63 |
53 60 61 62
|
divdird |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( log ` m ) + ( log ` ( ( A / d ) / m ) ) ) / m ) = ( ( ( log ` m ) / m ) + ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) |
64 |
59 63
|
eqtrd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` ( A / d ) ) / m ) = ( ( ( log ` m ) / m ) + ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) |
65 |
64
|
oveq2d |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) = ( ( X ` ( L ` m ) ) x. ( ( ( log ` m ) / m ) + ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) |
66 |
29 35 46
|
adddid |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) x. ( ( ( log ` m ) / m ) + ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) = ( ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) + ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) |
67 |
65 66
|
eqtrd |
|- ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) = ( ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) + ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) |
68 |
67
|
sumeq2dv |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) + ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) |
69 |
25 36 47
|
fsumadd |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) + ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) + sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) |
70 |
68 69
|
eqtrd |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) + sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) |
71 |
70
|
oveq2d |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) + sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) ) |
72 |
24 37 48
|
adddid |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) + sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) = ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) + ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) ) |
73 |
71 72
|
eqtrd |
|- ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) = ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) + ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) ) |
74 |
73
|
sumeq2dv |
|- ( ph -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) + ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) ) |
75 |
1 2 3 4 5 6 7 8 9
|
dchrvmasumlem1 |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) ) |
76 |
1 2 3 4 5 6 7 8 9 10
|
dchrvmasum2lem |
|- ( ph -> ( log ` A ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) |
77 |
75 76
|
oveq12d |
|- ( ph -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + ( log ` A ) ) = ( sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) + sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) ) ) |
78 |
50 74 77
|
3eqtr4rd |
|- ( ph -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + ( log ` A ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) ) |
79 |
78
|
adantr |
|- ( ( ph /\ ps ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + ( log ` A ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) ) |
80 |
|
iftrue |
|- ( ps -> if ( ps , ( log ` A ) , 0 ) = ( log ` A ) ) |
81 |
80
|
oveq2d |
|- ( ps -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( ps , ( log ` A ) , 0 ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + ( log ` A ) ) ) |
82 |
81
|
adantl |
|- ( ( ph /\ ps ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( ps , ( log ` A ) , 0 ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + ( log ` A ) ) ) |
83 |
|
iftrue |
|- ( ps -> if ( ps , ( A / d ) , m ) = ( A / d ) ) |
84 |
83
|
fveq2d |
|- ( ps -> ( log ` if ( ps , ( A / d ) , m ) ) = ( log ` ( A / d ) ) ) |
85 |
84
|
oveq1d |
|- ( ps -> ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) = ( ( log ` ( A / d ) ) / m ) ) |
86 |
85
|
oveq2d |
|- ( ps -> ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) = ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) |
87 |
86
|
sumeq2sdv |
|- ( ps -> sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) |
88 |
87
|
oveq2d |
|- ( ps -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) ) |
89 |
88
|
sumeq2sdv |
|- ( ps -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) ) |
90 |
89
|
adantl |
|- ( ( ph /\ ps ) -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( A / d ) ) / m ) ) ) ) |
91 |
79 82 90
|
3eqtr4d |
|- ( ( ph /\ ps ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( ps , ( log ` A ) , 0 ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) ) |
92 |
7
|
adantr |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> X e. D ) |
93 |
|
elfzelz |
|- ( n e. ( 1 ... ( |_ ` A ) ) -> n e. ZZ ) |
94 |
93
|
adantl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. ZZ ) |
95 |
4 1 5 2 92 94
|
dchrzrhcl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( X ` ( L ` n ) ) e. CC ) |
96 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN ) |
97 |
96
|
adantl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN ) |
98 |
|
vmacl |
|- ( n e. NN -> ( Lam ` n ) e. RR ) |
99 |
|
nndivre |
|- ( ( ( Lam ` n ) e. RR /\ n e. NN ) -> ( ( Lam ` n ) / n ) e. RR ) |
100 |
98 99
|
mpancom |
|- ( n e. NN -> ( ( Lam ` n ) / n ) e. RR ) |
101 |
100
|
recnd |
|- ( n e. NN -> ( ( Lam ` n ) / n ) e. CC ) |
102 |
97 101
|
syl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` n ) / n ) e. CC ) |
103 |
95 102
|
mulcld |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC ) |
104 |
11 103
|
fsumcl |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC ) |
105 |
104
|
adantr |
|- ( ( ph /\ -. ps ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC ) |
106 |
105
|
addid1d |
|- ( ( ph /\ -. ps ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + 0 ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) |
107 |
|
iffalse |
|- ( -. ps -> if ( ps , ( log ` A ) , 0 ) = 0 ) |
108 |
107
|
adantl |
|- ( ( ph /\ -. ps ) -> if ( ps , ( log ` A ) , 0 ) = 0 ) |
109 |
108
|
oveq2d |
|- ( ( ph /\ -. ps ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( ps , ( log ` A ) , 0 ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + 0 ) ) |
110 |
|
iffalse |
|- ( -. ps -> if ( ps , ( A / d ) , m ) = m ) |
111 |
110
|
fveq2d |
|- ( -. ps -> ( log ` if ( ps , ( A / d ) , m ) ) = ( log ` m ) ) |
112 |
111
|
oveq1d |
|- ( -. ps -> ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) = ( ( log ` m ) / m ) ) |
113 |
112
|
oveq2d |
|- ( -. ps -> ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) = ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) |
114 |
113
|
sumeq2sdv |
|- ( -. ps -> sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) |
115 |
114
|
oveq2d |
|- ( -. ps -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) ) |
116 |
115
|
sumeq2sdv |
|- ( -. ps -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) ) |
117 |
75
|
eqcomd |
|- ( ph -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) |
118 |
116 117
|
sylan9eqr |
|- ( ( ph /\ -. ps ) -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) |
119 |
106 109 118
|
3eqtr4d |
|- ( ( ph /\ -. ps ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( ps , ( log ` A ) , 0 ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) ) |
120 |
91 119
|
pm2.61dan |
|- ( ph -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( ps , ( log ` A ) , 0 ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) ) |