Metamath Proof Explorer

Theorem logfac2

Description: Another expression for the logarithm of a factorial, in terms of the von Mangoldt function. Equation 9.2.7 of Shapiro, p. 329. (Contributed by Mario Carneiro, 15-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

Ref Expression
Assertion logfac2 
|- ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ k e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` k ) x. ( |_ ` ( A / k ) ) ) )

Proof

Step Hyp Ref Expression
1 flge0nn0 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )
2 logfac 
 |-  ( ( |_ ` A ) e. NN0 -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
3 1 2 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
4 fzfid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 1 ... ( |_ ` A ) ) e. Fin )
5 fzfid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... ( |_ ` A ) ) e. Fin )
6 ssrab2 
 |-  { x e. ( 1 ... ( |_ ` A ) ) | k || x } C_ ( 1 ... ( |_ ` A ) )
7 ssfi 
 |-  ( ( ( 1 ... ( |_ ` A ) ) e. Fin /\ { x e. ( 1 ... ( |_ ` A ) ) | k || x } C_ ( 1 ... ( |_ ` A ) ) ) -> { x e. ( 1 ... ( |_ ` A ) ) | k || x } e. Fin )
8 5 6 7 sylancl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> { x e. ( 1 ... ( |_ ` A ) ) | k || x } e. Fin )
9 flcl 
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
10 9 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. ZZ )
11 fznn 
 |-  ( ( |_ ` A ) e. ZZ -> ( k e. ( 1 ... ( |_ ` A ) ) <-> ( k e. NN /\ k <_ ( |_ ` A ) ) ) )
12 10 11 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( k e. ( 1 ... ( |_ ` A ) ) <-> ( k e. NN /\ k <_ ( |_ ` A ) ) ) )
13 12 anbi1d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( k e. ( 1 ... ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) <-> ( ( k e. NN /\ k <_ ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) ) )
14 nnre 
 |-  ( k e. NN -> k e. RR )
15 14 ad2antlr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> k e. RR )
16 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
17 16 ad2antrl 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> n e. NN )
18 17 nnred 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> n e. RR )
19 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
20 19 ad3antrrr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> ( |_ ` A ) e. RR )
21 simprr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> k || n )
22 nnz 
 |-  ( k e. NN -> k e. ZZ )
23 22 ad2antlr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> k e. ZZ )
24 dvdsle 
 |-  ( ( k e. ZZ /\ n e. NN ) -> ( k || n -> k <_ n ) )
25 23 17 24 syl2anc 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> ( k || n -> k <_ n ) )
26 21 25 mpd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> k <_ n )
27 elfzle2 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n <_ ( |_ ` A ) )
28 27 ad2antrl 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> n <_ ( |_ ` A ) )
29 15 18 20 26 28 letrd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ k e. NN ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> k <_ ( |_ ` A ) )
30 29 expl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( k e. NN /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) -> k <_ ( |_ ` A ) ) )
31 30 pm4.71rd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( k e. NN /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) <-> ( k <_ ( |_ ` A ) /\ ( k e. NN /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) ) ) )
32 an12 
 |-  ( ( n e. ( 1 ... ( |_ ` A ) ) /\ ( k e. NN /\ k || n ) ) <-> ( k e. NN /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) )
33 an21 
 |-  ( ( ( k e. NN /\ k <_ ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) <-> ( k <_ ( |_ ` A ) /\ ( k e. NN /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) ) )
34 31 32 33 3bitr4g 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ ( k e. NN /\ k || n ) ) <-> ( ( k e. NN /\ k <_ ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) ) )
35 13 34 bitr4d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( k e. ( 1 ... ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) <-> ( n e. ( 1 ... ( |_ ` A ) ) /\ ( k e. NN /\ k || n ) ) ) )
36 breq2 
 |-  ( x = n -> ( k || x <-> k || n ) )
37 36 elrab 
 |-  ( n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } <-> ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) )
38 37 anbi2i 
 |-  ( ( k e. ( 1 ... ( |_ ` A ) ) /\ n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } ) <-> ( k e. ( 1 ... ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ k || n ) ) )
39 breq1 
 |-  ( x = k -> ( x || n <-> k || n ) )
40 39 elrab 
 |-  ( k e. { x e. NN | x || n } <-> ( k e. NN /\ k || n ) )
41 40 anbi2i 
 |-  ( ( n e. ( 1 ... ( |_ ` A ) ) /\ k e. { x e. NN | x || n } ) <-> ( n e. ( 1 ... ( |_ ` A ) ) /\ ( k e. NN /\ k || n ) ) )
42 35 38 41 3bitr4g 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( k e. ( 1 ... ( |_ ` A ) ) /\ n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } ) <-> ( n e. ( 1 ... ( |_ ` A ) ) /\ k e. { x e. NN | x || n } ) ) )
43 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` A ) ) -> k e. NN )
44 43 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> k e. NN )
45 vmacl 
 |-  ( k e. NN -> ( Lam ` k ) e. RR )
46 44 45 syl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` k ) e. RR )
47 46 recnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` k ) e. CC )
48 47 adantrr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( k e. ( 1 ... ( |_ ` A ) ) /\ n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } ) ) -> ( Lam ` k ) e. CC )
49 4 4 8 42 48 fsumcom2 
 |-  ( ( A e. RR /\ 0 <_ A ) -> sum_ k e. ( 1 ... ( |_ ` A ) ) sum_ n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } ( Lam ` k ) = sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ k e. { x e. NN | x || n } ( Lam ` k ) )
