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	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) ) ⇝𝑟 ( ! ‘ 𝑁 ) )

Proof

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