Metamath Proof Explorer

Theorem logfaclbnd

Description: A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016)

Ref Expression
Assertion logfaclbnd 
|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) <_ ( log ` ( ! ` ( |_ ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( A e. RR+ -> A e. CC )
2 1 times2d 
 |-  ( A e. RR+ -> ( A x. 2 ) = ( A + A ) )
3 2 oveq2d 
 |-  ( A e. RR+ -> ( ( A x. ( log ` A ) ) - ( A x. 2 ) ) = ( ( A x. ( log ` A ) ) - ( A + A ) ) )
4 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
5 4 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
6 2cnd 
 |-  ( A e. RR+ -> 2 e. CC )
7 1 5 6 subdid 
 |-  ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) = ( ( A x. ( log ` A ) ) - ( A x. 2 ) ) )
8 rpre 
 |-  ( A e. RR+ -> A e. RR )
9 8 4 remulcld 
 |-  ( A e. RR+ -> ( A x. ( log ` A ) ) e. RR )
10 9 recnd 
 |-  ( A e. RR+ -> ( A x. ( log ` A ) ) e. CC )
11 10 1 1 subsub4d 
 |-  ( A e. RR+ -> ( ( ( A x. ( log ` A ) ) - A ) - A ) = ( ( A x. ( log ` A ) ) - ( A + A ) ) )
12 3 7 11 3eqtr4d 
 |-  ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) = ( ( ( A x. ( log ` A ) ) - A ) - A ) )
13 9 8 resubcld 
 |-  ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) e. RR )
14 fzfid 
 |-  ( A e. RR+ -> ( 1 ... ( |_ ` A ) ) e. Fin )
15 fzfid 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... n ) e. Fin )
16 elfznn 
 |-  ( d e. ( 1 ... n ) -> d e. NN )
17 16 adantl 
 |-  ( ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> d e. NN )
18 17 nnrecred 
 |-  ( ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> ( 1 / d ) e. RR )
19 15 18 fsumrecl 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ d e. ( 1 ... n ) ( 1 / d ) e. RR )
20 14 19 fsumrecl 
 |-  ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) e. RR )
21 rprege0 
 |-  ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) )
22 flge0nn0 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )
23 21 22 syl 
 |-  ( A e. RR+ -> ( |_ ` A ) e. NN0 )
24 23 faccld 
 |-  ( A e. RR+ -> ( ! ` ( |_ ` A ) ) e. NN )
25 24 nnrpd 
 |-  ( A e. RR+ -> ( ! ` ( |_ ` A ) ) e. RR+ )
26 25 relogcld 
 |-  ( A e. RR+ -> ( log ` ( ! ` ( |_ ` A ) ) ) e. RR )
27 26 8 readdcld 
 |-  ( A e. RR+ -> ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) e. RR )
28 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` A ) ) -> d e. NN )
29 28 adantl 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. NN )
30 29 nnrecred 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / d ) e. RR )
31 14 30 fsumrecl 
 |-  ( A e. RR+ -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) e. RR )
32 8 31 remulcld 
 |-  ( A e. RR+ -> ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) e. RR )
33 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
34 8 33 syl 
 |-  ( A e. RR+ -> ( |_ ` A ) e. RR )
35 32 34 resubcld 
 |-  ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) e. RR )
36 harmoniclbnd 
 |-  ( A e. RR+ -> ( log ` A ) <_ sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) )
37 rpregt0 
 |-  ( A e. RR+ -> ( A e. RR /\ 0 < A ) )
38 lemul2 
 |-  ( ( ( log ` A ) e. RR /\ sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( log ` A ) <_ sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) <-> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) ) )
39 4 31 37 38 syl3anc 
 |-  ( A e. RR+ -> ( ( log ` A ) <_ sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) <-> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) ) )
40 36 39 mpbid 
 |-  ( A e. RR+ -> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) )
41 flle 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
42 8 41 syl 
 |-  ( A e. RR+ -> ( |_ ` A ) <_ A )
43 9 34 32 8 40 42 le2subd 
 |-  ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) )
