logexprlim

Description: The sum sum_ n <_ x , log ^ N ( x / n ) has the asymptotic expansion ( N ! ) x + o ( x ) . (More precisely, the omitted term has order O ( log ^ N ( x ) / x ) .) (Contributed by Mario Carneiro, 22-May-2016)

		Ref	Expression
	Assertion	logexprlim	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x}) \underset{ℝ}{⇝} N!$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
2		simpr	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to x \in ℝ^{+}$
3		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
4	3	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
5		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
6	2 4 5	syl2an	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
7	6	relogcld	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
8		simpll	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to N \in ℕ_{0}$
9	7 8	reexpcld	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{N} \in ℝ$
10	1 9	fsumrecl	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} \in ℝ$
11		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
12		id	$⊢ N \in ℕ_{0} \to N \in ℕ_{0}$
13		reexpcl	$⊢ (\log x \in ℝ \land N \in ℕ_{0}) \to {\log x}^{N} \in ℝ$
14	11 12 13	syl2anr	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to {\log x}^{N} \in ℝ$
15		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
16	15	adantr	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to N! \in ℕ$
17	16	nnred	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to N! \in ℝ$
18		fzfid	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to (0 \dots N) \in Fin$
19	11	adantl	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \log x \in ℝ$
20		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
21		reexpcl	$⊢ (\log x \in ℝ \land k \in ℕ_{0}) \to {\log x}^{k} \in ℝ$
22	19 20 21	syl2an	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to {\log x}^{k} \in ℝ$
23	20	adantl	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to k \in ℕ_{0}$
24	23	faccld	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to k! \in ℕ$
25	22 24	nndivred	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to \frac{{\log x}^{k}}{k!} \in ℝ$
26	18 25	fsumrecl	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℝ$
27	17 26	remulcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℝ$
28	14 27	resubcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to {\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℝ$
29	10 28	resubcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})) \in ℝ$
30	29 2	rerpdivcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x} \in ℝ$
31		rerpdivcl	$⊢ ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℝ \land x \in ℝ^{+}) \to \frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} \in ℝ$
32	28 31	sylancom	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} \in ℝ$
33		1red	$⊢ N \in ℕ_{0} \to 1 \in ℝ$
34	15	nncnd	$⊢ N \in ℕ_{0} \to N! \in ℂ$
35		simpl	$⊢ (k = N \land x \in ℝ^{+}) \to k = N$
36	35	oveq2d	$⊢ (k = N \land x \in ℝ^{+}) \to {\log x}^{k} = {\log x}^{N}$
37	36	oveq1d	$⊢ (k = N \land x \in ℝ^{+}) \to \frac{{\log x}^{k}}{x} = \frac{{\log x}^{N}}{x}$
38	37	mpteq2dva	$⊢ k = N \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{k}}{x}) = (x \in ℝ^{+} ⟼ \frac{{\log x}^{N}}{x})$
39	38	breq1d	$⊢ k = N \to ((x \in ℝ^{+} ⟼ \frac{{\log x}^{k}}{x}) \underset{ℝ}{⇝} 0 \leftrightarrow (x \in ℝ^{+} ⟼ \frac{{\log x}^{N}}{x}) \underset{ℝ}{⇝} 0)$
40	11	recnd	$⊢ x \in ℝ^{+} \to \log x \in ℂ$
41		id	$⊢ k \in ℕ_{0} \to k \in ℕ_{0}$
42		cxpexp	$⊢ (\log x \in ℂ \land k \in ℕ_{0}) \to {\log x}^{k} = {\log x}^{k}$
43	40 41 42	syl2anr	$⊢ (k \in ℕ_{0} \land x \in ℝ^{+}) \to {\log x}^{k} = {\log x}^{k}$
44		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
45	44	adantl	$⊢ (k \in ℕ_{0} \land x \in ℝ^{+}) \to x \in ℂ$
46	45	cxp1d	$⊢ (k \in ℕ_{0} \land x \in ℝ^{+}) \to x^{1} = x$
47	43 46	oveq12d	$⊢ (k \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{{\log x}^{k}}{x^{1}} = \frac{{\log x}^{k}}{x}$
48	47	mpteq2dva	$⊢ k \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{k}}{x^{1}}) = (x \in ℝ^{+} ⟼ \frac{{\log x}^{k}}{x})$
49		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
50		1rp	$⊢ 1 \in ℝ^{+}$
51		cxploglim2	$⊢ (k \in ℂ \land 1 \in ℝ^{+}) \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{k}}{x^{1}}) \underset{ℝ}{⇝} 0$
52	49 50 51	sylancl	$⊢ k \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{k}}{x^{1}}) \underset{ℝ}{⇝} 0$
53	48 52	eqbrtrrd	$⊢ k \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{k}}{x}) \underset{ℝ}{⇝} 0$
54	39 53	vtoclga	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{N}}{x}) \underset{ℝ}{⇝} 0$
55		rerpdivcl	$⊢ ({\log x}^{N} \in ℝ \land x \in ℝ^{+}) \to \frac{{\log x}^{N}}{x} \in ℝ$
56	14 55	sylancom	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{{\log x}^{N}}{x} \in ℝ$
57	56	recnd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{{\log x}^{N}}{x} \in ℂ$
58	10	recnd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} \in ℂ$
59	14	recnd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to {\log x}^{N} \in ℂ$
60	34	adantr	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to N! \in ℂ$
61	26	recnd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ$
62	60 61	mulcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ$
63	59 62	subcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to {\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ$
64	58 63	subcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})) \in ℂ$
65		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
66	65	adantl	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to (x \in ℂ \land x \neq 0)$
67	66	simpld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to x \in ℂ$
68	66	simprd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to x \neq 0$
69	64 67 68	divcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x} \in ℂ$
70	69	adantrr	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x} \in ℂ$
71	15	adantr	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to N! \in ℕ$
72	71	nncnd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to N! \in ℂ$
73	70 72	subcld	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N! \in ℂ$
74	73	abscld	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| \in ℝ$
75	56	adantrr	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{{\log x}^{N}}{x} \in ℝ$
76	75	recnd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{{\log x}^{N}}{x} \in ℂ$
77	76	abscld	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\frac{{\log x}^{N}}{x}\| \in ℝ$
78		ioorp	$⊢ (0, +∞) = ℝ^{+}$
79	78	eqcomi	$⊢ ℝ^{+} = (0, +∞)$
80		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
81		1z	$⊢ 1 \in ℤ$
82	81	a1i	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in ℤ$
83		1red	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in ℝ$
84		1re	$⊢ 1 \in ℝ$
85		1nn0	$⊢ 1 \in ℕ_{0}$
86	84 85	nn0addge1i	$⊢ 1 \leq 1 + 1$
87	86	a1i	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq 1 + 1$
88		0red	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \in ℝ$
89	71	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to N! \in ℕ$
90	89	nnred	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to N! \in ℝ$
91		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
92	91	adantl	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to y \in ℝ$
93		fzfid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to (0 \dots N) \in Fin$
94		simprl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ^{+}$
95		rpdivcl	$⊢ (x \in ℝ^{+} \land y \in ℝ^{+}) \to \frac{x}{y} \in ℝ^{+}$
96	94 95	sylan	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to \frac{x}{y} \in ℝ^{+}$
97	96	relogcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to \log (\frac{x}{y}) \in ℝ$
98		reexpcl	$⊢ (\log (\frac{x}{y}) \in ℝ \land k \in ℕ_{0}) \to {\log (\frac{x}{y})}^{k} \in ℝ$
99	97 20 98	syl2an	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \land k \in (0 \dots N)) \to {\log (\frac{x}{y})}^{k} \in ℝ$
100	20	adantl	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \land k \in (0 \dots N)) \to k \in ℕ_{0}$
101	100	faccld	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \land k \in (0 \dots N)) \to k! \in ℕ$
102	99 101	nndivred	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \land k \in (0 \dots N)) \to \frac{{\log (\frac{x}{y})}^{k}}{k!} \in ℝ$
103	93 102	fsumrecl	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) \in ℝ$
104	92 103	remulcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) \in ℝ$
105	90 104	remulcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) \in ℝ$
106		simpll	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to N \in ℕ_{0}$
107	97 106	reexpcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to {\log (\frac{x}{y})}^{N} \in ℝ$
108		nnrp	$⊢ y \in ℕ \to y \in ℝ^{+}$
109	108 107	sylan2	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℕ) \to {\log (\frac{x}{y})}^{N} \in ℝ$
110		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
111	110	a1i	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to ℝ \in \{ℝ, ℂ\}$
112	104	recnd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) \in ℂ$
113	107 89	nndivred	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to \frac{{\log (\frac{x}{y})}^{N}}{N!} \in ℝ$
114		simpl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to N \in ℕ_{0}$
115		advlogexp	$⊢ (x \in ℝ^{+} \land N \in ℕ_{0}) \to \frac{d (y \in ℝ^{+}⟼ y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}))}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ \frac{{\log (\frac{x}{y})}^{N}}{N!})$
116	94 114 115	syl2anc	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{d (y \in ℝ^{+}⟼ y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}))}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ \frac{{\log (\frac{x}{y})}^{N}}{N!})$
117	111 112 113 116 72	dvmptcmul	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{d (y \in ℝ^{+}⟼ N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}))}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ N! (\frac{{\log (\frac{x}{y})}^{N}}{N!}))$
118	107	recnd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to {\log (\frac{x}{y})}^{N} \in ℂ$
119	72	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to N! \in ℂ$
120	71	nnne0d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to N! \neq 0$
121	120	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to N! \neq 0$
122	118 119 121	divcan2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to N! (\frac{{\log (\frac{x}{y})}^{N}}{N!}) = {\log (\frac{x}{y})}^{N}$
123	122	mpteq2dva	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (y \in ℝ^{+} ⟼ N! (\frac{{\log (\frac{x}{y})}^{N}}{N!})) = (y \in ℝ^{+} ⟼ {\log (\frac{x}{y})}^{N})$
124	117 123	eqtrd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{d (y \in ℝ^{+}⟼ N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}))}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ {\log (\frac{x}{y})}^{N})$
125		oveq2	$⊢ y = n \to \frac{x}{y} = \frac{x}{n}$
126	125	fveq2d	$⊢ y = n \to \log (\frac{x}{y}) = \log (\frac{x}{n})$
127	126	oveq1d	$⊢ y = n \to {\log (\frac{x}{y})}^{N} = {\log (\frac{x}{n})}^{N}$
128	94	rpxrd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ^{*}$
129		simp1rl	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to x \in ℝ^{+}$
130		simp2r	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to n \in ℝ^{+}$
131	129 130	rpdivcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to \frac{x}{n} \in ℝ^{+}$
132	131	relogcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to \log (\frac{x}{n}) \in ℝ$
133		simp2l	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to y \in ℝ^{+}$
134	129 133	rpdivcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to \frac{x}{y} \in ℝ^{+}$
135	134	relogcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to \log (\frac{x}{y}) \in ℝ$
136		simp1l	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to N \in ℕ_{0}$
137		log1	$⊢ \log 1 = 0$
138	130	rpcnd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to n \in ℂ$
139	138	mulid2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to 1 n = n$
140		simp33	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to n \leq x$
141	139 140	eqbrtrd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to 1 n \leq x$
142		1red	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to 1 \in ℝ$
143	129	rpred	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to x \in ℝ$
144	142 143 130	lemuldivd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to (1 n \leq x \leftrightarrow 1 \leq \frac{x}{n})$
145	141 144	mpbid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to 1 \leq \frac{x}{n}$
146		logleb	$⊢ (1 \in ℝ^{+} \land \frac{x}{n} \in ℝ^{+}) \to (1 \leq \frac{x}{n} \leftrightarrow \log 1 \leq \log (\frac{x}{n}))$
147	50 131 146	sylancr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to (1 \leq \frac{x}{n} \leftrightarrow \log 1 \leq \log (\frac{x}{n}))$
148	145 147	mpbid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to \log 1 \leq \log (\frac{x}{n})$
149	137 148	eqbrtrrid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to 0 \leq \log (\frac{x}{n})$
150		simp32	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to y \leq n$
151	133 130 129	lediv2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to (y \leq n \leftrightarrow \frac{x}{n} \leq \frac{x}{y})$
152	150 151	mpbid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to \frac{x}{n} \leq \frac{x}{y}$
153	131 134	logled	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to (\frac{x}{n} \leq \frac{x}{y} \leftrightarrow \log (\frac{x}{n}) \leq \log (\frac{x}{y}))$
154	152 153	mpbid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to \log (\frac{x}{n}) \leq \log (\frac{x}{y})$
155		leexp1a	$⊢ ((\log (\frac{x}{n}) \in ℝ \land \log (\frac{x}{y}) \in ℝ \land N \in ℕ_{0}) \land (0 \leq \log (\frac{x}{n}) \land \log (\frac{x}{n}) \leq \log (\frac{x}{y}))) \to {\log (\frac{x}{n})}^{N} \leq {\log (\frac{x}{y})}^{N}$
156	132 135 136 149 154 155	syl32anc	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land n \in ℝ^{+}) \land (1 \leq y \land y \leq n \land n \leq x)) \to {\log (\frac{x}{n})}^{N} \leq {\log (\frac{x}{y})}^{N}$
157		eqid	$⊢ (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) = (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}))$
158	96	3ad2antr1	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to \frac{x}{y} \in ℝ^{+}$
159	158	relogcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to \log (\frac{x}{y}) \in ℝ$
160		simpll	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to N \in ℕ_{0}$
161		rpcn	$⊢ y \in ℝ^{+} \to y \in ℂ$
162	161	adantl	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y \in ℝ^{+}) \to y \in ℂ$
163	162	3ad2antr1	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to y \in ℂ$
164	163	mulid2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to 1 y = y$
165		simpr3	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to y \leq x$
166	164 165	eqbrtrd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to 1 y \leq x$
167		1red	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to 1 \in ℝ$
168	94	rpred	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ$
169	168	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to x \in ℝ$
170		simpr1	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to y \in ℝ^{+}$
171	167 169 170	lemuldivd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to (1 y \leq x \leftrightarrow 1 \leq \frac{x}{y})$
172	166 171	mpbid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to 1 \leq \frac{x}{y}$
173		logleb	$⊢ (1 \in ℝ^{+} \land \frac{x}{y} \in ℝ^{+}) \to (1 \leq \frac{x}{y} \leftrightarrow \log 1 \leq \log (\frac{x}{y}))$
174	50 158 173	sylancr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to (1 \leq \frac{x}{y} \leftrightarrow \log 1 \leq \log (\frac{x}{y}))$
175	172 174	mpbid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to \log 1 \leq \log (\frac{x}{y})$
176	137 175	eqbrtrrid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to 0 \leq \log (\frac{x}{y})$
177	159 160 176	expge0d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land (y \in ℝ^{+} \land 1 \leq y \land y \leq x)) \to 0 \leq {\log (\frac{x}{y})}^{N}$
178	50	a1i	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in ℝ^{+}$
179		1le1	$⊢ 1 \leq 1$
180	179	a1i	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq 1$
181		simprr	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
182	168	leidd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to x \leq x$
183	79 80 82 83 87 88 105 107 109 124 127 128 156 157 177 178 94 180 181 182	dvfsumlem4	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (x) - (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (1)\| \leq ⦋ 1 / y ⦌ {\log (\frac{x}{y})}^{N}$
184		fzfid	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x⌋) \in Fin$
185	94 4 5	syl2an	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
186	185	relogcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
187		simpll	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to N \in ℕ_{0}$
188	186 187	reexpcld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{N} \in ℝ$
189	184 188	fsumrecl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} \in ℝ$
190	189	recnd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} \in ℂ$
191	94	rpcnd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℂ$
192	72 191	mulcld	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to N! x \in ℂ$
193	11	ad2antrl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \in ℝ$
194	193	recnd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \in ℂ$
195	194 114	expcld	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to {\log x}^{N} \in ℂ$
196		fzfid	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (0 \dots N) \in Fin$
197	193 20 21	syl2an	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (0 \dots N)) \to {\log x}^{k} \in ℝ$
198	20	adantl	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (0 \dots N)) \to k \in ℕ_{0}$
199	198	faccld	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (0 \dots N)) \to k! \in ℕ$
200	197 199	nndivred	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (0 \dots N)) \to \frac{{\log x}^{k}}{k!} \in ℝ$
201	200	recnd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (0 \dots N)) \to \frac{{\log x}^{k}}{k!} \in ℂ$
202	196 201	fsumcl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ$
203	72 202	mulcld	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ$
204	195 203	subcld	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to {\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ$
205	190 192 204	sub32d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - N! x - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})) = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})) - N! x$
206		eqidd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) = (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}))$
207		simpr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to y = x$
208	207	fveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to ⌊y⌋ = ⌊x⌋$
209	208	oveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to (1 \dots ⌊y⌋) = (1 \dots ⌊x⌋)$
210	209	sumeq1d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}$
211		oveq2	$⊢ y = x \to \frac{x}{y} = \frac{x}{x}$
212	65	ad2antrl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \in ℂ \land x \neq 0)$
213		divid	$⊢ (x \in ℂ \land x \neq 0) \to \frac{x}{x} = 1$
214	212 213	syl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{x}{x} = 1$
215	211 214	sylan9eqr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to \frac{x}{y} = 1$
216	215	adantr	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in (0 \dots N)) \to \frac{x}{y} = 1$
217	216	fveq2d	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in (0 \dots N)) \to \log (\frac{x}{y}) = \log 1$
218	217 137	eqtrdi	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in (0 \dots N)) \to \log (\frac{x}{y}) = 0$
219	218	oveq1d	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in (0 \dots N)) \to {\log (\frac{x}{y})}^{k} = 0^{k}$
220	219	oveq1d	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in (0 \dots N)) \to \frac{{\log (\frac{x}{y})}^{k}}{k!} = \frac{0^{k}}{k!}$
221	220	sumeq2dv	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = \sum_{k = 0}^{N} (\frac{0^{k}}{k!})$
222		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
223	114 222	eleqtrdi	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to N \in ℤ_{\geq 0}$
224		eluzfz1	$⊢ N \in ℤ_{\geq 0} \to 0 \in (0 \dots N)$
225	223 224	syl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \in (0 \dots N)$
226	225	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to 0 \in (0 \dots N)$
227	226	snssd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to \{0\} \subseteq (0 \dots N)$
228		elsni	$⊢ k \in \{0\} \to k = 0$
229	228	adantl	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in \{0\}) \to k = 0$
230		oveq2	$⊢ k = 0 \to 0^{k} = 0^{0}$
231		0exp0e1	$⊢ 0^{0} = 1$
232	230 231	eqtrdi	$⊢ k = 0 \to 0^{k} = 1$
233		fveq2	$⊢ k = 0 \to k! = 0!$
234		fac0	$⊢ 0! = 1$
235	233 234	eqtrdi	$⊢ k = 0 \to k! = 1$
236	232 235	oveq12d	$⊢ k = 0 \to \frac{0^{k}}{k!} = \frac{1}{1}$
237		1div1e1	$⊢ \frac{1}{1} = 1$
238	236 237	eqtrdi	$⊢ k = 0 \to \frac{0^{k}}{k!} = 1$
239	229 238	syl	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in \{0\}) \to \frac{0^{k}}{k!} = 1$
240		ax-1cn	$⊢ 1 \in ℂ$
241	239 240	eqeltrdi	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in \{0\}) \to \frac{0^{k}}{k!} \in ℂ$
242		eldifi	$⊢ k \in ((0 \dots N) ∖ \{0\}) \to k \in (0 \dots N)$
243	242	adantl	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to k \in (0 \dots N)$
244	243 20	syl	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to k \in ℕ_{0}$
245		eldifsni	$⊢ k \in ((0 \dots N) ∖ \{0\}) \to k \neq 0$
246	245	adantl	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to k \neq 0$
247		eldifsn	$⊢ k \in (ℕ_{0} ∖ \{0\}) \leftrightarrow (k \in ℕ_{0} \land k \neq 0)$
248	244 246 247	sylanbrc	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to k \in (ℕ_{0} ∖ \{0\})$
249		dfn2	$⊢ ℕ = ℕ_{0} ∖ \{0\}$
250	248 249	eleqtrrdi	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to k \in ℕ$
251	250	0expd	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to 0^{k} = 0$
252	251	oveq1d	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to \frac{0^{k}}{k!} = \frac{0}{k!}$
253	244	faccld	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to k! \in ℕ$
254	253	nncnd	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to k! \in ℂ$
255	253	nnne0d	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to k! \neq 0$
256	254 255	div0d	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to \frac{0}{k!} = 0$
257	252 256	eqtrd	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \land k \in ((0 \dots N) ∖ \{0\})) \to \frac{0^{k}}{k!} = 0$
258		fzfid	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to (0 \dots N) \in Fin$
259	227 241 257 258	fsumss	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to \sum_{k \in \{0\}} (\frac{0^{k}}{k!}) = \sum_{k = 0}^{N} (\frac{0^{k}}{k!})$
260	221 259	eqtr4d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = \sum_{k \in \{0\}} (\frac{0^{k}}{k!})$
261		0cn	$⊢ 0 \in ℂ$
262	238	sumsn	$⊢ (0 \in ℂ \land 1 \in ℂ) \to \sum_{k \in \{0\}} (\frac{0^{k}}{k!}) = 1$
263	261 240 262	mp2an	$⊢ \sum_{k \in \{0\}} (\frac{0^{k}}{k!}) = 1$
264	260 263	eqtrdi	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = 1$
265	207 264	oveq12d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = x \cdot 1$
266	191	mulid1d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to x \cdot 1 = x$
267	266	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to x \cdot 1 = x$
268	265 267	eqtrd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = x$
269	268	oveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = N! x$
270	210 269	oveq12d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = x) \to \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - N! x$
271		ovexd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - N! x \in V$
272	206 270 94 271	fvmptd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (x) = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - N! x$
273		simpr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to y = 1$
274	273	fveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to ⌊y⌋ = ⌊1⌋$
275		flid	$⊢ 1 \in ℤ \to ⌊1⌋ = 1$
276	81 275	ax-mp	$⊢ ⌊1⌋ = 1$
277	274 276	eqtrdi	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to ⌊y⌋ = 1$
278	277	oveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to (1 \dots ⌊y⌋) = (1 \dots 1)$
279	278	sumeq1d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} = \sum_{n = 1}^{1} {\log (\frac{x}{n})}^{N}$
280	191	div1d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{x}{1} = x$
281	280	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \frac{x}{1} = x$
282	281	fveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \log (\frac{x}{1}) = \log x$
283	282	oveq1d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to {\log (\frac{x}{1})}^{N} = {\log x}^{N}$
284	195	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to {\log x}^{N} \in ℂ$
285	283 284	eqeltrd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to {\log (\frac{x}{1})}^{N} \in ℂ$
286		oveq2	$⊢ n = 1 \to \frac{x}{n} = \frac{x}{1}$
287	286	fveq2d	$⊢ n = 1 \to \log (\frac{x}{n}) = \log (\frac{x}{1})$
288	287	oveq1d	$⊢ n = 1 \to {\log (\frac{x}{n})}^{N} = {\log (\frac{x}{1})}^{N}$
289	288	fsum1	$⊢ (1 \in ℤ \land {\log (\frac{x}{1})}^{N} \in ℂ) \to \sum_{n = 1}^{1} {\log (\frac{x}{n})}^{N} = {\log (\frac{x}{1})}^{N}$
290	81 285 289	sylancr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \sum_{n = 1}^{1} {\log (\frac{x}{n})}^{N} = {\log (\frac{x}{1})}^{N}$
291	279 290 283	3eqtrd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} = {\log x}^{N}$
292	273	oveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \frac{x}{y} = \frac{x}{1}$
293	292 281	eqtrd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \frac{x}{y} = x$
294	293	fveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \log (\frac{x}{y}) = \log x$
295	294	adantr	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \land k \in (0 \dots N)) \to \log (\frac{x}{y}) = \log x$
296	295	oveq1d	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \land k \in (0 \dots N)) \to {\log (\frac{x}{y})}^{k} = {\log x}^{k}$
297	296	oveq1d	$⊢ (((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \land k \in (0 \dots N)) \to \frac{{\log (\frac{x}{y})}^{k}}{k!} = \frac{{\log x}^{k}}{k!}$
298	297	sumeq2dv	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})$
299	273 298	oveq12d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = 1 \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})$
300	202	adantr	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ$
301	300	mulid2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to 1 \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) = \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})$
302	299 301	eqtrd	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})$
303	302	oveq2d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})$
304	291 303	oveq12d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!}) = {\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})$
305		ovexd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to {\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in V$
306	206 304 178 305	fvmptd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (1) = {\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})$
307	272 306	oveq12d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (x) - (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (1) = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - N! x - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))$
308	70 72 191	subdird	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to ((\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!) x = (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) x - N! x$
309	64	adantrr	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})) \in ℂ$
310	212	simprd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to x \neq 0$
311	309 191 310	divcan1d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) x = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))$
312	311	oveq1d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) x - N! x = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})) - N! x$
313	308 312	eqtrd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to ((\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!) x = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})) - N! x$
314	205 307 313	3eqtr4d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (x) - (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (1) = ((\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!) x$
315	314	fveq2d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (x) - (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (1)\| = \|((\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!) x\|$
316	73 191	absmuld	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|((\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!) x\| = \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| \|x\|$
317		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
318	317	ad2antrl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \in ℝ \land 0 \leq x)$
319		absid	$⊢ (x \in ℝ \land 0 \leq x) \to \|x\| = x$
320	318 319	syl	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|x\| = x$
321	320	oveq2d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| \|x\| = \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| x$
322	315 316 321	3eqtrd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (x) - (y \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊y⌋} {\log (\frac{x}{n})}^{N} - N! y \sum_{k = 0}^{N} (\frac{{\log (\frac{x}{y})}^{k}}{k!})) (1)\| = \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| x$
323		1cnd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in ℂ$
324	294	oveq1d	$⊢ ((N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \land y = 1) \to {\log (\frac{x}{y})}^{N} = {\log x}^{N}$
325	323 324	csbied	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to ⦋ 1 / y ⦌ {\log (\frac{x}{y})}^{N} = {\log x}^{N}$
326	183 322 325	3brtr3d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| x \leq {\log x}^{N}$
327	14	adantrr	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to {\log x}^{N} \in ℝ$
328	74 327 94	lemuldivd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (\|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| x \leq {\log x}^{N} \leftrightarrow \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| \leq \frac{{\log x}^{N}}{x})$
329	326 328	mpbid	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| \leq \frac{{\log x}^{N}}{x}$
330	75	leabsd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{{\log x}^{N}}{x} \leq \|\frac{{\log x}^{N}}{x}\|$
331	74 75 77 329 330	letrd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| \leq \|\frac{{\log x}^{N}}{x}\|$
332	57	adantrr	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{{\log x}^{N}}{x} \in ℂ$
333	332	subid1d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to (\frac{{\log x}^{N}}{x}) - 0 = \frac{{\log x}^{N}}{x}$
334	333	fveq2d	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{{\log x}^{N}}{x}) - 0\| = \|\frac{{\log x}^{N}}{x}\|$
335	331 334	breqtrrd	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) - N!\| \leq \|(\frac{{\log x}^{N}}{x}) - 0\|$
336	33 34 54 57 69 335	rlimsqzlem	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) \underset{ℝ}{⇝} N!$
337		divsubdir	$⊢ ({\log x}^{N} \in ℂ \land N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} = (\frac{{\log x}^{N}}{x}) - (\frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})$
338	59 62 66 337	syl3anc	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} = (\frac{{\log x}^{N}}{x}) - (\frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})$
339	338	mpteq2dva	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) = (x \in ℝ^{+} ⟼ (\frac{{\log x}^{N}}{x}) - (\frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}))$
340		rerpdivcl	$⊢ (N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℝ \land x \in ℝ^{+}) \to \frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} \in ℝ$
341	27 340	sylancom	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} \in ℝ$
342		divass	$⊢ (N! \in ℂ \land \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} = N! (\frac{\sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})$
343	60 61 66 342	syl3anc	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} = N! (\frac{\sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})$
344	25	recnd	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to \frac{{\log x}^{k}}{k!} \in ℂ$
345	18 67 344 68	fsumdivc	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{\sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} = \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{k!}}{x})$
346	22	recnd	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to {\log x}^{k} \in ℂ$
347	24	nnrpd	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to k! \in ℝ^{+}$
348	347	rpcnne0d	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to (k! \in ℂ \land k! \neq 0)$
349	66	adantr	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to (x \in ℂ \land x \neq 0)$
350		divdiv32	$⊢ ({\log x}^{k} \in ℂ \land (k! \in ℂ \land k! \neq 0) \land (x \in ℂ \land x \neq 0)) \to \frac{\frac{{\log x}^{k}}{k!}}{x} = \frac{\frac{{\log x}^{k}}{x}}{k!}$
351	346 348 349 350	syl3anc	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to \frac{\frac{{\log x}^{k}}{k!}}{x} = \frac{\frac{{\log x}^{k}}{x}}{k!}$
352	351	sumeq2dv	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{k!}}{x}) = \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!})$
353	345 352	eqtrd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{\sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} = \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!})$
354	353	oveq2d	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to N! (\frac{\sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) = N! \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!})$
355	343 354	eqtrd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} = N! \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!})$
356	355	mpteq2dva	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) = (x \in ℝ^{+} ⟼ N! \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!}))$
357	2	adantr	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to x \in ℝ^{+}$
358	22 357	rerpdivcld	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to \frac{{\log x}^{k}}{x} \in ℝ$
359	358 24	nndivred	$⊢ ((N \in ℕ_{0} \land x \in ℝ^{+}) \land k \in (0 \dots N)) \to \frac{\frac{{\log x}^{k}}{x}}{k!} \in ℝ$
360	18 359	fsumrecl	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!}) \in ℝ$
361		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
362		rlimconst	$⊢ (ℝ^{+} \subseteq ℝ \land N! \in ℂ) \to (x \in ℝ^{+} ⟼ N!) \underset{ℝ}{⇝} N!$
363	361 34 362	sylancr	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ N!) \underset{ℝ}{⇝} N!$
364	361	a1i	$⊢ N \in ℕ_{0} \to ℝ^{+} \subseteq ℝ$
365		fzfid	$⊢ N \in ℕ_{0} \to (0 \dots N) \in Fin$
366	359	anasss	$⊢ (N \in ℕ_{0} \land (x \in ℝ^{+} \land k \in (0 \dots N))) \to \frac{\frac{{\log x}^{k}}{x}}{k!} \in ℝ$
367	358	an32s	$⊢ ((N \in ℕ_{0} \land k \in (0 \dots N)) \land x \in ℝ^{+}) \to \frac{{\log x}^{k}}{x} \in ℝ$
368	20	adantl	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to k \in ℕ_{0}$
369	368	faccld	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to k! \in ℕ$
370	369	nnred	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to k! \in ℝ$
371	370	adantr	$⊢ ((N \in ℕ_{0} \land k \in (0 \dots N)) \land x \in ℝ^{+}) \to k! \in ℝ$
372	368 53	syl	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{k}}{x}) \underset{ℝ}{⇝} 0$
373	369	nncnd	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to k! \in ℂ$
374		rlimconst	$⊢ (ℝ^{+} \subseteq ℝ \land k! \in ℂ) \to (x \in ℝ^{+} ⟼ k!) \underset{ℝ}{⇝} k!$
375	361 373 374	sylancr	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to (x \in ℝ^{+} ⟼ k!) \underset{ℝ}{⇝} k!$
376	369	nnne0d	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to k! \neq 0$
377	376	adantr	$⊢ ((N \in ℕ_{0} \land k \in (0 \dots N)) \land x \in ℝ^{+}) \to k! \neq 0$
378	367 371 372 375 376 377	rlimdiv	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to (x \in ℝ^{+} ⟼ \frac{\frac{{\log x}^{k}}{x}}{k!}) \underset{ℝ}{⇝} (\frac{0}{k!})$
379	373 376	div0d	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to \frac{0}{k!} = 0$
380	378 379	breqtrd	$⊢ (N \in ℕ_{0} \land k \in (0 \dots N)) \to (x \in ℝ^{+} ⟼ \frac{\frac{{\log x}^{k}}{x}}{k!}) \underset{ℝ}{⇝} 0$
381	364 365 366 380	fsumrlim	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!})) \underset{ℝ}{⇝} \sum_{k = 0}^{N} 0$
382		fzfi	$⊢ (0 \dots N) \in Fin$
383	382	olci	$⊢ ((0 \dots N) \subseteq ℤ_{\geq 0} \lor (0 \dots N) \in Fin)$
384		sumz	$⊢ ((0 \dots N) \subseteq ℤ_{\geq 0} \lor (0 \dots N) \in Fin) \to \sum_{k = 0}^{N} 0 = 0$
385	383 384	ax-mp	$⊢ \sum_{k = 0}^{N} 0 = 0$
386	381 385	breqtrdi	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!})) \underset{ℝ}{⇝} 0$
387	17 360 363 386	rlimmul	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ N! \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!})) \underset{ℝ}{⇝} N! \cdot 0$
388	34	mul01d	$⊢ N \in ℕ_{0} \to N! \cdot 0 = 0$
389	387 388	breqtrd	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ N! \sum_{k = 0}^{N} (\frac{\frac{{\log x}^{k}}{x}}{k!})) \underset{ℝ}{⇝} 0$
390	356 389	eqbrtrd	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) \underset{ℝ}{⇝} 0$
391	56 341 54 390	rlimsub	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ (\frac{{\log x}^{N}}{x}) - (\frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})) \underset{ℝ}{⇝} (0 - 0)$
392		0m0e0	$⊢ 0 - 0 = 0$
393	391 392	breqtrdi	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ (\frac{{\log x}^{N}}{x}) - (\frac{N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})) \underset{ℝ}{⇝} 0$
394	339 393	eqbrtrd	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) \underset{ℝ}{⇝} 0$
395	30 32 336 394	rlimadd	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) + (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})) \underset{ℝ}{⇝} (N! + 0)$
396		divsubdir	$⊢ (\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} \in ℂ \land {\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}) \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x}) - (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})$
397	58 63 66 396	syl3anc	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x}) - (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})$
398	397	oveq1d	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) + (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) = (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x}) - (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) + (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})$
399	10 2	rerpdivcld	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x} \in ℝ$
400	399	recnd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x} \in ℂ$
401	32	recnd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to \frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x} \in ℂ$
402	400 401	npcand	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x}) - (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) + (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) = \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x}$
403	398 402	eqtrd	$⊢ (N \in ℕ_{0} \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) + (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x}) = \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x}$
404	403	mpteq2dva	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N} - ({\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!}))}{x}) + (\frac{{\log x}^{N} - N! \sum_{k = 0}^{N} (\frac{{\log x}^{k}}{k!})}{x})) = (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x})$
405	34	addid1d	$⊢ N \in ℕ_{0} \to N! + 0 = N!$
406	395 404 405	3brtr3d	$⊢ N \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{N}}{x}) \underset{ℝ}{⇝} N!$

Metamath Proof Explorer

Theorem logexprlim

Proof