50 fsumconst 
 |-  ( ( { x e. ( 1 ... ( |_ ` A ) ) | k || x } e. Fin /\ ( Lam ` k ) e. CC ) -> sum_ n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } ( Lam ` k ) = ( ( # ` { x e. ( 1 ... ( |_ ` A ) ) | k || x } ) x. ( Lam ` k ) ) )
51 8 47 50 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } ( Lam ` k ) = ( ( # ` { x e. ( 1 ... ( |_ ` A ) ) | k || x } ) x. ( Lam ` k ) ) )
52 fzfid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... ( |_ ` ( A / k ) ) ) e. Fin )
53 simpll 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> A e. RR )
54 eqid 
 |-  ( m e. ( 1 ... ( |_ ` ( A / k ) ) ) |-> ( k x. m ) ) = ( m e. ( 1 ... ( |_ ` ( A / k ) ) ) |-> ( k x. m ) )
55 53 44 54 dvdsflf1o 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( m e. ( 1 ... ( |_ ` ( A / k ) ) ) |-> ( k x. m ) ) : ( 1 ... ( |_ ` ( A / k ) ) ) -1-1-onto-> { x e. ( 1 ... ( |_ ` A ) ) | k || x } )
56 52 55 hasheqf1od 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( # ` ( 1 ... ( |_ ` ( A / k ) ) ) ) = ( # ` { x e. ( 1 ... ( |_ ` A ) ) | k || x } ) )
57 simpl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. RR )
58 nndivre 
 |-  ( ( A e. RR /\ k e. NN ) -> ( A / k ) e. RR )
59 57 43 58 syl2an 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( A / k ) e. RR )
60 nngt0 
 |-  ( k e. NN -> 0 < k )
61 14 60 jca 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
62 43 61 syl 
 |-  ( k e. ( 1 ... ( |_ ` A ) ) -> ( k e. RR /\ 0 < k ) )
63 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( k e. RR /\ 0 < k ) ) -> 0 <_ ( A / k ) )
64 62 63 sylan2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> 0 <_ ( A / k ) )
65 flge0nn0 
 |-  ( ( ( A / k ) e. RR /\ 0 <_ ( A / k ) ) -> ( |_ ` ( A / k ) ) e. NN0 )
66 59 64 65 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` ( A / k ) ) e. NN0 )
67 hashfz1 
 |-  ( ( |_ ` ( A / k ) ) e. NN0 -> ( # ` ( 1 ... ( |_ ` ( A / k ) ) ) ) = ( |_ ` ( A / k ) ) )
68 66 67 syl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( # ` ( 1 ... ( |_ ` ( A / k ) ) ) ) = ( |_ ` ( A / k ) ) )
69 56 68 eqtr3d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( # ` { x e. ( 1 ... ( |_ ` A ) ) | k || x } ) = ( |_ ` ( A / k ) ) )
70 69 oveq1d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( ( # ` { x e. ( 1 ... ( |_ ` A ) ) | k || x } ) x. ( Lam ` k ) ) = ( ( |_ ` ( A / k ) ) x. ( Lam ` k ) ) )
71 59 flcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` ( A / k ) ) e. ZZ )
72 71 zcnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` ( A / k ) ) e. CC )
73 72 47 mulcomd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( ( |_ ` ( A / k ) ) x. ( Lam ` k ) ) = ( ( Lam ` k ) x. ( |_ ` ( A / k ) ) ) )
74 51 70 73 3eqtrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ k e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } ( Lam ` k ) = ( ( Lam ` k ) x. ( |_ ` ( A / k ) ) ) )
75 74 sumeq2dv 
 |-  ( ( A e. RR /\ 0 <_ A ) -> sum_ k e. ( 1 ... ( |_ ` A ) ) sum_ n e. { x e. ( 1 ... ( |_ ` A ) ) | k || x } ( Lam ` k ) = sum_ k e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` k ) x. ( |_ ` ( A / k ) ) ) )
76 16 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
77 vmasum 
 |-  ( n e. NN -> sum_ k e. { x e. NN | x || n } ( Lam ` k ) = ( log ` n ) )
78 76 77 syl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ k e. { x e. NN | x || n } ( Lam ` k ) = ( log ` n ) )
79 78 sumeq2dv 
 |-  ( ( A e. RR /\ 0 <_ A ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ k e. { x e. NN | x || n } ( Lam ` k ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
80 49 75 79 3eqtr3d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> sum_ k e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` k ) x. ( |_ ` ( A / k ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
81 3 80 eqtr4d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ k e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` k ) x. ( |_ ` ( A / k ) ) ) )