Metamath Proof Explorer

Theorem dchrvmasumlem1

Description: An alternative expression for a Dirichlet-weighted von Mangoldt sum in terms of the Möbius function. Equation 9.4.11 of Shapiro, p. 377. (Contributed by Mario Carneiro, 3-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. )
dchrvmasum.a 
|- ( ph -> A e. RR+ )
Assertion 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 ) ) ) )

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 dchrvmasum.a 
 |-  ( ph -> A e. RR+ )
10 2fveq3 
 |-  ( n = ( d x. m ) -> ( X ` ( L ` n ) ) = ( X ` ( L ` ( d x. m ) ) ) )
11 oveq2 
 |-  ( n = ( d x. m ) -> ( ( mmu ` d ) / n ) = ( ( mmu ` d ) / ( d x. m ) ) )
12 fvoveq1 
 |-  ( n = ( d x. m ) -> ( log ` ( n / d ) ) = ( log ` ( ( d x. m ) / d ) ) )
13 11 12 oveq12d 
 |-  ( n = ( d x. m ) -> ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) = ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) )
14 10 13 oveq12d 
 |-  ( n = ( d x. m ) -> ( ( X ` ( L ` n ) ) x. ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) ) = ( ( X ` ( L ` ( d x. m ) ) ) x. ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) ) )
15 9 rpred 
 |-  ( ph -> A e. RR )
16 7 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> X e. D )
17 elfzelz 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. ZZ )
18 17 adantl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. ZZ )
19 4 1 5 2 16 18 dchrzrhcl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( X ` ( L ` n ) ) e. CC )
20 19 adantrr 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( X ` ( L ` n ) ) e. CC )
21 elrabi 
 |-  ( d e. { x e. NN | x || n } -> d e. NN )
22 21 ad2antll 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> d e. NN )
23 mucl 
 |-  ( d e. NN -> ( mmu ` d ) e. ZZ )
24 22 23 syl 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( mmu ` d ) e. ZZ )
25 24 zred 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( mmu ` d ) e. RR )
26 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
27 26 ad2antrl 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> n e. NN )
28 25 27 nndivred 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( ( mmu ` d ) / n ) e. RR )
29 28 recnd 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( ( mmu ` d ) / n ) e. CC )
30 27 nnrpd 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> n e. RR+ )
31 22 nnrpd 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> d e. RR+ )
32 30 31 rpdivcld 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( n / d ) e. RR+ )
33 32 relogcld 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( log ` ( n / d ) ) e. RR )
34 33 recnd 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( log ` ( n / d ) ) e. CC )
35 29 34 mulcld 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) e. CC )
36 20 35 mulcld 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( ( X ` ( L ` n ) ) x. ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) ) e. CC )
37 14 15 36 dvdsflsumcom 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } ( ( X ` ( L ` n ) ) x. ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` ( d x. m ) ) ) x. ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) ) )
38 vmaf 
 |-  Lam : NN --> RR
39 38 a1i 
 |-  ( ph -> Lam : NN --> RR )
40 ax-resscn 
 |-  RR C_ CC
41 fss 
 |-  ( ( Lam : NN --> RR /\ RR C_ CC ) -> Lam : NN --> CC )
42 39 40 41 sylancl 
 |-  ( ph -> Lam : NN --> CC )
43 vmasum 
 |-  ( m e. NN -> sum_ i e. { x e. NN | x || m } ( Lam ` i ) = ( log ` m ) )
44 43 adantl 
 |-  ( ( ph /\ m e. NN ) -> sum_ i e. { x e. NN | x || m } ( Lam ` i ) = ( log ` m ) )
45 44 eqcomd 
 |-  ( ( ph /\ m e. NN ) -> ( log ` m ) = sum_ i e. { x e. NN | x || m } ( Lam ` i ) )
46 45 mpteq2dva 
 |-  ( ph -> ( m e. NN |-> ( log ` m ) ) = ( m e. NN |-> sum_ i e. { x e. NN | x || m } ( Lam ` i ) ) )
47 42 46 muinv 
 |-  ( ph -> Lam = ( n e. NN |-> sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) ) )
48 47 fveq1d 
 |-  ( ph -> ( Lam ` n ) = ( ( n e. NN |-> sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) ) ` n ) )
49 sumex 
 |-  sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) e. _V
50 eqid 
 |-  ( n e. NN |-> sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) ) = ( n e. NN |-> sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) )
