This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem logfacrlim

Description: Combine the estimates logfacubnd and logfaclbnd , to get log ( x ! ) = x log x + O ( x ) . Equation 9.2.9 of Shapiro, p. 329. This is a weak form of the even stronger statement, log ( x ! ) = x log x - x + O ( log x ) . (Contributed by Mario Carneiro, 16-Apr-2016) (Revised by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion logfacrlim ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ⇝𝑟 1

Proof

Step Hyp Ref Expression
1 1red ⊢ ( ⊤ → 1 ∈ ℝ )
2 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
3 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
4 3 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
5 4 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
6 1cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
7 rpcnne0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
8 7 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
9 divdir ⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) = ( ( ( log ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) )
10 5 6 8 9 syl3anc ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) = ( ( ( log ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) )
11 10 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) )
12 simpr ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
13 4 12 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
14 rpreccl ⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
15 14 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ+ )
16 15 rpred ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ )
17 8 simpld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
18 17 cxp1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 1 ) = 𝑥 )
19 18 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 1 ) ) = ( ( log ‘ 𝑥 ) / 𝑥 ) )
20 19 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 1 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) ) )
21 1rp ⊢ 1 ∈ ℝ+
22 cxploglim ⊢ ( 1 ∈ ℝ+ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 1 ) ) ) ⇝𝑟 0 )
23 21 22 mp1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 1 ) ) ) ⇝𝑟 0 )
24 20 23 eqbrtrrd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 0 )
25 ax-1cn ⊢ 1 ∈ ℂ
26 divrcnv ⊢ ( 1 ∈ ℂ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0 )
27 25 26 mp1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0 )
28 13 16 24 27 rlimadd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) ⇝𝑟 ( 0 + 0 ) )
29 11 28 eqbrtrd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) ⇝𝑟 ( 0 + 0 ) )
30 00id ⊢ ( 0 + 0 ) = 0
31 29 30 breqtrdi ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) ⇝𝑟 0 )
32 peano2re ⊢ ( ( log ‘ 𝑥 ) ∈ ℝ → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℝ )
33 4 32 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℝ )
34 33 12 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℝ )
35 34 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℂ )
36 rprege0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
37 36 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
38 flge0nn0 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
39 faccl ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℕ )
40 37 38 39 3syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℕ )
41 40 nnrpd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℝ+ )
42 relogcl ⊢ ( ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℝ+ → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℝ )
43 41 42 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℝ )
44 43 12 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℝ )
45 44 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℂ )
46 5 45 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ ℂ )
47 logfacbnd3 ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
48 47 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
49 43 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℂ )
50 49 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℂ )
51 7 ad2antrl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
52 51 simpld ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℂ )
53 5 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
54 subcl ⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( log ‘ 𝑥 ) − 1 ) ∈ ℂ )
55 53 25 54 sylancl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) − 1 ) ∈ ℂ )
56 52 55 mulcld ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ∈ ℂ )
57 50 56 subcld ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ∈ ℂ )
58 57 abscld ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) ∈ ℝ )
59 4 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
60 59 32 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℝ )
61 rpregt0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
62 61 ad2antrl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
63 lediv1 ⊢ ( ( ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) ∈ ℝ ∧ ( ( log ‘ 𝑥 ) + 1 ) ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) ≤ ( ( log ‘ 𝑥 ) + 1 ) ↔ ( ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) / 𝑥 ) ≤ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
64 58 60 62 63 syl3anc ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) ≤ ( ( log ‘ 𝑥 ) + 1 ) ↔ ( ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) / 𝑥 ) ≤ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
65 48 64 mpbid ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) / 𝑥 ) ≤ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) )
66 51 simprd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ≠ 0 )
67 55 52 66 divcan3d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) / 𝑥 ) = ( ( log ‘ 𝑥 ) − 1 ) )
68 67 oveq1d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) / 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) = ( ( ( log ‘ 𝑥 ) − 1 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) )
69 divsubdir ⊢ ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ∈ ℂ ∧ ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) = ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) / 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) )
70 56 50 51 69 syl3anc ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) = ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) / 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) )
71 45 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℂ )
72 1cnd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℂ )
73 53 71 72 sub32d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − 1 ) = ( ( ( log ‘ 𝑥 ) − 1 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) )
74 68 70 73 3eqtr4rd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − 1 ) = ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) )
75 74 fveq2d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − 1 ) ) = ( abs ‘ ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ) )
76 56 50 subcld ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ∈ ℂ )
77 76 52 66 absdivd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ) = ( ( abs ‘ ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) / ( abs ‘ 𝑥 ) ) )
78 56 50 abssubd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) = ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) )
79 36 ad2antrl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
80 absid ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( abs ‘ 𝑥 ) = 𝑥 )
81 79 80 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ 𝑥 ) = 𝑥 )
82 78 81 oveq12d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( abs ‘ ( ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) / ( abs ‘ 𝑥 ) ) = ( ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) / 𝑥 ) )
83 75 77 82 3eqtrd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − 1 ) ) = ( ( abs ‘ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) − ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) / 𝑥 ) )
84 35 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℂ )
85 84 subid1d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) − 0 ) = ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) )
86 85 fveq2d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) − 0 ) ) = ( abs ‘ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
87 log1 ⊢ ( log ‘ 1 ) = 0
88 simprr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
89 12 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
90 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) )
91 21 89 90 sylancr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) )
92 88 91 mpbid ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) )
93 87 92 eqbrtrrid ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( log ‘ 𝑥 ) )
94 59 93 ge0p1rpd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℝ+ )
95 94 89 rpdivcld ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℝ+ )
96 rprege0 ⊢ ( ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℝ+ → ( ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
97 absid ⊢ ( ( ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) → ( abs ‘ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) = ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) )
98 95 96 97 3syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) ) = ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) )
99 86 98 eqtrd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) − 0 ) ) = ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) )
100 65 83 99 3brtr4d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − 1 ) ) ≤ ( abs ‘ ( ( ( ( log ‘ 𝑥 ) + 1 ) / 𝑥 ) − 0 ) ) )
101 1 2 31 35 46 100 rlimsqzlem ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ⇝𝑟 1 )
102 101 mptru ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ⇝𝑟 1