Metamath Proof Explorer

Theorem pclogsum

Description: The logarithmic analogue of pcprod . The sum of the logarithms of the primes dividing A multiplied by their powers yields the logarithm of A . (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Assertion pclogsum 
|- ( A e. NN -> sum_ p e. ( ( 1 ... A ) i^i Prime ) ( ( p pCnt A ) x. ( log ` p ) ) = ( log ` A ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( p e. ( ( 1 ... A ) i^i Prime ) <-> ( p e. ( 1 ... A ) /\ p e. Prime ) )
2 1 baib 
 |-  ( p e. ( 1 ... A ) -> ( p e. ( ( 1 ... A ) i^i Prime ) <-> p e. Prime ) )
3 2 ifbid 
 |-  ( p e. ( 1 ... A ) -> if ( p e. ( ( 1 ... A ) i^i Prime ) , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) = if ( p e. Prime , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) )
4 fvif 
 |-  ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) = if ( p e. Prime , ( log ` ( p ^ ( p pCnt A ) ) ) , ( log ` 1 ) )
5 log1 
 |-  ( log ` 1 ) = 0
6 ifeq2 
 |-  ( ( log ` 1 ) = 0 -> if ( p e. Prime , ( log ` ( p ^ ( p pCnt A ) ) ) , ( log ` 1 ) ) = if ( p e. Prime , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) )
7 5 6 ax-mp 
 |-  if ( p e. Prime , ( log ` ( p ^ ( p pCnt A ) ) ) , ( log ` 1 ) ) = if ( p e. Prime , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 )
8 4 7 eqtri 
 |-  ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) = if ( p e. Prime , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 )
9 3 8 eqtr4di 
 |-  ( p e. ( 1 ... A ) -> if ( p e. ( ( 1 ... A ) i^i Prime ) , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) = ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) )
10 9 sumeq2i 
 |-  sum_ p e. ( 1 ... A ) if ( p e. ( ( 1 ... A ) i^i Prime ) , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) = sum_ p e. ( 1 ... A ) ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) )
11 inss1 
 |-  ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A )
12 simpr 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> p e. ( ( 1 ... A ) i^i Prime ) )
13 12 elin1d 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> p e. ( 1 ... A ) )
14 elfznn 
 |-  ( p e. ( 1 ... A ) -> p e. NN )
15 13 14 syl 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> p e. NN )
16 12 elin2d 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> p e. Prime )
17 simpl 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> A e. NN )
18 16 17 pccld 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( p pCnt A ) e. NN0 )
19 15 18 nnexpcld 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( p ^ ( p pCnt A ) ) e. NN )
20 19 nnrpd 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( p ^ ( p pCnt A ) ) e. RR+ )
21 20 relogcld 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( log ` ( p ^ ( p pCnt A ) ) ) e. RR )
22 21 recnd 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( log ` ( p ^ ( p pCnt A ) ) ) e. CC )
23 22 ralrimiva 
 |-  ( A e. NN -> A. p e. ( ( 1 ... A ) i^i Prime ) ( log ` ( p ^ ( p pCnt A ) ) ) e. CC )
24 fzfi 
 |-  ( 1 ... A ) e. Fin
25 24 olci 
 |-  ( ( 1 ... A ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... A ) e. Fin )
26 sumss2 
 |-  ( ( ( ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A ) /\ A. p e. ( ( 1 ... A ) i^i Prime ) ( log ` ( p ^ ( p pCnt A ) ) ) e. CC ) /\ ( ( 1 ... A ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... A ) e. Fin ) ) -> sum_ p e. ( ( 1 ... A ) i^i Prime ) ( log ` ( p ^ ( p pCnt A ) ) ) = sum_ p e. ( 1 ... A ) if ( p e. ( ( 1 ... A ) i^i Prime ) , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) )
27 25 26 mpan2 
 |-  ( ( ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A ) /\ A. p e. ( ( 1 ... A ) i^i Prime ) ( log ` ( p ^ ( p pCnt A ) ) ) e. CC ) -> sum_ p e. ( ( 1 ... A ) i^i Prime ) ( log ` ( p ^ ( p pCnt A ) ) ) = sum_ p e. ( 1 ... A ) if ( p e. ( ( 1 ... A ) i^i Prime ) , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) )
28 11 23 27 sylancr 
 |-  ( A e. NN -> sum_ p e. ( ( 1 ... A ) i^i Prime ) ( log ` ( p ^ ( p pCnt A ) ) ) = sum_ p e. ( 1 ... A ) if ( p e. ( ( 1 ... A ) i^i Prime ) , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) )
29 15 nnrpd 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> p e. RR+ )
30 18 nn0zd 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( p pCnt A ) e. ZZ )
31 relogexp 
 |-  ( ( p e. RR+ /\ ( p pCnt A ) e. ZZ ) -> ( log ` ( p ^ ( p pCnt A ) ) ) = ( ( p pCnt A ) x. ( log ` p ) ) )
32 29 30 31 syl2anc 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( log ` ( p ^ ( p pCnt A ) ) ) = ( ( p pCnt A ) x. ( log ` p ) ) )
33 32 sumeq2dv 
 |-  ( A e. NN -> sum_ p e. ( ( 1 ... A ) i^i Prime ) ( log ` ( p ^ ( p pCnt A ) ) ) = sum_ p e. ( ( 1 ... A ) i^i Prime ) ( ( p pCnt A ) x. ( log ` p ) ) )
