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