51 50 fvmpt2 
 |-  ( ( n e. NN /\ sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) e. _V ) -> ( ( n e. NN |-> sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) ) ` n ) = sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) )
52 26 49 51 sylancl 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> ( ( n e. NN |-> sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) ) ` n ) = sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) )
53 48 52 sylan9eq 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` n ) = sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) )
54 breq1 
 |-  ( x = d -> ( x || n <-> d || n ) )
55 54 elrab 
 |-  ( d e. { x e. NN | x || n } <-> ( d e. NN /\ d || n ) )
56 55 simprbi 
 |-  ( d e. { x e. NN | x || n } -> d || n )
57 56 adantl 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> d || n )
58 26 adantl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
59 nndivdvds 
 |-  ( ( n e. NN /\ d e. NN ) -> ( d || n <-> ( n / d ) e. NN ) )
60 58 21 59 syl2an 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( d || n <-> ( n / d ) e. NN ) )
61 57 60 mpbid 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( n / d ) e. NN )
62 fveq2 
 |-  ( m = ( n / d ) -> ( log ` m ) = ( log ` ( n / d ) ) )
63 eqid 
 |-  ( m e. NN |-> ( log ` m ) ) = ( m e. NN |-> ( log ` m ) )
64 fvex 
 |-  ( log ` ( n / d ) ) e. _V
65 62 63 64 fvmpt 
 |-  ( ( n / d ) e. NN -> ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) = ( log ` ( n / d ) ) )
66 61 65 syl 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) = ( log ` ( n / d ) ) )
67 66 oveq2d 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) = ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) )
68 67 sumeq2dv 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( m e. NN |-> ( log ` m ) ) ` ( n / d ) ) ) = sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) )
69 53 68 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` n ) = sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) )
70 69 oveq1d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` n ) / n ) = ( sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) / n ) )
71 fzfid 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... n ) e. Fin )
72 dvdsssfz1 
 |-  ( n e. NN -> { x e. NN | x || n } C_ ( 1 ... n ) )
73 58 72 syl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> { x e. NN | x || n } C_ ( 1 ... n ) )
74 71 73 ssfid 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> { x e. NN | x || n } e. Fin )
75 58 nncnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. CC )
76 24 zcnd 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( mmu ` d ) e. CC )
77 76 anassrs 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( mmu ` d ) e. CC )
78 34 anassrs 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( log ` ( n / d ) ) e. CC )
79 77 78 mulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) e. CC )
80 58 nnne0d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n =/= 0 )
81 74 75 79 80 fsumdivc 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) / n ) = sum_ d e. { x e. NN | x || n } ( ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) / n ) )
82 21 adantl 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> d e. NN )
83 82 23 syl 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( mmu ` d ) e. ZZ )
84 83 zcnd 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( mmu ` d ) e. CC )
85 75 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> n e. CC )
86 80 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> n =/= 0 )
87 84 78 85 86 div23d 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) / n ) = ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) )
88 87 sumeq2dv 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ d e. { x e. NN | x || n } ( ( ( mmu ` d ) x. ( log ` ( n / d ) ) ) / n ) = sum_ d e. { x e. NN | x || n } ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) )
89 70 81 88 3eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` n ) / n ) = sum_ d e. { x e. NN | x || n } ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) )
90 89 oveq2d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) = ( ( X ` ( L ` n ) ) x. sum_ d e. { x e. NN | x || n } ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) ) )
91 35 anassrs 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. { x e. NN | x || n } ) -> ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) e. CC )
92 74 19 91 fsummulc2 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( X ` ( L ` n ) ) x. sum_ d e. { x e. NN | x || n } ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) ) = sum_ d e. { x e. NN | x || n } ( ( X ` ( L ` n ) ) x. ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) ) )
93 90 92 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) = sum_ d e. { x e. NN | x || n } ( ( X ` ( L ` n ) ) x. ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) ) )
94 93 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } ( ( X ` ( L ` n ) ) x. ( ( ( mmu ` d ) / n ) x. ( log ` ( n / d ) ) ) ) )
95 fzfid 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... ( |_ ` ( A / d ) ) ) e. Fin )
96 7 adantr 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> X e. D )
97 elfzelz 
 |-  ( d e. ( 1 ... ( |_ ` A ) ) -> d e. ZZ )
98 97 adantl 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. ZZ )
99 4 1 5 2 96 98 dchrzrhcl 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( X ` ( L ` d ) ) e. CC )
100 fznnfl 
 |-  ( A e. RR -> ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. NN /\ d <_ A ) ) )
101 15 100 syl 
 |-  ( ph -> ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. NN /\ d <_ A ) ) )