44 28 nnrecred 
 |-  ( d e. ( 1 ... ( |_ ` A ) ) -> ( 1 / d ) e. RR )
45 remulcl 
 |-  ( ( A e. RR /\ ( 1 / d ) e. RR ) -> ( A x. ( 1 / d ) ) e. RR )
46 8 44 45 syl2an 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A x. ( 1 / d ) ) e. RR )
47 peano2rem 
 |-  ( ( A x. ( 1 / d ) ) e. RR -> ( ( A x. ( 1 / d ) ) - 1 ) e. RR )
48 46 47 syl 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) e. RR )
49 fzfid 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( d ... ( |_ ` A ) ) e. Fin )
50 30 adantr 
 |-  ( ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ n e. ( d ... ( |_ ` A ) ) ) -> ( 1 / d ) e. RR )
51 49 50 fsumrecl 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) e. RR )
52 8 adantr 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> A e. RR )
53 52 33 syl 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` A ) e. RR )
54 peano2re 
 |-  ( ( |_ ` A ) e. RR -> ( ( |_ ` A ) + 1 ) e. RR )
55 53 54 syl 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( |_ ` A ) + 1 ) e. RR )
56 29 nnred 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. RR )
57 fllep1 
 |-  ( A e. RR -> A <_ ( ( |_ ` A ) + 1 ) )
58 8 57 syl 
 |-  ( A e. RR+ -> A <_ ( ( |_ ` A ) + 1 ) )
59 58 adantr 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> A <_ ( ( |_ ` A ) + 1 ) )
60 52 55 56 59 lesub1dd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A - d ) <_ ( ( ( |_ ` A ) + 1 ) - d ) )
61 52 56 resubcld 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A - d ) e. RR )
62 55 56 resubcld 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( |_ ` A ) + 1 ) - d ) e. RR )
63 29 nnrpd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. RR+ )
64 63 rpreccld 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / d ) e. RR+ )
65 61 62 64 lemul1d 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A - d ) <_ ( ( ( |_ ` A ) + 1 ) - d ) <-> ( ( A - d ) x. ( 1 / d ) ) <_ ( ( ( ( |_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) ) )
66 60 65 mpbid 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A - d ) x. ( 1 / d ) ) <_ ( ( ( ( |_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) )
67 1 adantr 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> A e. CC )
68 29 nncnd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. CC )
69 30 recnd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / d ) e. CC )
70 67 68 69 subdird 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A - d ) x. ( 1 / d ) ) = ( ( A x. ( 1 / d ) ) - ( d x. ( 1 / d ) ) ) )
71 29 nnne0d 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d =/= 0 )
72 68 71 recidd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( d x. ( 1 / d ) ) = 1 )
73 72 oveq2d 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - ( d x. ( 1 / d ) ) ) = ( ( A x. ( 1 / d ) ) - 1 ) )
74 70 73 eqtr2d 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) = ( ( A - d ) x. ( 1 / d ) ) )
75 fsumconst 
 |-  ( ( ( d ... ( |_ ` A ) ) e. Fin /\ ( 1 / d ) e. CC ) -> sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) = ( ( # ` ( d ... ( |_ ` A ) ) ) x. ( 1 / d ) ) )
76 49 69 75 syl2anc 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) = ( ( # ` ( d ... ( |_ ` A ) ) ) x. ( 1 / d ) ) )
77 elfzuz3 
 |-  ( d e. ( 1 ... ( |_ ` A ) ) -> ( |_ ` A ) e. ( ZZ>= ` d ) )
78 77 adantl 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` A ) e. ( ZZ>= ` d ) )
79 hashfz 
 |-  ( ( |_ ` A ) e. ( ZZ>= ` d ) -> ( # ` ( d ... ( |_ ` A ) ) ) = ( ( ( |_ ` A ) - d ) + 1 ) )
80 78 79 syl 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( # ` ( d ... ( |_ ` A ) ) ) = ( ( ( |_ ` A ) - d ) + 1 ) )
81 34 recnd 
 |-  ( A e. RR+ -> ( |_ ` A ) e. CC )
82 81 adantr 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` A ) e. CC )
83 1cnd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> 1 e. CC )
84 82 83 68 addsubd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( |_ ` A ) + 1 ) - d ) = ( ( ( |_ ` A ) - d ) + 1 ) )
85 80 84 eqtr4d 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( # ` ( d ... ( |_ ` A ) ) ) = ( ( ( |_ ` A ) + 1 ) - d ) )
86 85 oveq1d 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( # ` ( d ... ( |_ ` A ) ) ) x. ( 1 / d ) ) = ( ( ( ( |_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) )
87 76 86 eqtrd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) = ( ( ( ( |_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) )
88 66 74 87 3brtr4d 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) <_ sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) )
89 14 48 51 88 fsumle 
 |-  ( A e. RR+ -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) <_ sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) )
