Metamath Proof Explorer

Theorem dchrvmasum2if

Description: Combine the results of dchrvmasumlem1 and dchrvmasum2lem inside a conditional. (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 dchrvmasum2if 
|- ( 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 ) ) ) )

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