102 101 simprbda 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. NN )
103 102 23 syl 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( mmu ` d ) e. ZZ )
104 103 zred 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( mmu ` d ) e. RR )
105 104 102 nndivred 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( mmu ` d ) / d ) e. RR )
106 105 recnd 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( mmu ` d ) / d ) e. CC )
107 99 106 mulcld 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC )
108 7 ad2antrr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> X e. D )
109 elfzelz 
 |-  ( m e. ( 1 ... ( |_ ` ( A / d ) ) ) -> m e. ZZ )
110 109 adantl 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. ZZ )
111 4 1 5 2 108 110 dchrzrhcl 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( X ` ( L ` m ) ) e. CC )
112 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( A / d ) ) ) -> m e. NN )
113 112 adantl 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. NN )
114 113 nnrpd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. RR+ )
115 114 relogcld 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` m ) e. RR )
116 115 113 nndivred 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` m ) / m ) e. RR )
117 116 recnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` m ) / m ) e. CC )
118 111 117 mulcld 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) e. CC )
119 95 107 118 fsummulc2 
 |-  ( ( 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 ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) )
120 99 adantr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( X ` ( L ` d ) ) e. CC )
121 106 adantr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( mmu ` d ) / d ) e. CC )
122 120 121 111 117 mul4d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) x. ( ( ( mmu ` d ) / d ) x. ( ( log ` m ) / m ) ) ) )
123 97 ad2antlr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> d e. ZZ )
124 4 1 5 2 108 123 110 dchrzrhmul 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( X ` ( L ` ( d x. m ) ) ) = ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) )
125 104 adantr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( mmu ` d ) e. RR )
126 125 recnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( mmu ` d ) e. CC )
127 115 recnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` m ) e. CC )
128 102 nnrpd 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. RR+ )
129 128 adantr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> d e. RR+ )
130 129 114 rpmulcld 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( d x. m ) e. RR+ )
131 130 rpcnne0d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( d x. m ) e. CC /\ ( d x. m ) =/= 0 ) )
132 div23 
 |-  ( ( ( mmu ` d ) e. CC /\ ( log ` m ) e. CC /\ ( ( d x. m ) e. CC /\ ( d x. m ) =/= 0 ) ) -> ( ( ( mmu ` d ) x. ( log ` m ) ) / ( d x. m ) ) = ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` m ) ) )
133 126 127 131 132 syl3anc 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( mmu ` d ) x. ( log ` m ) ) / ( d x. m ) ) = ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` m ) ) )
134 129 rpcnne0d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( d e. CC /\ d =/= 0 ) )
135 114 rpcnne0d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( m e. CC /\ m =/= 0 ) )
136 divmuldiv 
 |-  ( ( ( ( mmu ` d ) e. CC /\ ( log ` m ) e. CC ) /\ ( ( d e. CC /\ d =/= 0 ) /\ ( m e. CC /\ m =/= 0 ) ) ) -> ( ( ( mmu ` d ) / d ) x. ( ( log ` m ) / m ) ) = ( ( ( mmu ` d ) x. ( log ` m ) ) / ( d x. m ) ) )
137 126 127 134 135 136 syl22anc 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( mmu ` d ) / d ) x. ( ( log ` m ) / m ) ) = ( ( ( mmu ` d ) x. ( log ` m ) ) / ( d x. m ) ) )
138 113 nncnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. CC )
139 129 rpcnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> d e. CC )
140 129 rpne0d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> d =/= 0 )
141 138 139 140 divcan3d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( d x. m ) / d ) = m )
142 141 fveq2d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( ( d x. m ) / d ) ) = ( log ` m ) )
143 142 oveq2d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) = ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` m ) ) )
144 133 137 143 3eqtr4rd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) = ( ( ( mmu ` d ) / d ) x. ( ( log ` m ) / m ) ) )
145 124 144 oveq12d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` ( d x. m ) ) ) x. ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) x. ( ( ( mmu ` d ) / d ) x. ( ( log ` m ) / m ) ) ) )
146 122 145 eqtr4d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) = ( ( X ` ( L ` ( d x. m ) ) ) x. ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) ) )
147 146 sumeq2dv 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` ( d x. m ) ) ) x. ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) ) )
148 119 147 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 ` m ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` ( d x. m ) ) ) x. ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) ) )
149 148 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 ` m ) / m ) ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` ( d x. m ) ) ) x. ( ( ( mmu ` d ) / ( d x. m ) ) x. ( log ` ( ( d x. m ) / d ) ) ) ) )
150 37 94 149 3eqtr4d 
 |-  ( 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 ) ) ) )