Theorem vmadivsum

Description: The sum of the von Mangoldt function over n is asymptotic to log x + O(1) . Equation 9.2.13 of Shapiro, p. 331. (Contributed by Mario Carneiro, 16-Apr-2016)

	Ref	Expression
Assertion	vmadivsum	⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		reex	⊢ ℝ ∈ V
2		rpssre	⊢ ℝ+ ⊆ ℝ
3	1 2	ssexi	⊢ ℝ+ ∈ V
4	3	a1i	⊢ ( ⊤ → ℝ+ ∈ V )
5		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ V )
6		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ V )
7		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) )
8		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) )
9	4 5 6 7 8	offval2	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ) )
10	9	mptru	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) )
11		fzfid	⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
12		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
13	12	adantl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
14		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
15	13 14	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
16	15 13	nndivred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
17	11 16	fsumrecl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
18	17	recnd	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
19		relogcl	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
20	19	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℂ )
21		rprege0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
22		flge0nn0	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
23		faccl	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℕ )
24	21 22 23	3syl	⊢ ( 𝑥 ∈ ℝ+ → ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℕ )
25	24	nnrpd	⊢ ( 𝑥 ∈ ℝ+ → ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℝ+ )
26	25	relogcld	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℝ )
27		rerpdivcl	⊢ ( ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℝ )
28	26 27	mpancom	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℝ )
29	28	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℂ )
30	18 20 29	nnncan2d	⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) )
31	30	mpteq2ia	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) − ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) )
32	10 31	eqtri	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) )
33		1red	⊢ ( ⊤ → 1 ∈ ℝ )
34		chpo1ub	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)
35	34	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
36		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
37		chpcl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
38	36 37	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℝ )
39		rerpdivcl	⊢ ( ( ( ψ ‘ 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
40	38 39	mpancom	⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
41	40	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
42	41	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
43	18 29	subcld	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ ℂ )
44	43	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ ℂ )
45	36	adantr	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
46	16 45	remulcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) ∈ ℝ )
47		nndivre	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
48	36 12 47	syl2an	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
49		reflcl	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
50	48 49	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
51	15 50	remulcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
52	46 51	resubcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
53	48 50	resubcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
54		1red	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
55		vmage0	⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
56	13 55	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
57		fracle1	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ 1 )
58	48 57	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ 1 )
59	53 54 15 56 58	lemul2ad	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ ( ( Λ ‘ 𝑛 ) · 1 ) )
60	15	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
61	48	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℂ )
62	50	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
63	60 61 62	subdid	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( 𝑥 / 𝑛 ) ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
64		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
65	64	adantr	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
66	13	nnrpd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
67		rpcnne0	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
68	66 67	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
69		div23	⊢ ( ( ( Λ ‘ 𝑛 ) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( ( Λ ‘ 𝑛 ) · 𝑥 ) / 𝑛 ) = ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) )
70		divass	⊢ ( ( ( Λ ‘ 𝑛 ) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( ( Λ ‘ 𝑛 ) · 𝑥 ) / 𝑛 ) = ( ( Λ ‘ 𝑛 ) · ( 𝑥 / 𝑛 ) ) )
71	69 70	eqtr3d	⊢ ( ( ( Λ ‘ 𝑛 ) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) = ( ( Λ ‘ 𝑛 ) · ( 𝑥 / 𝑛 ) ) )
72	60 65 68 71	syl3anc	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) = ( ( Λ ‘ 𝑛 ) · ( 𝑥 / 𝑛 ) ) )
73	72	oveq1d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( 𝑥 / 𝑛 ) ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
74	63 73	eqtr4d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
75	60	mulid1d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · 1 ) = ( Λ ‘ 𝑛 ) )
76	59 74 75	3brtr3d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ ( Λ ‘ 𝑛 ) )
77	11 52 15 76	fsumle	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )
78	16	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
79	11 64 78	fsummulc1	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) )
80		logfac2	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) )
81	21 80	syl	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) )
82	79 81	oveq12d	⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
83	46	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) ∈ ℂ )
84	51	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
85	11 83 84	fsumsub	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
86	82 85	eqtr4d	⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
87		chpval	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )
88	36 87	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )
89	77 86 88	3brtr4d	⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ≤ ( ψ ‘ 𝑥 ) )
90	17 36	remulcld	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) ∈ ℝ )
91	90 26	resubcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ∈ ℝ )
92		rpregt0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
93		lediv1	⊢ ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ∈ ℝ ∧ ( ψ ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ≤ ( ψ ‘ 𝑥 ) ↔ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ≤ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
94	91 38 92 93	syl3anc	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ≤ ( ψ ‘ 𝑥 ) ↔ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ≤ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
95	89 94	mpbid	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ≤ ( ( ψ ‘ 𝑥 ) / 𝑥 ) )
96	90	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) ∈ ℂ )
97	26	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℂ )
98		rpcnne0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
99		divsubdir	⊢ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) ∈ ℂ ∧ ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) / 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) )
100	96 97 98 99	syl3anc	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) / 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) )
101		rpne0	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
102	18 64 101	divcan4d	⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
103	102	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) / 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) )
104	100 103	eqtr2d	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) )
105	104	fveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) = ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ) )
106		rerpdivcl	⊢ ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ∈ ℝ )
107	91 106	mpancom	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ∈ ℝ )
108		flle	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( 𝑥 / 𝑛 ) )
109	48 108	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( 𝑥 / 𝑛 ) )
110	48 50	subge0d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 0 ≤ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ↔ ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( 𝑥 / 𝑛 ) ) )
111	109 110	mpbird	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) )
112	15 53 56 111	mulge0d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) · ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
113	112 74	breqtrd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
114	11 52 113	fsumge0	⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( ( Λ ‘ 𝑛 ) · ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
115	114 86	breqtrrd	⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) )
116		divge0	⊢ ( ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ∈ ℝ ∧ 0 ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → 0 ≤ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) )
117	91 115 92 116	syl21anc	⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) )
118	107 117	absidd	⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) )
119	105 118	eqtrd	⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝑥 ) − ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) ) / 𝑥 ) )
120		chpge0	⊢ ( 𝑥 ∈ ℝ → 0 ≤ ( ψ ‘ 𝑥 ) )
121	36 120	syl	⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ ( ψ ‘ 𝑥 ) )
122		divge0	⊢ ( ( ( ( ψ ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ψ ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → 0 ≤ ( ( ψ ‘ 𝑥 ) / 𝑥 ) )
123	38 121 92 122	syl21anc	⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ ( ( ψ ‘ 𝑥 ) / 𝑥 ) )
124	40 123	absidd	⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) = ( ( ψ ‘ 𝑥 ) / 𝑥 ) )
125	95 119 124	3brtr4d	⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ≤ ( abs ‘ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
126	125	ad2antrl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ≤ ( abs ‘ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
127	33 35 42 44 126	o1le	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1) )
128	127	mptru	⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1)
129		logfacrlim	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ⇝𝑟 1
130		rlimo1	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ⇝𝑟 1 → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1) )
131	129 130	ax-mp	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1)
132		o1sub	⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ) ∈ 𝑂(1) )
133	128 131 132	mp2an	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝑥 ) ) ) / 𝑥 ) ) ) ) ∈ 𝑂(1)
134	32 133	eqeltrri	⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)