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	mullidi	⊢ ( 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 ) )