Metamath Proof Explorer


Theorem logfacbnd3

Description: Show the stronger statement log ( x ! ) = x log x - x + O ( log x ) alluded to in logfacrlim . (Contributed by Mario Carneiro, 20-May-2016)

Ref Expression
Assertion logfacbnd3 A + 1 A log A ! A log A 1 log A + 1

Proof

Step Hyp Ref Expression
1 simpl A + 1 A A +
2 1 rprege0d A + 1 A A 0 A
3 flge0nn0 A 0 A A 0
4 2 3 syl A + 1 A A 0
5 4 faccld A + 1 A A !
6 5 nnrpd A + 1 A A ! +
7 relogcl A ! + log A !
8 6 7 syl A + 1 A log A !
9 rpre A + A
10 9 adantr A + 1 A A
11 relogcl A + log A
12 11 adantr A + 1 A log A
13 peano2rem log A log A 1
14 12 13 syl A + 1 A log A 1
15 10 14 remulcld A + 1 A A log A 1
16 8 15 resubcld A + 1 A log A ! A log A 1
17 16 recnd A + 1 A log A ! A log A 1
18 17 abscld A + 1 A log A ! A log A 1
19 peano2rem log A ! A log A 1 log A ! A log A 1 1
20 18 19 syl A + 1 A log A ! A log A 1 1
21 ax-1cn 1
22 subcl log A ! A log A 1 1 log A ! - A log A 1 - 1
23 17 21 22 sylancl A + 1 A log A ! - A log A 1 - 1
24 23 abscld A + 1 A log A ! - A log A 1 - 1
25 abs1 1 = 1
26 25 oveq2i log A ! A log A 1 1 = log A ! A log A 1 1
27 abs2dif log A ! A log A 1 1 log A ! A log A 1 1 log A ! - A log A 1 - 1
28 17 21 27 sylancl A + 1 A log A ! A log A 1 1 log A ! - A log A 1 - 1
29 26 28 eqbrtrrid A + 1 A log A ! A log A 1 1 log A ! - A log A 1 - 1
30 fveq2 x = A x = A
31 30 oveq2d x = A 1 x = 1 A
32 31 sumeq1d x = A n = 1 x log n = n = 1 A log n
33 id x = A x = A
34 fveq2 x = A log x = log A
35 34 oveq1d x = A log x 1 = log A 1
36 33 35 oveq12d x = A x log x 1 = A log A 1
37 32 36 oveq12d x = A n = 1 x log n x log x 1 = n = 1 A log n A log A 1
38 eqid x + n = 1 x log n x log x 1 = x + n = 1 x log n x log x 1
39 ovex n = 1 x log n x log x 1 V
40 37 38 39 fvmpt3i A + x + n = 1 x log n x log x 1 A = n = 1 A log n A log A 1
41 40 adantr A + 1 A x + n = 1 x log n x log x 1 A = n = 1 A log n A log A 1
42 logfac A 0 log A ! = n = 1 A log n
43 4 42 syl A + 1 A log A ! = n = 1 A log n
44 43 oveq1d A + 1 A log A ! A log A 1 = n = 1 A log n A log A 1
45 41 44 eqtr4d A + 1 A x + n = 1 x log n x log x 1 A = log A ! A log A 1
46 1rp 1 +
47 fveq2 x = 1 x = 1
48 1z 1
49 flid 1 1 = 1
50 48 49 ax-mp 1 = 1
51 47 50 eqtrdi x = 1 x = 1
52 51 oveq2d x = 1 1 x = 1 1
53 52 sumeq1d x = 1 n = 1 x log n = n = 1 1 log n
54 0cn 0
55 fveq2 n = 1 log n = log 1
56 log1 log 1 = 0
57 55 56 eqtrdi n = 1 log n = 0
58 57 fsum1 1 0 n = 1 1 log n = 0
59 48 54 58 mp2an n = 1 1 log n = 0
60 53 59 eqtrdi x = 1 n = 1 x log n = 0
61 id x = 1 x = 1
62 fveq2 x = 1 log x = log 1
63 62 56 eqtrdi x = 1 log x = 0
64 63 oveq1d x = 1 log x 1 = 0 1
65 61 64 oveq12d x = 1 x log x 1 = 1 0 1
66 54 21 subcli 0 1
67 66 mulid2i 1 0 1 = 0 1
68 65 67 eqtrdi x = 1 x log x 1 = 0 1
69 60 68 oveq12d x = 1 n = 1 x log n x log x 1 = 0 0 1
70 nncan 0 1 0 0 1 = 1
71 54 21 70 mp2an 0 0 1 = 1
72 69 71 eqtrdi x = 1 n = 1 x log n x log x 1 = 1
73 72 38 39 fvmpt3i 1 + x + n = 1 x log n x log x 1 1 = 1
74 46 73 mp1i A + 1 A x + n = 1 x log n x log x 1 1 = 1
75 45 74 oveq12d A + 1 A x + n = 1 x log n x log x 1 A x + n = 1 x log n x log x 1 1 = log A ! - A log A 1 - 1
76 75 fveq2d A + 1 A x + n = 1 x log n x log x 1 A x + n = 1 x log n x log x 1 1 = log A ! - A log A 1 - 1
77 ioorp 0 +∞ = +
78 77 eqcomi + = 0 +∞
79 nnuz = 1
80 48 a1i A + 1 A 1
81 1re 1
82 81 a1i A + 1 A 1
83 pnfxr +∞ *
84 83 a1i A + 1 A +∞ *
85 1nn0 1 0
86 81 85 nn0addge1i 1 1 + 1
87 86 a1i A + 1 A 1 1 + 1
88 0red A + 1 A 0
89 rpre x + x
90 89 adantl A + 1 A x + x
91 relogcl x + log x
92 91 adantl A + 1 A x + log x
93 peano2rem log x log x 1
94 92 93 syl A + 1 A x + log x 1
95 90 94 remulcld A + 1 A x + x log x 1
96 nnrp x x +
97 96 92 sylan2 A + 1 A x log x
98 advlog dx + x log x 1 d x = x + log x
99 98 a1i A + 1 A dx + x log x 1 d x = x + log x
100 fveq2 x = n log x = log n
101 simp32 A + 1 A x + n + 1 x x n n +∞ x n
102 logleb x + n + x n log x log n
103 102 3ad2ant2 A + 1 A x + n + 1 x x n n +∞ x n log x log n
104 101 103 mpbid A + 1 A x + n + 1 x x n n +∞ log x log n
105 simprr A + 1 A x + 1 x 1 x
106 simprl A + 1 A x + 1 x x +
107 logleb 1 + x + 1 x log 1 log x
108 46 106 107 sylancr A + 1 A x + 1 x 1 x log 1 log x
109 105 108 mpbid A + 1 A x + 1 x log 1 log x
110 56 109 eqbrtrrid A + 1 A x + 1 x 0 log x
111 46 a1i A + 1 A 1 +
112 1le1 1 1
113 112 a1i A + 1 A 1 1
114 simpr A + 1 A 1 A
115 10 rexrd A + 1 A A *
116 pnfge A * A +∞
117 115 116 syl A + 1 A A +∞
118 78 79 80 82 84 87 88 95 92 97 99 100 104 38 110 111 1 113 114 117 34 dvfsum2 A + 1 A x + n = 1 x log n x log x 1 A x + n = 1 x log n x log x 1 1 log A
119 76 118 eqbrtrrd A + 1 A log A ! - A log A 1 - 1 log A
120 20 24 12 29 119 letrd A + 1 A log A ! A log A 1 1 log A
121 18 82 12 lesubaddd A + 1 A log A ! A log A 1 1 log A log A ! A log A 1 log A + 1
122 120 121 mpbid A + 1 A log A ! A log A 1 log A + 1