90 14 1 69 fsummulc2 
 |-  ( A e. RR+ -> ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( A x. ( 1 / d ) ) )
91 ax-1cn 
 |-  1 e. CC
92 fsumconst 
 |-  ( ( ( 1 ... ( |_ ` A ) ) e. Fin /\ 1 e. CC ) -> sum_ d e. ( 1 ... ( |_ ` A ) ) 1 = ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) )
93 14 91 92 sylancl 
 |-  ( A e. RR+ -> sum_ d e. ( 1 ... ( |_ ` A ) ) 1 = ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) )
94 hashfz1 
 |-  ( ( |_ ` A ) e. NN0 -> ( # ` ( 1 ... ( |_ ` A ) ) ) = ( |_ ` A ) )
95 23 94 syl 
 |-  ( A e. RR+ -> ( # ` ( 1 ... ( |_ ` A ) ) ) = ( |_ ` A ) )
96 95 oveq1d 
 |-  ( A e. RR+ -> ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) = ( ( |_ ` A ) x. 1 ) )
97 81 mulid1d 
 |-  ( A e. RR+ -> ( ( |_ ` A ) x. 1 ) = ( |_ ` A ) )
98 93 96 97 3eqtrrd 
 |-  ( A e. RR+ -> ( |_ ` A ) = sum_ d e. ( 1 ... ( |_ ` A ) ) 1 )
99 90 98 oveq12d 
 |-  ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) = ( sum_ d e. ( 1 ... ( |_ ` A ) ) ( A x. ( 1 / d ) ) - sum_ d e. ( 1 ... ( |_ ` A ) ) 1 ) )
100 46 recnd 
 |-  ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A x. ( 1 / d ) ) e. CC )
101 14 100 83 fsumsub 
 |-  ( A e. RR+ -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) = ( sum_ d e. ( 1 ... ( |_ ` A ) ) ( A x. ( 1 / d ) ) - sum_ d e. ( 1 ... ( |_ ` A ) ) 1 ) )
102 99 101 eqtr4d 
 |-  ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) )
103 eqid 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` 1 )
104 103 uztrn2 
 |-  ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) -> n e. ( ZZ>= ` 1 ) )
105 104 adantl 
 |-  ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> n e. ( ZZ>= ` 1 ) )
106 105 biantrurd 
 |-  ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( |_ ` A ) e. ( ZZ>= ` n ) <-> ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) )
107 uzss 
 |-  ( n e. ( ZZ>= ` d ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` d ) )
108 107 ad2antll 
 |-  ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` d ) )
109 108 sseld 
 |-  ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( |_ ` A ) e. ( ZZ>= ` n ) -> ( |_ ` A ) e. ( ZZ>= ` d ) ) )
110 109 pm4.71rd 
 |-  ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( |_ ` A ) e. ( ZZ>= ` n ) <-> ( ( |_ ` A ) e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) )
111 106 110 bitr3d 
 |-  ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) <-> ( ( |_ ` A ) e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) )
112 111 pm5.32da 
 |-  ( A e. RR+ -> ( ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( ( |_ ` A ) e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) )
113 ancom 
 |-  ( ( ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) )
