Metamath Proof Explorer

Theorem dchrvmasum2lem

Description: Give an expression for log x remarkably similar to sum_ n <_ x ( X ( n ) Lam ( n ) / n ) given in dchrvmasumlem1 . Part of Lemma 9.4.3 of Shapiro, p. 380. (Contributed by Mario Carneiro, 4-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+ )
dchrvmasum2.2 
|- ( ph -> 1 <_ A )
Assertion 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 ) ) ) )

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 dchrvmasum2.2 
 |-  ( ph -> 1 <_ A )
11 2fveq3 
 |-  ( n = ( d x. m ) -> ( X ` ( L ` n ) ) = ( X ` ( L ` ( d x. m ) ) ) )
12 id 
 |-  ( n = ( d x. m ) -> n = ( d x. m ) )
13 11 12 oveq12d 
 |-  ( n = ( d x. m ) -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) )
14 oveq2 
 |-  ( n = ( d x. m ) -> ( A / n ) = ( A / ( d x. m ) ) )
15 14 fveq2d 
 |-  ( n = ( d x. m ) -> ( log ` ( A / n ) ) = ( log ` ( A / ( d x. m ) ) ) )
16 13 15 oveq12d 
 |-  ( n = ( d x. m ) -> ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) = ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) )
17 16 oveq2d 
 |-  ( n = ( d x. m ) -> ( ( mmu ` d ) x. ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) ) = ( ( mmu ` d ) x. ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) ) )
18 9 rpred 
 |-  ( ph -> A e. RR )
19 elrabi 
 |-  ( d e. { x e. NN | x || n } -> d e. NN )
20 19 ad2antll 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> d e. NN )
21 mucl 
 |-  ( d e. NN -> ( mmu ` d ) e. ZZ )
22 20 21 syl 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( mmu ` d ) e. ZZ )
23 22 zcnd 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( mmu ` d ) e. CC )
24 7 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> X e. D )
25 elfzelz 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. ZZ )
26 25 adantl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. ZZ )
27 4 1 5 2 24 26 dchrzrhcl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( X ` ( L ` n ) ) e. CC )
28 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
29 28 adantl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
30 29 nncnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. CC )
31 29 nnne0d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n =/= 0 )
32 27 30 31 divcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( X ` ( L ` n ) ) / n ) e. CC )
33 28 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. RR+ )
34 rpdivcl 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> ( A / n ) e. RR+ )
35 9 33 34 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( A / n ) e. RR+ )
36 35 relogcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` ( A / n ) ) e. RR )
37 36 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` ( A / n ) ) e. CC )
38 32 37 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) e. CC )
39 38 adantrr 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) e. CC )
40 23 39 mulcld 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> ( ( mmu ` d ) x. ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) ) e. CC )
41 17 18 40 dvdsflsumcom 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( mmu ` d ) x. ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) ) )
42 2fveq3 
 |-  ( n = 1 -> ( X ` ( L ` n ) ) = ( X ` ( L ` 1 ) ) )
43 id 
 |-  ( n = 1 -> n = 1 )
44 42 43 oveq12d 
 |-  ( n = 1 -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` 1 ) ) / 1 ) )
45 oveq2 
 |-  ( n = 1 -> ( A / n ) = ( A / 1 ) )
46 45 fveq2d 
 |-  ( n = 1 -> ( log ` ( A / n ) ) = ( log ` ( A / 1 ) ) )
47 44 46 oveq12d 
 |-  ( n = 1 -> ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) = ( ( ( X ` ( L ` 1 ) ) / 1 ) x. ( log ` ( A / 1 ) ) ) )
48 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` A ) ) e. Fin )
49 fz1ssnn 
 |-  ( 1 ... ( |_ ` A ) ) C_ NN
50 49 a1i 
 |-  ( ph -> ( 1 ... ( |_ ` A ) ) C_ NN )
51 flge1nn 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( |_ ` A ) e. NN )
52 18 10 51 syl2anc 
 |-  ( ph -> ( |_ ` A ) e. NN )
53 nnuz 
 |-  NN = ( ZZ>= ` 1 )
54 52 53 eleqtrdi 
 |-  ( ph -> ( |_ ` A ) e. ( ZZ>= ` 1 ) )
55 eluzfz1 
 |-  ( ( |_ ` A ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( |_ ` A ) ) )
56 54 55 syl 
 |-  ( ph -> 1 e. ( 1 ... ( |_ ` A ) ) )
