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