114 an4 
 |-  ( ( ( d e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( ( |_ ` A ) e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) )
115 112 113 114 3bitr4g 
 |-  ( A e. RR+ -> ( ( ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) )
116 elfzuzb 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) <-> ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) )
117 elfzuzb 
 |-  ( d e. ( 1 ... n ) <-> ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) )
118 116 117 anbi12i 
 |-  ( ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. ( 1 ... n ) ) <-> ( ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) )
119 elfzuzb 
 |-  ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` d ) ) )
120 elfzuzb 
 |-  ( n e. ( d ... ( |_ ` A ) ) <-> ( n e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) )
121 119 120 anbi12i 
 |-  ( ( d e. ( 1 ... ( |_ ` A ) ) /\ n e. ( d ... ( |_ ` A ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) )
122 115 118 121 3bitr4g 
 |-  ( A e. RR+ -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. ( 1 ... n ) ) <-> ( d e. ( 1 ... ( |_ ` A ) ) /\ n e. ( d ... ( |_ ` A ) ) ) ) )
123 18 recnd 
 |-  ( ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> ( 1 / d ) e. CC )
124 123 anasss 
 |-  ( ( A e. RR+ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. ( 1 ... n ) ) ) -> ( 1 / d ) e. CC )
125 14 14 15 122 124 fsumcom2 
 |-  ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) )
126 89 102 125 3brtr4d 
 |-  ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) )
127 13 35 20 43 126 letrd 
 |-  ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) )
128 26 34 readdcld 
 |-  ( A e. RR+ -> ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) e. RR )
129 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
130 129 adantl 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
131 130 nnrpd 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. RR+ )
132 131 relogcld 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` n ) e. RR )
133 peano2re 
 |-  ( ( log ` n ) e. RR -> ( ( log ` n ) + 1 ) e. RR )
134 132 133 syl 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` n ) + 1 ) e. RR )
135 nnz 
 |-  ( n e. NN -> n e. ZZ )
136 flid 
 |-  ( n e. ZZ -> ( |_ ` n ) = n )
137 135 136 syl 
 |-  ( n e. NN -> ( |_ ` n ) = n )
138 137 oveq2d 
 |-  ( n e. NN -> ( 1 ... ( |_ ` n ) ) = ( 1 ... n ) )
139 138 sumeq1d 
 |-  ( n e. NN -> sum_ d e. ( 1 ... ( |_ ` n ) ) ( 1 / d ) = sum_ d e. ( 1 ... n ) ( 1 / d ) )
140 nnre 
 |-  ( n e. NN -> n e. RR )
141 nnge1 
 |-  ( n e. NN -> 1 <_ n )
142 harmonicubnd 
 |-  ( ( n e. RR /\ 1 <_ n ) -> sum_ d e. ( 1 ... ( |_ ` n ) ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) )
143 140 141 142 syl2anc 
 |-  ( n e. NN -> sum_ d e. ( 1 ... ( |_ ` n ) ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) )
144 139 143 eqbrtrrd 
 |-  ( n e. NN -> sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) )
145 130 144 syl 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) )
146 14 19 134 145 fsumle 
 |-  ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) + 1 ) )
147 132 recnd 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` n ) e. CC )
148 1cnd 
 |-  ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> 1 e. CC )
149 14 147 148 fsumadd 
 |-  ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) + 1 ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) + sum_ n e. ( 1 ... ( |_ ` A ) ) 1 ) )
150 logfac 
 |-  ( ( |_ ` A ) e. NN0 -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
151 23 150 syl 
 |-  ( A e. RR+ -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
152 fsumconst 
 |-  ( ( ( 1 ... ( |_ ` A ) ) e. Fin /\ 1 e. CC ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) 1 = ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) )
153 14 91 152 sylancl 
 |-  ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) 1 = ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) )
154 153 96 97 3eqtrrd 
 |-  ( A e. RR+ -> ( |_ ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) 1 )
155 151 154 oveq12d 
 |-  ( A e. RR+ -> ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) + sum_ n e. ( 1 ... ( |_ ` A ) ) 1 ) )
156 149 155 eqtr4d 
 |-  ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) + 1 ) = ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) )
157 146 156 breqtrd 
 |-  ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) )
158 34 8 26 42 leadd2dd 
 |-  ( A e. RR+ -> ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) )
159 20 128 27 157 158 letrd 
 |-  ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) )
160 13 20 27 127 159 letrd 
 |-  ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) )
161 13 8 26 lesubaddd 
 |-  ( A e. RR+ -> ( ( ( ( A x. ( log ` A ) ) - A ) - A ) <_ ( log ` ( ! ` ( |_ ` A ) ) ) <-> ( ( A x. ( log ` A ) ) - A ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) ) )
162 160 161 mpbird 
 |-  ( A e. RR+ -> ( ( ( A x. ( log ` A ) ) - A ) - A ) <_ ( log ` ( ! ` ( |_ ` A ) ) ) )
163 12 162 eqbrtrd 
 |-  ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) <_ ( log ` ( ! ` ( |_ ` A ) ) ) )