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