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