34 28 33 eqtr3d 
 |-  ( A e. NN -> sum_ p e. ( 1 ... A ) if ( p e. ( ( 1 ... A ) i^i Prime ) , ( log ` ( p ^ ( p pCnt A ) ) ) , 0 ) = sum_ p e. ( ( 1 ... A ) i^i Prime ) ( ( p pCnt A ) x. ( log ` p ) ) )
35 14 adantl 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> p e. NN )
36 eleq1w 
 |-  ( n = p -> ( n e. Prime <-> p e. Prime ) )
37 id 
 |-  ( n = p -> n = p )
38 oveq1 
 |-  ( n = p -> ( n pCnt A ) = ( p pCnt A ) )
39 37 38 oveq12d 
 |-  ( n = p -> ( n ^ ( n pCnt A ) ) = ( p ^ ( p pCnt A ) ) )
40 36 39 ifbieq1d 
 |-  ( n = p -> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) = if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) )
41 40 fveq2d 
 |-  ( n = p -> ( log ` if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) = ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) )
42 eqid 
 |-  ( n e. NN |-> ( log ` if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) = ( n e. NN |-> ( log ` if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) )
43 fvex 
 |-  ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) e. _V
44 41 42 43 fvmpt 
 |-  ( p e. NN -> ( ( n e. NN |-> ( log ` if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) ` p ) = ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) )
45 35 44 syl 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> ( ( n e. NN |-> ( log ` if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) ` p ) = ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) )
46 elnnuz 
 |-  ( A e. NN <-> A e. ( ZZ>= ` 1 ) )
47 46 biimpi 
 |-  ( A e. NN -> A e. ( ZZ>= ` 1 ) )
48 35 adantr 
 |-  ( ( ( A e. NN /\ p e. ( 1 ... A ) ) /\ p e. Prime ) -> p e. NN )
49 simpr 
 |-  ( ( ( A e. NN /\ p e. ( 1 ... A ) ) /\ p e. Prime ) -> p e. Prime )
50 simpll 
 |-  ( ( ( A e. NN /\ p e. ( 1 ... A ) ) /\ p e. Prime ) -> A e. NN )
51 49 50 pccld 
 |-  ( ( ( A e. NN /\ p e. ( 1 ... A ) ) /\ p e. Prime ) -> ( p pCnt A ) e. NN0 )
52 48 51 nnexpcld 
 |-  ( ( ( A e. NN /\ p e. ( 1 ... A ) ) /\ p e. Prime ) -> ( p ^ ( p pCnt A ) ) e. NN )
53 1nn 
 |-  1 e. NN
54 53 a1i 
 |-  ( ( ( A e. NN /\ p e. ( 1 ... A ) ) /\ -. p e. Prime ) -> 1 e. NN )
55 52 54 ifclda 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) e. NN )
56 55 nnrpd 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) e. RR+ )
57 56 relogcld 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) e. RR )
58 57 recnd 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) e. CC )
59 45 47 58 fsumser 
 |-  ( A e. NN -> sum_ p e. ( 1 ... A ) ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) = ( seq 1 ( + , ( n e. NN |-> ( log ` if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) ) ` A ) )
60 rpmulcl 
 |-  ( ( p e. RR+ /\ m e. RR+ ) -> ( p x. m ) e. RR+ )
61 60 adantl 
 |-  ( ( A e. NN /\ ( p e. RR+ /\ m e. RR+ ) ) -> ( p x. m ) e. RR+ )
62 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) )
63 ovex 
 |-  ( p ^ ( p pCnt A ) ) e. _V
64 1ex 
 |-  1 e. _V
65 63 64 ifex 
 |-  if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) e. _V
66 40 62 65 fvmpt 
 |-  ( p e. NN -> ( ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ` p ) = if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) )
67 35 66 syl 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ` p ) = if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) )
68 67 56 eqeltrd 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ` p ) e. RR+ )
69 relogmul 
 |-  ( ( p e. RR+ /\ m e. RR+ ) -> ( log ` ( p x. m ) ) = ( ( log ` p ) + ( log ` m ) ) )
70 69 adantl 
 |-  ( ( A e. NN /\ ( p e. RR+ /\ m e. RR+ ) ) -> ( log ` ( p x. m ) ) = ( ( log ` p ) + ( log ` m ) ) )
71 67 fveq2d 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> ( log ` ( ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ` p ) ) = ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) )
72 71 45 eqtr4d 
 |-  ( ( A e. NN /\ p e. ( 1 ... A ) ) -> ( log ` ( ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ` p ) ) = ( ( n e. NN |-> ( log ` if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) ` p ) )
73 61 68 47 70 72 seqhomo 
 |-  ( A e. NN -> ( log ` ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) ` A ) ) = ( seq 1 ( + , ( n e. NN |-> ( log ` if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) ) ` A ) )
74 62 pcprod 
 |-  ( A e. NN -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) ` A ) = A )
75 74 fveq2d 
 |-  ( A e. NN -> ( log ` ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt A ) ) , 1 ) ) ) ` A ) ) = ( log ` A ) )
76 59 73 75 3eqtr2d 
 |-  ( A e. NN -> sum_ p e. ( 1 ... A ) ( log ` if ( p e. Prime , ( p ^ ( p pCnt A ) ) , 1 ) ) = ( log ` A ) )
77 10 34 76 3eqtr3a 
 |-  ( A e. NN -> sum_ p e. ( ( 1 ... A ) i^i Prime ) ( ( p pCnt A ) x. ( log ` p ) ) = ( log ` A ) )