Theorem 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 {\mathbb{N}}_0\to \left(x\in {ℝ}^{+}⟼\frac{\sum _{n=1}^{⌊x⌋}{\log \left(\frac{x}{n}\right)}^N}{x}\right)\underset{ℝ}{⇝}N!$$

Proof

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