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 ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) − ( 𝐴 · ( ( log ‘ 𝐴 ) − 1 ) ) ) ) ≤ ( ( log ‘ 𝐴 ) + 1 ) )

Proof

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