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