Theorem logexprlim 25961

Description: The sum Σ𝑛 ≤ 𝑥, log↑𝑁(𝑥 / 𝑛) has the asymptotic expansion (𝑁!)𝑥 + 𝑜(𝑥). (More precisely, the omitted term has order 𝑂(log↑𝑁(𝑥) / 𝑥).) (Contributed by Mario Carneiro, 22-May-2016.)

Assertion

Ref	Expression
logexprlim	⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁))

Distinct variable group:   𝑥,𝑛,𝑁

Proof of Theorem logexprlim

Dummy variables 𝑘 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 13433	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
2		simpr 488	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
3		elfznn 13028	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
4	3	nnrpd 12513	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
5		rpdivcl 12498	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
6	2, 4, 5	syl2an 599	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
7	6	relogcld 25366	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
8		simpll 767	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
9	7, 8	reexpcld 13620	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
10	1, 9	fsumrecl 15185	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
11		relogcl 25319	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
12		id 22	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0)
13		reexpcl 13539	. . . . . . 7 ⊢ (((log‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℕ0) → ((log‘𝑥)↑𝑁) ∈ ℝ)
14	11, 12, 13	syl2anr 600	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℝ)
15		faccl 13736	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
16	15	adantr 484	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
17	16	nnred 11732	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
18		fzfid 13433	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (0...𝑁) ∈ Fin)
19	11	adantl 485	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
20		elfznn0 13092	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
21		reexpcl 13539	. . . . . . . . . 10 ⊢ (((log‘𝑥) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑘) ∈ ℝ)
22	19, 20, 21	syl2an 599	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
23	20	adantl 485	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
24	23	faccld 13737	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
25	22, 24	nndivred 11771	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
26	18, 25	fsumrecl 15185	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
27	17, 26	remulcld 10750	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ)
28	14, 27	resubcld 11147	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ)
29	10, 28	resubcld 11147	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℝ)
30	29, 2	rerpdivcld 12546	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℝ)
31		rerpdivcl 12503	. . . 4 ⊢ (((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
32	28, 31	sylancom 591	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
33		1red 10721	. . . 4 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℝ)
34	15	nncnd 11733	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℂ)
35		simpl 486	. . . . . . . . 9 ⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → 𝑘 = 𝑁)
36	35	oveq2d 7187	. . . . . . . 8 ⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑘) = ((log‘𝑥)↑𝑁))
37	36	oveq1d 7186	. . . . . . 7 ⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) = (((log‘𝑥)↑𝑁) / 𝑥))
38	37	mpteq2dva 5126	. . . . . 6 ⊢ (𝑘 = 𝑁 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)))
39	38	breq1d 5041	. . . . 5 ⊢ (𝑘 = 𝑁 → ((𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0 ↔ (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0))
40	11	recnd 10748	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℂ)
41		id 22	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℕ0)
42		cxpexp 25411	. . . . . . . . 9 ⊢ (((log‘𝑥) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
43	40, 41, 42	syl2anr 600	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
44		rpcn 12483	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ)
45	44	adantl 485	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
46	45	cxp1d 25449	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐1) = 𝑥)
47	43, 46	oveq12d 7189	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)) = (((log‘𝑥)↑𝑘) / 𝑥))
48	47	mpteq2dva 5126	. . . . . 6 ⊢ (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)))
49		nn0cn 11987	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
50		1rp 12477	. . . . . . 7 ⊢ 1 ∈ ℝ+
51		cxploglim2 25716	. . . . . . 7 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℝ+) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) ⇝𝑟 0)
52	49, 50, 51	sylancl 589	. . . . . 6 ⊢ (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) ⇝𝑟 0)
53	48, 52	eqbrtrrd 5055	. . . . 5 ⊢ (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
54	39, 53	vtoclga 3479	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0)
55		rerpdivcl 12503	. . . . . 6 ⊢ ((((log‘𝑥)↑𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
56	14, 55	sylancom 591	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
57	56	recnd 10748	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
58	10	recnd 10748	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
59	14	recnd 10748	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℂ)
60	34	adantr 484	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
61	26	recnd 10748	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
62	60, 61	mulcld 10740	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
63	59, 62	subcld 11076	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
64	58, 63	subcld 11076	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
65		rpcnne0 12491	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
66	65	adantl 485	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
67	66	simpld 498	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
68	66	simprd 499	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
69	64, 67, 68	divcld 11495	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
70	69	adantrr 717	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
71	15	adantr 484	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℕ)
72	71	nncnd 11733	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℂ)
73	70, 72	subcld 11076	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) ∈ ℂ)
74	73	abscld 14887	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ∈ ℝ)
75	56	adantrr 717	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
76	75	recnd 10748	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
77	76	abscld 14887	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥)↑𝑁) / 𝑥)) ∈ ℝ)
78		ioorp 12900	. . . . . . . . . 10 ⊢ (0(,)+∞) = ℝ+
79	78	eqcomi 2747	. . . . . . . . 9 ⊢ ℝ+ = (0(,)+∞)
80		nnuz 12364	. . . . . . . . 9 ⊢ ℕ = (ℤ≥‘1)
81		1z 12094	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
82	81	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℤ)
83		1red 10721	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ)
84		1re 10720	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
85		1nn0 11993	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
86	84, 85	nn0addge1i 12025	. . . . . . . . . 10 ⊢ 1 ≤ (1 + 1)
87	86	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ (1 + 1))
88		0red 10723	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ)
89	71	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
90	89	nnred 11732	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
91		rpre 12481	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
92	91	adantl 485	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
93		fzfid 13433	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (0...𝑁) ∈ Fin)
94		simprl 771	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
95		rpdivcl 12498	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
96	94, 95	sylan 583	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
97	96	relogcld 25366	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
98		reexpcl 13539	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
99	97, 20, 98	syl2an 599	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
100	20	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
101	100	faccld 13737	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
102	99, 101	nndivred 11771	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
103	93, 102	fsumrecl 15185	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
104	92, 103	remulcld 10750	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℝ)
105	90, 104	remulcld 10750	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) ∈ ℝ)
106		simpll 767	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑁 ∈ ℕ0)
107	97, 106	reexpcld 13620	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
108		nnrp 12484	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
109	108, 107	sylan2 596	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℕ) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
110		reelprrecn 10708	. . . . . . . . . . . 12 ⊢ ℝ ∈ {ℝ, ℂ}
111	110	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ℝ ∈ {ℝ, ℂ})
112	104	recnd 10748	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℂ)
113	107, 89	nndivred 11771	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)) ∈ ℝ)
114		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
115		advlogexp 25398	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
116	94, 114, 115	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
117	111, 112, 113, 116, 72	dvmptcmul 24716	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))))
118	107	recnd 10748	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℂ)
119	72	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
120	71	nnne0d 11767	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ≠ 0)
121	120	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ≠ 0)
122	118, 119, 121	divcan2d 11497	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))) = ((log‘(𝑥 / 𝑦))↑𝑁))
123	122	mpteq2dva 5126	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
124	117, 123	eqtrd 2773	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
125		oveq2 7179	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (𝑥 / 𝑦) = (𝑥 / 𝑛))
126	125	fveq2d 6679	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (log‘(𝑥 / 𝑦)) = (log‘(𝑥 / 𝑛)))
127	126	oveq1d 7186	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘(𝑥 / 𝑛))↑𝑁))
128	94	rpxrd 12516	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ*)
129		simp1rl 1239	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
130		simp2r 1201	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℝ+)
131	129, 130	rpdivcld 12532	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ∈ ℝ+)
132	131	relogcld 25366	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
133		simp2l 1200	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ∈ ℝ+)
134	129, 133	rpdivcld 12532	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
135	134	relogcld 25366	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
136		simp1l 1198	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
137		log1 25329	. . . . . . . . . . 11 ⊢ (log‘1) = 0
138	130	rpcnd 12517	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℂ)
139	138	mulid2d 10738	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) = 𝑛)
140		simp33 1212	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥)
141	139, 140	eqbrtrd 5053	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) ≤ 𝑥)
142		1red 10721	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ∈ ℝ)
143	129	rpred 12515	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ)
144	142, 143, 130	lemuldivd 12564	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
145	141, 144	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑛))
146		logleb 25346	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
147	50, 131, 146	sylancr 590	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
148	145, 147	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
149	137, 148	eqbrtrrid 5067	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑛)))
150		simp32 1211	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ≤ 𝑛)
151	133, 130, 129	lediv2d 12539	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑦 ≤ 𝑛 ↔ (𝑥 / 𝑛) ≤ (𝑥 / 𝑦)))
152	150, 151	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ≤ (𝑥 / 𝑦))
153	131, 134	logled 25370	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((𝑥 / 𝑛) ≤ (𝑥 / 𝑦) ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦))))
154	152, 153	mpbid 235	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))
155		leexp1a 13632	. . . . . . . . . 10 ⊢ ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ (log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ (log‘(𝑥 / 𝑛)) ∧ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
156	132, 135, 136, 149, 154, 155	syl32anc 1379	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
157		eqid 2738	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))
158	96	3ad2antr1 1189	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
159	158	relogcld 25366	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
160		simpll 767	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
161		rpcn 12483	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
162	161	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℂ)
163	162	3ad2antr1 1189	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℂ)
164	163	mulid2d 10738	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) = 𝑦)
165		simpr3 1197	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ≤ 𝑥)
166	164, 165	eqbrtrd 5053	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) ≤ 𝑥)
167		1red 10721	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ∈ ℝ)
168	94	rpred 12515	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
169	168	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑥 ∈ ℝ)
170		simpr1 1195	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℝ+)
171	167, 169, 170	lemuldivd 12564	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → ((1 · 𝑦) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑦)))
172	166, 171	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑦))
173		logleb 25346	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ+ ∧ (𝑥 / 𝑦) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
174	50, 158, 173	sylancr 590	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
175	172, 174	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑦)))
176	137, 175	eqbrtrrid 5067	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑦)))
177	159, 160, 176	expge0d 13621	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
178	50	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ+)
179		1le1 11347	. . . . . . . . . 10 ⊢ 1 ≤ 1
180	179	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 1)
181		simprr 773	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
182	168	leidd 11285	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≤ 𝑥)
183	79, 80, 82, 83, 87, 88, 105, 107, 109, 124, 127, 128, 156, 157, 177, 178, 94, 180, 181, 182	dvfsumlem4 24781	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) ≤ ⦋1 / 𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁))
184		fzfid 13433	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
185	94, 4, 5	syl2an 599	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
186	185	relogcld 25366	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
187		simpll 767	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
188	186, 187	reexpcld 13620	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
189	184, 188	fsumrecl 15185	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
190	189	recnd 10748	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
191	94	rpcnd 12517	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ)
192	72, 191	mulcld 10740	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · 𝑥) ∈ ℂ)
193	11	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
194	193	recnd 10748	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ)
195	194, 114	expcld 13603	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℂ)
196		fzfid 13433	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (0...𝑁) ∈ Fin)
197	193, 20, 21	syl2an 599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
198	20	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
199	198	faccld 13737	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
200	197, 199	nndivred 11771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
201	200	recnd 10748	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
202	196, 201	fsumcl 15184	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
203	72, 202	mulcld 10740	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
204	195, 203	subcld 11076	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
205	190, 192, 204	sub32d 11108	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
206		eqidd 2739	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))))
207		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
208	207	fveq2d 6679	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (⌊‘𝑦) = (⌊‘𝑥))
209	208	oveq2d 7187	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (1...(⌊‘𝑦)) = (1...(⌊‘𝑥)))
210	209	sumeq1d 15152	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁))
211		oveq2 7179	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (𝑥 / 𝑦) = (𝑥 / 𝑥))
212	65	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
213		divid 11406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
214	212, 213	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 𝑥) = 1)
215	211, 214	sylan9eqr 2795	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 / 𝑦) = 1)
216	215	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 / 𝑦) = 1)
217	216	fveq2d 6679	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘1))
218	217, 137	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = 0)
219	218	oveq1d 7186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = (0↑𝑘))
220	219	oveq1d 7186	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = ((0↑𝑘) / (!‘𝑘)))
221	220	sumeq2dv 15154	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
222		nn0uz 12363	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ0 = (ℤ≥‘0)
223	114, 222	eleqtrdi 2843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ (ℤ≥‘0))
224		eluzfz1 13006	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ≥‘0) → 0 ∈ (0...𝑁))
225	223, 224	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ (0...𝑁))
226	225	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 0 ∈ (0...𝑁))
227	226	snssd 4698	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → {0} ⊆ (0...𝑁))
228		elsni 4534	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ {0} → 𝑘 = 0)
229	228	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → 𝑘 = 0)
230		oveq2 7179	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0))
231		0exp0e1 13527	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0↑0) = 1
232	230, 231	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 0 → (0↑𝑘) = 1)
233		fveq2 6675	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
234		fac0 13729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (!‘0) = 1
235	233, 234	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
236	232, 235	oveq12d 7189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = (1 / 1))
237		1div1e1 11409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 / 1) = 1
238	236, 237	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = 1)
239	229, 238	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) = 1)
240		ax-1cn 10674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
241	239, 240	eqeltrdi 2841	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) ∈ ℂ)
242		eldifi 4018	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ∈ (0...𝑁))
243	242	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (0...𝑁))
244	243, 20	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ0)
245		eldifsni 4679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ≠ 0)
246	245	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ≠ 0)
247		eldifsn 4676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (ℕ0 ∖ {0}) ↔ (𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0))
248	244, 246, 247	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (ℕ0 ∖ {0}))
249		dfn2 11990	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ = (ℕ0 ∖ {0})
250	248, 249	eleqtrrdi 2844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ)
251	250	0expd 13596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0↑𝑘) = 0)
252	251	oveq1d 7186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = (0 / (!‘𝑘)))
253	244	faccld 13737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℕ)
254	253	nncnd 11733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℂ)
255	253	nnne0d 11767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ≠ 0)
256	254, 255	div0d 11494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0 / (!‘𝑘)) = 0)
257	252, 256	eqtrd 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = 0)
258		fzfid 13433	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (0...𝑁) ∈ Fin)
259	227, 241, 257, 258	fsumss 15176	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
260	221, 259	eqtr4d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)))
261		0cn 10712	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℂ
262	238	sumsn 15195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1)
263	261, 240, 262	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1
264	260, 263	eqtrdi 2789	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = 1)
265	207, 264	oveq12d 7189	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (𝑥 · 1))
266	191	mulid1d 10737	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥)
267	266	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 · 1) = 𝑥)
268	265, 267	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = 𝑥)
269	268	oveq2d 7187	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · 𝑥))
270	210, 269	oveq12d 7189	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
271		ovexd 7206	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V)
272	206, 270, 94, 271	fvmptd 6783	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
273		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → 𝑦 = 1)
274	273	fveq2d 6679	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = (⌊‘1))
275		flid 13270	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℤ → (⌊‘1) = 1)
276	81, 275	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (⌊‘1) = 1
277	274, 276	eqtrdi 2789	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = 1)
278	277	oveq2d 7187	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1...(⌊‘𝑦)) = (1...1))
279	278	sumeq1d 15152	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁))
280	191	div1d 11487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 1) = 𝑥)
281	280	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 1) = 𝑥)
282	281	fveq2d 6679	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 1)) = (log‘𝑥))
283	282	oveq1d 7186	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) = ((log‘𝑥)↑𝑁))
284	195	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘𝑥)↑𝑁) ∈ ℂ)
285	283, 284	eqeltrd 2833	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ)
286		oveq2 7179	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑥 / 𝑛) = (𝑥 / 1))
287	286	fveq2d 6679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (log‘(𝑥 / 𝑛)) = (log‘(𝑥 / 1)))
288	287	oveq1d 7186	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
289	288	fsum1 15196	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℤ ∧ ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
290	81, 285, 289	sylancr 590	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
291	279, 290, 283	3eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘𝑥)↑𝑁))
292	273	oveq2d 7187	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = (𝑥 / 1))
293	292, 281	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = 𝑥)
294	293	fveq2d 6679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
295	294	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
296	295	oveq1d 7186	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = ((log‘𝑥)↑𝑘))
297	296	oveq1d 7186	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = (((log‘𝑥)↑𝑘) / (!‘𝑘)))
298	297	sumeq2dv 15154	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
299	273, 298	oveq12d 7189	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
300	202	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
301	300	mulid2d 10738	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
302	299, 301	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
303	302	oveq2d 7187	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
304	291, 303	oveq12d 7189	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
305		ovexd 7206	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V)
306	206, 304, 178, 305	fvmptd 6783	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
307	272, 306	oveq12d 7189	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
308	70, 72, 191	subdird 11176	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)))
309	64	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
310	212	simprd 499	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0)
311	309, 191, 310	divcan1d 11496	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
312	311	oveq1d 7186	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
313	308, 312	eqtrd 2773	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
314	205, 307, 313	3eqtr4d 2783	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥))
315	314	fveq2d 6679	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)))
316	73, 191	absmuld 14905	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)))
317		rprege0 12488	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
318	317	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
319		absid 14747	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
320	318, 319	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥)
321	320	oveq2d 7187	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
322	315, 316, 321	3eqtrd 2777	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
323		1cnd 10715	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ)
324	294	oveq1d 7186	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
325	323, 324	csbied 3827	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ⦋1 / 𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
326	183, 322, 325	3brtr3d 5062	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁))
327	14	adantrr 717	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℝ)
328	74, 327, 94	lemuldivd 12564	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁) ↔ (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥)))
329	326, 328	mpbid 235	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥))
330	75	leabsd 14865	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
331	74, 75, 77, 329, 330	letrd 10876	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
332	57	adantrr 717	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
333	332	subid1d 11065	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥)↑𝑁) / 𝑥) − 0) = (((log‘𝑥)↑𝑁) / 𝑥))
334	333	fveq2d 6679	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)) = (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
335	331, 334	breqtrrd 5059	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)))
336	33, 34, 54, 57, 69, 335	rlimsqzlem 15099	. . 3 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥)) ⇝𝑟 (!‘𝑁))
337		divsubdir 11413	. . . . . 6 ⊢ ((((log‘𝑥)↑𝑁) ∈ ℂ ∧ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
338	59, 62, 66, 337	syl3anc 1372	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
339	338	mpteq2dva 5126	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))))
340		rerpdivcl 12503	. . . . . . 7 ⊢ ((((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
341	27, 340	sylancom 591	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
342		divass 11395	. . . . . . . . . 10 ⊢ (((!‘𝑁) ∈ ℂ ∧ Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
343	60, 61, 66, 342	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
344	25	recnd 10748	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
345	18, 67, 344, 68	fsumdivc 15235	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))
346	22	recnd 10748	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℂ)
347	24	nnrpd 12513	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ+)
348	347	rpcnne0d 12524	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0))
349	66	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
350		divdiv32 11427	. . . . . . . . . . . . 13 ⊢ ((((log‘𝑥)↑𝑘) ∈ ℂ ∧ ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
351	346, 348, 349, 350	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
352	351	sumeq2dv 15154	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
353	345, 352	eqtrd 2773	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
354	353	oveq2d 7187	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
355	343, 354	eqtrd 2773	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
356	355	mpteq2dva 5126	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))))
357	2	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℝ+)
358	22, 357	rerpdivcld 12546	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
359	358, 24	nndivred 11771	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
360	18, 359	fsumrecl 15185	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
361		rpssre 12480	. . . . . . . . . 10 ⊢ ℝ+ ⊆ ℝ
362		rlimconst 14992	. . . . . . . . . 10 ⊢ ((ℝ+ ⊆ ℝ ∧ (!‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
363	361, 34, 362	sylancr 590	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
364	361	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → ℝ+ ⊆ ℝ)
365		fzfid 13433	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (0...𝑁) ∈ Fin)
366	359	anasss 470	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 𝑘 ∈ (0...𝑁))) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
367	358	an32s 652	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
368	20	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
369	368	faccld 13737	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
370	369	nnred 11732	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ)
371	370	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ∈ ℝ)
372	368, 53	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
373	369	nncnd 11733	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℂ)
374		rlimconst 14992	. . . . . . . . . . . . . 14 ⊢ ((ℝ+ ⊆ ℝ ∧ (!‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
375	361, 373, 374	sylancr 590	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
376	369	nnne0d 11767	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0)
377	376	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ≠ 0)
378	367, 371, 372, 375, 376, 377	rlimdiv 15096	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 (0 / (!‘𝑘)))
379	373, 376	div0d 11494	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (0 / (!‘𝑘)) = 0)
380	378, 379	breqtrd 5057	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
381	364, 365, 366, 380	fsumrlim 15260	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 Σ𝑘 ∈ (0...𝑁)0)
382		fzfi 13432	. . . . . . . . . . . 12 ⊢ (0...𝑁) ∈ Fin
383	382	olci 865	. . . . . . . . . . 11 ⊢ ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin)
384		sumz 15173	. . . . . . . . . . 11 ⊢ (((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin) → Σ𝑘 ∈ (0...𝑁)0 = 0)
385	383, 384	ax-mp 5	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...𝑁)0 = 0
386	381, 385	breqtrdi 5072	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
387	17, 360, 363, 386	rlimmul 15094	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 ((!‘𝑁) · 0))
388	34	mul01d 10918	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → ((!‘𝑁) · 0) = 0)
389	387, 388	breqtrd 5057	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 0)
390	356, 389	eqbrtrd 5053	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) ⇝𝑟 0)
391	56, 341, 54, 390	rlimsub 15093	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 (0 − 0))
392		0m0e0 11837	. . . . 5 ⊢ (0 − 0) = 0
393	391, 392	breqtrdi 5072	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 0)
394	339, 393	eqbrtrd 5053	. . 3 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) ⇝𝑟 0)
395	30, 32, 336, 394	rlimadd 15091	. 2 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) ⇝𝑟 ((!‘𝑁) + 0))
396		divsubdir 11413	. . . . . 6 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ ∧ (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
397	58, 63, 66, 396	syl3anc 1372	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
398	397	oveq1d 7186	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
399	10, 2	rerpdivcld 12546	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℝ)
400	399	recnd 10748	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℂ)
401	32	recnd 10748	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℂ)
402	400, 401	npcand 11080	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
403	398, 402	eqtrd 2773	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
404	403	mpteq2dva 5126	. 2 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)))
405	34	addid1d 10919	. 2 ⊢ (𝑁 ∈ ℕ0 → ((!‘𝑁) + 0) = (!‘𝑁))
406	395, 404, 405	3brtr3d 5062	1 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2113   ≠ wne 2934  Vcvv 3398  ⦋csb 3791   ∖ cdif 3841   ⊆ wss 3844  {csn 4517  {cpr 4519   class class class wbr 5031   ↦ cmpt 5111  ‘cfv 6340  (class class class)co 7171  Fincfn 8556  ℂcc 10614  ℝcr 10615  0cc0 10616  1c1 10617   + caddc 10619   · cmul 10621  +∞cpnf 10751   ≤ cle 10755   − cmin 10949   / cdiv 11376  ℕcn 11717  ℕ₀cn0 11977  ℤcz 12063  ℤ_≥cuz 12325  ℝ⁺crp 12473  (,)cioo 12822  ...cfz 12982  ⌊cfl 13252  ↑cexp 13522  !cfa 13726  abscabs 14684   ⇝_𝑟 crli 14933  Σcsu 15136   D cdv 24615  logclog 25298  ↑_𝑐ccxp 25299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480  ax-inf2 9178  ax-cnex 10672  ax-resscn 10673  ax-1cn 10674  ax-icn 10675  ax-addcl 10676  ax-addrcl 10677  ax-mulcl 10678  ax-mulrcl 10679  ax-mulcom 10680  ax-addass 10681  ax-mulass 10682  ax-distr 10683  ax-i2m1 10684  ax-1ne0 10685  ax-1rid 10686  ax-rnegex 10687  ax-rrecex 10688  ax-cnre 10689  ax-pre-lttri 10690  ax-pre-lttrn 10691  ax-pre-ltadd 10692  ax-pre-mulgt0 10693  ax-pre-sup 10694  ax-addf 10695  ax-mulf 10696

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-se 5485  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7128  df-ov 7174  df-oprab 7175  df-mpo 7176  df-of 7426  df-om 7601  df-1st 7715  df-2nd 7716  df-supp 7858  df-wrecs 7977  df-recs 8038  df-rdg 8076  df-1o 8132  df-2o 8133  df-er 8321  df-map 8440  df-pm 8441  df-ixp 8509  df-en 8557  df-dom 8558  df-sdom 8559  df-fin 8560  df-fsupp 8908  df-fi 8949  df-sup 8980  df-inf 8981  df-oi 9048  df-card 9442  df-pnf 10756  df-mnf 10757  df-xr 10758  df-ltxr 10759  df-le 10760  df-sub 10951  df-neg 10952  df-div 11377  df-nn 11718  df-2 11780  df-3 11781  df-4 11782  df-5 11783  df-6 11784  df-7 11785  df-8 11786  df-9 11787  df-n0 11978  df-z 12064  df-dec 12181  df-uz 12326  df-q 12432  df-rp 12474  df-xneg 12591  df-xadd 12592  df-xmul 12593  df-ioo 12826  df-ioc 12827  df-ico 12828  df-icc 12829  df-fz 12983  df-fzo 13126  df-fl 13254  df-mod 13330  df-seq 13462  df-exp 13523  df-fac 13727  df-bc 13756  df-hash 13784  df-shft 14517  df-cj 14549  df-re 14550  df-im 14551  df-sqrt 14685  df-abs 14686  df-limsup 14919  df-clim 14936  df-rlim 14937  df-sum 15137  df-ef 15514  df-e 15515  df-sin 15516  df-cos 15517  df-pi 15519  df-struct 16589  df-ndx 16590  df-slot 16591  df-base 16593  df-sets 16594  df-ress 16595  df-plusg 16682  df-mulr 16683  df-starv 16684  df-sca 16685  df-vsca 16686  df-ip 16687  df-tset 16688  df-ple 16689  df-ds 16691  df-unif 16692  df-hom 16693  df-cco 16694  df-rest 16800  df-topn 16801  df-0g 16819  df-gsum 16820  df-topgen 16821  df-pt 16822  df-prds 16825  df-xrs 16879  df-qtop 16884  df-imas 16885  df-xps 16887  df-mre 16961  df-mrc 16962  df-acs 16964  df-mgm 17969  df-sgrp 18018  df-mnd 18029  df-submnd 18074  df-mulg 18344  df-cntz 18566  df-cmn 19027  df-psmet 20210  df-xmet 20211  df-met 20212  df-bl 20213  df-mopn 20214  df-fbas 20215  df-fg 20216  df-cnfld 20219  df-top 21646  df-topon 21663  df-topsp 21685  df-bases 21698  df-cld 21771  df-ntr 21772  df-cls 21773  df-nei 21850  df-lp 21888  df-perf 21889  df-cn 21979  df-cnp 21980  df-haus 22067  df-cmp 22139  df-tx 22314  df-hmeo 22507  df-fil 22598  df-fm 22690  df-flim 22691  df-flf 22692  df-xms 23074  df-ms 23075  df-tms 23076  df-cncf 23631  df-limc 24618  df-dv 24619  df-log 25300  df-cxp 25301

This theorem is referenced by:  logfacrlim2  25962  selberglem2  26282