57 47 48 50 56 38 musumsum 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) ) = ( ( ( X ` ( L ` 1 ) ) / 1 ) x. ( log ` ( A / 1 ) ) ) )
58 4 1 5 2 7 dchrzrh1 
 |-  ( ph -> ( X ` ( L ` 1 ) ) = 1 )
59 58 oveq1d 
 |-  ( ph -> ( ( X ` ( L ` 1 ) ) / 1 ) = ( 1 / 1 ) )
60 1div1e1 
 |-  ( 1 / 1 ) = 1
61 59 60 eqtrdi 
 |-  ( ph -> ( ( X ` ( L ` 1 ) ) / 1 ) = 1 )
62 9 rpcnd 
 |-  ( ph -> A e. CC )
63 62 div1d 
 |-  ( ph -> ( A / 1 ) = A )
64 63 fveq2d 
 |-  ( ph -> ( log ` ( A / 1 ) ) = ( log ` A ) )
65 61 64 oveq12d 
 |-  ( ph -> ( ( ( X ` ( L ` 1 ) ) / 1 ) x. ( log ` ( A / 1 ) ) ) = ( 1 x. ( log ` A ) ) )
66 9 relogcld 
 |-  ( ph -> ( log ` A ) e. RR )
67 66 recnd 
 |-  ( ph -> ( log ` A ) e. CC )
68 67 mulid2d 
 |-  ( ph -> ( 1 x. ( log ` A ) ) = ( log ` A ) )
69 57 65 68 3eqtrrd 
 |-  ( ph -> ( log ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } ( ( mmu ` d ) x. ( ( ( X ` ( L ` n ) ) / n ) x. ( log ` ( A / n ) ) ) ) )
70 fzfid 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... ( |_ ` ( A / d ) ) ) e. Fin )
71 7 adantr 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> X e. D )
72 elfzelz 
 |-  ( d e. ( 1 ... ( |_ ` A ) ) -> d e. ZZ )
73 72 adantl 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. ZZ )
74 4 1 5 2 71 73 dchrzrhcl 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( X ` ( L ` d ) ) e. CC )
75 fznnfl 
 |-  ( A e. RR -> ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. NN /\ d <_ A ) ) )
76 18 75 syl 
 |-  ( ph -> ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. NN /\ d <_ A ) ) )
77 76 simprbda 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. NN )
78 77 21 syl 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( mmu ` d ) e. ZZ )
79 78 zred 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( mmu ` d ) e. RR )
80 79 77 nndivred 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( mmu ` d ) / d ) e. RR )
81 80 recnd 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( mmu ` d ) / d ) e. CC )
82 74 81 mulcld 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC )
83 7 ad2antrr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> X e. D )
84 elfzelz 
 |-  ( m e. ( 1 ... ( |_ ` ( A / d ) ) ) -> m e. ZZ )
85 84 adantl 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. ZZ )
86 4 1 5 2 83 85 dchrzrhcl 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( X ` ( L ` m ) ) e. CC )
87 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` A ) ) -> d e. NN )
88 87 nnrpd 
 |-  ( d e. ( 1 ... ( |_ ` A ) ) -> d e. RR+ )
89 rpdivcl 
 |-  ( ( A e. RR+ /\ d e. RR+ ) -> ( A / d ) e. RR+ )
