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