90 9 88 89 syl2an 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A / d ) e. RR+ )
91 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( A / d ) ) ) -> m e. NN )
92 91 nnrpd 
 |-  ( m e. ( 1 ... ( |_ ` ( A / d ) ) ) -> m e. RR+ )
93 rpdivcl 
 |-  ( ( ( A / d ) e. RR+ /\ m e. RR+ ) -> ( ( A / d ) / m ) e. RR+ )
94 90 92 93 syl2an 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( A / d ) / m ) e. RR+ )
95 94 relogcld 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( ( A / d ) / m ) ) e. RR )
96 91 adantl 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. NN )
97 95 96 nndivred 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` ( ( A / d ) / m ) ) / m ) e. RR )
98 97 recnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( log ` ( ( A / d ) / m ) ) / m ) e. CC )
99 86 98 mulcld 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) e. CC )
100 70 82 99 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 ` ( ( A / d ) / m ) ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) )
101 74 adantr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( X ` ( L ` d ) ) e. CC )
102 79 adantr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( mmu ` d ) e. RR )
103 102 recnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( mmu ` d ) e. CC )
104 77 nnrpd 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. RR+ )
105 104 adantr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> d e. RR+ )
106 105 rpcnne0d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( d e. CC /\ d =/= 0 ) )
107 div12 
 |-  ( ( ( X ` ( L ` d ) ) e. CC /\ ( mmu ` d ) e. CC /\ ( d e. CC /\ d =/= 0 ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) = ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) )
108 101 103 106 107 syl3anc 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) = ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) )
109 95 recnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( ( A / d ) / m ) ) e. CC )
110 96 nnrpd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. RR+ )
111 110 rpcnne0d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( m e. CC /\ m =/= 0 ) )
112 div12 
 |-  ( ( ( X ` ( L ` m ) ) e. CC /\ ( log ` ( ( A / d ) / m ) ) e. CC /\ ( m e. CC /\ m =/= 0 ) ) -> ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) = ( ( log ` ( ( A / d ) / m ) ) x. ( ( X ` ( L ` m ) ) / m ) ) )
113 86 109 111 112 syl3anc 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) = ( ( log ` ( ( A / d ) / m ) ) x. ( ( X ` ( L ` m ) ) / m ) ) )
114 108 113 oveq12d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) = ( ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) x. ( ( log ` ( ( A / d ) / m ) ) x. ( ( X ` ( L ` m ) ) / m ) ) ) )
115 105 rpcnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> d e. CC )
116 105 rpne0d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> d =/= 0 )
117 101 115 116 divcld 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` d ) ) / d ) e. CC )
118 96 nncnd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m e. CC )
119 96 nnne0d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> m =/= 0 )
120 86 118 119 divcld 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
121 117 120 mulcld 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) e. CC )
122 103 109 121 mulassd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( mmu ` d ) x. ( log ` ( ( A / d ) / m ) ) ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) = ( ( mmu ` d ) x. ( ( log ` ( ( A / d ) / m ) ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) ) )
123 103 117 109 120 mul4d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) x. ( ( log ` ( ( A / d ) / m ) ) x. ( ( X ` ( L ` m ) ) / m ) ) ) = ( ( ( mmu ` d ) x. ( log ` ( ( A / d ) / m ) ) ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) )
124 72 ad2antlr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> d e. ZZ )
125 4 1 5 2 83 124 85 dchrzrhmul 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( X ` ( L ` ( d x. m ) ) ) = ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) )
126 125 oveq1d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) / ( d x. m ) ) )
127 divmuldiv 
 |-  ( ( ( ( X ` ( L ` d ) ) e. CC /\ ( X ` ( L ` m ) ) e. CC ) /\ ( ( d e. CC /\ d =/= 0 ) /\ ( m e. CC /\ m =/= 0 ) ) ) -> ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) / ( d x. m ) ) )
128 101 86 106 111 127 syl22anc 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) / ( d x. m ) ) )
129 126 128 eqtr4d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) = ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) )
130 62 ad2antrr 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> A e. CC )
131 divdiv1 
 |-  ( ( A e. CC /\ ( d e. CC /\ d =/= 0 ) /\ ( m e. CC /\ m =/= 0 ) ) -> ( ( A / d ) / m ) = ( A / ( d x. m ) ) )
132 130 106 111 131 syl3anc 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( A / d ) / m ) = ( A / ( d x. m ) ) )
133 132 eqcomd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( A / ( d x. m ) ) = ( ( A / d ) / m ) )
134 133 fveq2d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( log ` ( A / ( d x. m ) ) ) = ( log ` ( ( A / d ) / m ) ) )
135 129 134 oveq12d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) = ( ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) x. ( log ` ( ( A / d ) / m ) ) ) )
136 121 109 mulcomd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) x. ( log ` ( ( A / d ) / m ) ) ) = ( ( log ` ( ( A / d ) / m ) ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) )
137 135 136 eqtrd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) = ( ( log ` ( ( A / d ) / m ) ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) )
138 137 oveq2d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) ) = ( ( mmu ` d ) x. ( ( log ` ( ( A / d ) / m ) ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) ) )
139 122 123 138 3eqtr4d 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) x. ( ( log ` ( ( A / d ) / m ) ) x. ( ( X ` ( L ` m ) ) / m ) ) ) = ( ( mmu ` d ) x. ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) ) )
140 114 139 eqtrd 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) = ( ( mmu ` d ) x. ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) ) )
141 140 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 ` ( ( A / d ) / m ) ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( mmu ` d ) x. ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) ) )
142 100 141 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 ) ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( mmu ` d ) x. ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) ) )
143 142 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 ) ) / m ) ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( mmu ` d ) x. ( ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) x. ( log ` ( A / ( d x. m ) ) ) ) ) )
144 41 69 143 3eqtr4d 
 |-  ( 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 ) ) ) )