Theorem logexprlim 27152

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 13898	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
2		simpr 484	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
3		elfznn 13474	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
4	3	nnrpd 12953	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
5		rpdivcl 12938	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
6	2, 4, 5	syl2an 596	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
7	6	relogcld 26548	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
8		simpll 766	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
9	7, 8	reexpcld 14088	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
10	1, 9	fsumrecl 15659	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
11		relogcl 26500	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
12		id 22	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0)
13		reexpcl 14003	. . . . . . 7 ⊢ (((log‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℕ0) → ((log‘𝑥)↑𝑁) ∈ ℝ)
14	11, 12, 13	syl2anr 597	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℝ)
15		faccl 14208	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
16	15	adantr 480	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
17	16	nnred 12161	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
18		fzfid 13898	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (0...𝑁) ∈ Fin)
19	11	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
20		elfznn0 13541	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
21		reexpcl 14003	. . . . . . . . . 10 ⊢ (((log‘𝑥) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑘) ∈ ℝ)
22	19, 20, 21	syl2an 596	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
23	20	adantl 481	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
24	23	faccld 14209	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
25	22, 24	nndivred 12200	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
26	18, 25	fsumrecl 15659	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
27	17, 26	remulcld 11164	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ)
28	14, 27	resubcld 11566	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ)
29	10, 28	resubcld 11566	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℝ)
30	29, 2	rerpdivcld 12986	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℝ)
31		rerpdivcl 12943	. . . 4 ⊢ (((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
32	28, 31	sylancom 588	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
33		1red 11135	. . . 4 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℝ)
34	15	nncnd 12162	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℂ)
35		simpl 482	. . . . . . . . 9 ⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → 𝑘 = 𝑁)
36	35	oveq2d 7369	. . . . . . . 8 ⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑘) = ((log‘𝑥)↑𝑁))
37	36	oveq1d 7368	. . . . . . 7 ⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) = (((log‘𝑥)↑𝑁) / 𝑥))
38	37	mpteq2dva 5188	. . . . . 6 ⊢ (𝑘 = 𝑁 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)))
39	38	breq1d 5105	. . . . 5 ⊢ (𝑘 = 𝑁 → ((𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0 ↔ (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0))
40	11	recnd 11162	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℂ)
41		id 22	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℕ0)
42		cxpexp 26593	. . . . . . . . 9 ⊢ (((log‘𝑥) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
43	40, 41, 42	syl2anr 597	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
44		rpcn 12922	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ)
45	44	adantl 481	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
46	45	cxp1d 26631	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐1) = 𝑥)
47	43, 46	oveq12d 7371	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)) = (((log‘𝑥)↑𝑘) / 𝑥))
48	47	mpteq2dva 5188	. . . . . 6 ⊢ (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)))
49		nn0cn 12412	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
50		1rp 12915	. . . . . . 7 ⊢ 1 ∈ ℝ+
51		cxploglim2 26905	. . . . . . 7 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℝ+) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) ⇝𝑟 0)
52	49, 50, 51	sylancl 586	. . . . . 6 ⊢ (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) ⇝𝑟 0)
53	48, 52	eqbrtrrd 5119	. . . . 5 ⊢ (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
54	39, 53	vtoclga 3534	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0)
55		rerpdivcl 12943	. . . . . 6 ⊢ ((((log‘𝑥)↑𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
56	14, 55	sylancom 588	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
57	56	recnd 11162	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
58	10	recnd 11162	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
59	14	recnd 11162	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℂ)
60	34	adantr 480	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
61	26	recnd 11162	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
62	60, 61	mulcld 11154	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
63	59, 62	subcld 11493	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
64	58, 63	subcld 11493	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
65		rpcnne0 12930	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
66	65	adantl 481	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
67	66	simpld 494	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
68	66	simprd 495	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
69	64, 67, 68	divcld 11918	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
70	69	adantrr 717	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
71	15	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℕ)
72	71	nncnd 12162	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℂ)
73	70, 72	subcld 11493	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) ∈ ℂ)
74	73	abscld 15364	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ∈ ℝ)
75	56	adantrr 717	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
76	75	recnd 11162	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
77	76	abscld 15364	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥)↑𝑁) / 𝑥)) ∈ ℝ)
78		ioorp 13346	. . . . . . . . . 10 ⊢ (0(,)+∞) = ℝ+
79	78	eqcomi 2738	. . . . . . . . 9 ⊢ ℝ+ = (0(,)+∞)
80		nnuz 12796	. . . . . . . . 9 ⊢ ℕ = (ℤ≥‘1)
81		1z 12523	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
82	81	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℤ)
83		1red 11135	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ)
84		1re 11134	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
85		1nn0 12418	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
86	84, 85	nn0addge1i 12450	. . . . . . . . . 10 ⊢ 1 ≤ (1 + 1)
87	86	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ (1 + 1))
88		0red 11137	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ)
89	71	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
90	89	nnred 12161	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
91		rpre 12920	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
92	91	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
93		fzfid 13898	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (0...𝑁) ∈ Fin)
94		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
95		rpdivcl 12938	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
96	94, 95	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
97	96	relogcld 26548	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
98		reexpcl 14003	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
99	97, 20, 98	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
100	20	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
101	100	faccld 14209	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
102	99, 101	nndivred 12200	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
103	93, 102	fsumrecl 15659	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
104	92, 103	remulcld 11164	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℝ)
105	90, 104	remulcld 11164	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) ∈ ℝ)
106		simpll 766	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑁 ∈ ℕ0)
107	97, 106	reexpcld 14088	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
108		nnrp 12923	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
109	108, 107	sylan2 593	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℕ) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
110		reelprrecn 11120	. . . . . . . . . . . 12 ⊢ ℝ ∈ {ℝ, ℂ}
111	110	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ℝ ∈ {ℝ, ℂ})
112	104	recnd 11162	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℂ)
113	107, 89	nndivred 12200	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)) ∈ ℝ)
114		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
115		advlogexp 26580	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
116	94, 114, 115	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
117	111, 112, 113, 116, 72	dvmptcmul 25884	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))))
118	107	recnd 11162	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℂ)
119	72	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
120	71	nnne0d 12196	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ≠ 0)
121	120	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ≠ 0)
122	118, 119, 121	divcan2d 11920	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))) = ((log‘(𝑥 / 𝑦))↑𝑁))
123	122	mpteq2dva 5188	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
124	117, 123	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
125		oveq2 7361	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (𝑥 / 𝑦) = (𝑥 / 𝑛))
126	125	fveq2d 6830	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (log‘(𝑥 / 𝑦)) = (log‘(𝑥 / 𝑛)))
127	126	oveq1d 7368	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘(𝑥 / 𝑛))↑𝑁))
128	94	rpxrd 12956	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ*)
129		simp1rl 1239	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
130		simp2r 1201	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℝ+)
131	129, 130	rpdivcld 12972	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ∈ ℝ+)
132	131	relogcld 26548	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
133		simp2l 1200	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ∈ ℝ+)
134	129, 133	rpdivcld 12972	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
135	134	relogcld 26548	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
136		simp1l 1198	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
137		log1 26510	. . . . . . . . . . 11 ⊢ (log‘1) = 0
138	130	rpcnd 12957	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℂ)
139	138	mullidd 11152	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) = 𝑛)
140		simp33 1212	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥)
141	139, 140	eqbrtrd 5117	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) ≤ 𝑥)
142		1red 11135	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ∈ ℝ)
143	129	rpred 12955	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ)
144	142, 143, 130	lemuldivd 13004	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
145	141, 144	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑛))
146		logleb 26528	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
147	50, 131, 146	sylancr 587	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
148	145, 147	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
149	137, 148	eqbrtrrid 5131	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑛)))
150		simp32 1211	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ≤ 𝑛)
151	133, 130, 129	lediv2d 12979	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑦 ≤ 𝑛 ↔ (𝑥 / 𝑛) ≤ (𝑥 / 𝑦)))
152	150, 151	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ≤ (𝑥 / 𝑦))
153	131, 134	logled 26552	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((𝑥 / 𝑛) ≤ (𝑥 / 𝑦) ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦))))
154	152, 153	mpbid 232	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))
155		leexp1a 14100	. . . . . . . . . 10 ⊢ ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ (log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ (log‘(𝑥 / 𝑛)) ∧ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
156	132, 135, 136, 149, 154, 155	syl32anc 1380	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
157		eqid 2729	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))
158	96	3ad2antr1 1189	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
159	158	relogcld 26548	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
160		simpll 766	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
161		rpcn 12922	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
162	161	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℂ)
163	162	3ad2antr1 1189	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℂ)
164	163	mullidd 11152	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) = 𝑦)
165		simpr3 1197	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ≤ 𝑥)
166	164, 165	eqbrtrd 5117	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) ≤ 𝑥)
167		1red 11135	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ∈ ℝ)
168	94	rpred 12955	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
169	168	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑥 ∈ ℝ)
170		simpr1 1195	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℝ+)
171	167, 169, 170	lemuldivd 13004	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → ((1 · 𝑦) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑦)))
172	166, 171	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑦))
173		logleb 26528	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ+ ∧ (𝑥 / 𝑦) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
174	50, 158, 173	sylancr 587	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
175	172, 174	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑦)))
176	137, 175	eqbrtrrid 5131	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑦)))
177	159, 160, 176	expge0d 14089	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
178	50	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ+)
179		1le1 11766	. . . . . . . . . 10 ⊢ 1 ≤ 1
180	179	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 1)
181		simprr 772	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
182	168	leidd 11704	. . . . . . . . 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 25952	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) ≤ ⦋1 / 𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁))
184		fzfid 13898	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
185	94, 4, 5	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
186	185	relogcld 26548	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
187		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
188	186, 187	reexpcld 14088	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
189	184, 188	fsumrecl 15659	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
190	189	recnd 11162	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
191	94	rpcnd 12957	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ)
192	72, 191	mulcld 11154	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · 𝑥) ∈ ℂ)
193	11	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
194	193	recnd 11162	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ)
195	194, 114	expcld 14071	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℂ)
196		fzfid 13898	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (0...𝑁) ∈ Fin)
197	193, 20, 21	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
198	20	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
199	198	faccld 14209	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
200	197, 199	nndivred 12200	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
201	200	recnd 11162	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
202	196, 201	fsumcl 15658	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
203	72, 202	mulcld 11154	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
204	195, 203	subcld 11493	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
205	190, 192, 204	sub32d 11525	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
206		eqidd 2730	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))))
207		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
208	207	fveq2d 6830	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (⌊‘𝑦) = (⌊‘𝑥))
209	208	oveq2d 7369	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (1...(⌊‘𝑦)) = (1...(⌊‘𝑥)))
210	209	sumeq1d 15625	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁))
211		oveq2 7361	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (𝑥 / 𝑦) = (𝑥 / 𝑥))
212	65	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
213		divid 11828	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
214	212, 213	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 𝑥) = 1)
215	211, 214	sylan9eqr 2786	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 / 𝑦) = 1)
216	215	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 / 𝑦) = 1)
217	216	fveq2d 6830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘1))
218	217, 137	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = 0)
219	218	oveq1d 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = (0↑𝑘))
220	219	oveq1d 7368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = ((0↑𝑘) / (!‘𝑘)))
221	220	sumeq2dv 15627	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
222		nn0uz 12795	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ0 = (ℤ≥‘0)
223	114, 222	eleqtrdi 2838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ (ℤ≥‘0))
224		eluzfz1 13452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ≥‘0) → 0 ∈ (0...𝑁))
225	223, 224	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ (0...𝑁))
226	225	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 0 ∈ (0...𝑁))
227	226	snssd 4763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → {0} ⊆ (0...𝑁))
228		elsni 4596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ {0} → 𝑘 = 0)
229	228	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → 𝑘 = 0)
230		oveq2 7361	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0))
231		0exp0e1 13991	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0↑0) = 1
232	230, 231	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 0 → (0↑𝑘) = 1)
233		fveq2 6826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
234		fac0 14201	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (!‘0) = 1
235	233, 234	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
236	232, 235	oveq12d 7371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = (1 / 1))
237		1div1e1 11833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 / 1) = 1
238	236, 237	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = 1)
239	229, 238	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) = 1)
240		ax-1cn 11086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
241	239, 240	eqeltrdi 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) ∈ ℂ)
242		eldifi 4084	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ∈ (0...𝑁))
243	242	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (0...𝑁))
244	243, 20	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ0)
245		eldifsni 4744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ≠ 0)
246	245	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ≠ 0)
247		eldifsn 4740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (ℕ0 ∖ {0}) ↔ (𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0))
248	244, 246, 247	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (ℕ0 ∖ {0}))
249		dfn2 12415	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ = (ℕ0 ∖ {0})
250	248, 249	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ)
251	250	0expd 14064	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0↑𝑘) = 0)
252	251	oveq1d 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = (0 / (!‘𝑘)))
253	244	faccld 14209	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℕ)
254	253	nncnd 12162	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℂ)
255	253	nnne0d 12196	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ≠ 0)
256	254, 255	div0d 11917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0 / (!‘𝑘)) = 0)
257	252, 256	eqtrd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = 0)
258		fzfid 13898	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (0...𝑁) ∈ Fin)
259	227, 241, 257, 258	fsumss 15650	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
260	221, 259	eqtr4d 2767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)))
261		0cn 11126	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℂ
262	238	sumsn 15671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1)
263	261, 240, 262	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1
264	260, 263	eqtrdi 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = 1)
265	207, 264	oveq12d 7371	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (𝑥 · 1))
266	191	mulridd 11151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥)
267	266	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 · 1) = 𝑥)
268	265, 267	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = 𝑥)
269	268	oveq2d 7369	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · 𝑥))
270	210, 269	oveq12d 7371	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
271		ovexd 7388	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V)
272	206, 270, 94, 271	fvmptd 6941	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
273		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → 𝑦 = 1)
274	273	fveq2d 6830	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = (⌊‘1))
275		flid 13730	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℤ → (⌊‘1) = 1)
276	81, 275	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (⌊‘1) = 1
277	274, 276	eqtrdi 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = 1)
278	277	oveq2d 7369	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1...(⌊‘𝑦)) = (1...1))
279	278	sumeq1d 15625	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁))
280	191	div1d 11910	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 1) = 𝑥)
281	280	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 1) = 𝑥)
282	281	fveq2d 6830	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 1)) = (log‘𝑥))
283	282	oveq1d 7368	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) = ((log‘𝑥)↑𝑁))
284	195	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘𝑥)↑𝑁) ∈ ℂ)
285	283, 284	eqeltrd 2828	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ)
286		oveq2 7361	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (𝑥 / 𝑛) = (𝑥 / 1))
287	286	fveq2d 6830	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (log‘(𝑥 / 𝑛)) = (log‘(𝑥 / 1)))
288	287	oveq1d 7368	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → ((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
289	288	fsum1 15672	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℤ ∧ ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
290	81, 285, 289	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
291	279, 290, 283	3eqtrd 2768	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘𝑥)↑𝑁))
292	273	oveq2d 7369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = (𝑥 / 1))
293	292, 281	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = 𝑥)
294	293	fveq2d 6830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
295	294	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
296	295	oveq1d 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = ((log‘𝑥)↑𝑘))
297	296	oveq1d 7368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = (((log‘𝑥)↑𝑘) / (!‘𝑘)))
298	297	sumeq2dv 15627	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
299	273, 298	oveq12d 7371	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
300	202	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
301	300	mullidd 11152	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
302	299, 301	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
303	302	oveq2d 7369	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
304	291, 303	oveq12d 7371	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
305		ovexd 7388	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V)
306	206, 304, 178, 305	fvmptd 6941	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
307	272, 306	oveq12d 7371	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
308	70, 72, 191	subdird 11595	. . . . . . . . . . . 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 495	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0)
311	309, 191, 310	divcan1d 11919	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
312	311	oveq1d 7368	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
313	308, 312	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
314	205, 307, 313	3eqtr4d 2774	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥))
315	314	fveq2d 6830	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)))
316	73, 191	absmuld 15382	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)))
317		rprege0 12927	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
318	317	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
319		absid 15221	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
320	318, 319	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥)
321	320	oveq2d 7369	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
322	315, 316, 321	3eqtrd 2768	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
323		1cnd 11129	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ)
324	294	oveq1d 7368	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
325	323, 324	csbied 3889	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ⦋1 / 𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
326	183, 322, 325	3brtr3d 5126	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁))
327	14	adantrr 717	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℝ)
328	74, 327, 94	lemuldivd 13004	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁) ↔ (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥)))
329	326, 328	mpbid 232	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥))
330	75	leabsd 15340	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
331	74, 75, 77, 329, 330	letrd 11291	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
332	57	adantrr 717	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
333	332	subid1d 11482	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥)↑𝑁) / 𝑥) − 0) = (((log‘𝑥)↑𝑁) / 𝑥))
334	333	fveq2d 6830	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)) = (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
335	331, 334	breqtrrd 5123	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)))
336	33, 34, 54, 57, 69, 335	rlimsqzlem 15574	. . 3 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥)) ⇝𝑟 (!‘𝑁))
337		divsubdir 11836	. . . . . 6 ⊢ ((((log‘𝑥)↑𝑁) ∈ ℂ ∧ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
338	59, 62, 66, 337	syl3anc 1373	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
339	338	mpteq2dva 5188	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))))
340		rerpdivcl 12943	. . . . . . 7 ⊢ ((((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
341	27, 340	sylancom 588	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
342		divass 11815	. . . . . . . . . 10 ⊢ (((!‘𝑁) ∈ ℂ ∧ Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
343	60, 61, 66, 342	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
344	25	recnd 11162	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
345	18, 67, 344, 68	fsumdivc 15711	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))
346	22	recnd 11162	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℂ)
347	24	nnrpd 12953	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ+)
348	347	rpcnne0d 12964	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0))
349	66	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
350		divdiv32 11850	. . . . . . . . . . . . 13 ⊢ ((((log‘𝑥)↑𝑘) ∈ ℂ ∧ ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
351	346, 348, 349, 350	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
352	351	sumeq2dv 15627	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
353	345, 352	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
354	353	oveq2d 7369	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
355	343, 354	eqtrd 2764	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
356	355	mpteq2dva 5188	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))))
357	2	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℝ+)
358	22, 357	rerpdivcld 12986	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
359	358, 24	nndivred 12200	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
360	18, 359	fsumrecl 15659	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
361		rpssre 12919	. . . . . . . . . 10 ⊢ ℝ+ ⊆ ℝ
362		rlimconst 15469	. . . . . . . . . 10 ⊢ ((ℝ+ ⊆ ℝ ∧ (!‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
363	361, 34, 362	sylancr 587	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
364	361	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → ℝ+ ⊆ ℝ)
365		fzfid 13898	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (0...𝑁) ∈ Fin)
366	359	anasss 466	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 𝑘 ∈ (0...𝑁))) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
367	358	an32s 652	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
368	20	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
369	368	faccld 14209	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
370	369	nnred 12161	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ)
371	370	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ∈ ℝ)
372	368, 53	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
373	369	nncnd 12162	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℂ)
374		rlimconst 15469	. . . . . . . . . . . . . 14 ⊢ ((ℝ+ ⊆ ℝ ∧ (!‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
375	361, 373, 374	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
376	369	nnne0d 12196	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0)
377	376	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ≠ 0)
378	367, 371, 372, 375, 376, 377	rlimdiv 15571	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 (0 / (!‘𝑘)))
379	373, 376	div0d 11917	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (0 / (!‘𝑘)) = 0)
380	378, 379	breqtrd 5121	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
381	364, 365, 366, 380	fsumrlim 15736	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 Σ𝑘 ∈ (0...𝑁)0)
382		fzfi 13897	. . . . . . . . . . . 12 ⊢ (0...𝑁) ∈ Fin
383	382	olci 866	. . . . . . . . . . 11 ⊢ ((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin)
384		sumz 15647	. . . . . . . . . . 11 ⊢ (((0...𝑁) ⊆ (ℤ≥‘0) ∨ (0...𝑁) ∈ Fin) → Σ𝑘 ∈ (0...𝑁)0 = 0)
385	383, 384	ax-mp 5	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...𝑁)0 = 0
386	381, 385	breqtrdi 5136	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
387	17, 360, 363, 386	rlimmul 15570	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 ((!‘𝑁) · 0))
388	34	mul01d 11333	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → ((!‘𝑁) · 0) = 0)
389	387, 388	breqtrd 5121	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 0)
390	356, 389	eqbrtrd 5117	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) ⇝𝑟 0)
391	56, 341, 54, 390	rlimsub 15569	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 (0 − 0))
392		0m0e0 12261	. . . . 5 ⊢ (0 − 0) = 0
393	391, 392	breqtrdi 5136	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 0)
394	339, 393	eqbrtrd 5117	. . 3 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) ⇝𝑟 0)
395	30, 32, 336, 394	rlimadd 15568	. 2 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) ⇝𝑟 ((!‘𝑁) + 0))
396		divsubdir 11836	. . . . . 6 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ ∧ (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
397	58, 63, 66, 396	syl3anc 1373	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
398	397	oveq1d 7368	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
399	10, 2	rerpdivcld 12986	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℝ)
400	399	recnd 11162	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℂ)
401	32	recnd 11162	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℂ)
402	400, 401	npcand 11497	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
403	398, 402	eqtrd 2764	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
404	403	mpteq2dva 5188	. 2 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)))
405	34	addridd 11334	. 2 ⊢ (𝑁 ∈ ℕ0 → ((!‘𝑁) + 0) = (!‘𝑁))
406	395, 404, 405	3brtr3d 5126	1 ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  Vcvv 3438  ⦋csb 3853   ∖ cdif 3902   ⊆ wss 3905  {csn 4579  {cpr 4581   class class class wbr 5095   ↦ cmpt 5176  ‘cfv 6486  (class class class)co 7353  Fincfn 8879  ℂcc 11026  ℝcr 11027  0cc0 11028  1c1 11029   + caddc 11031   · cmul 11033  +∞cpnf 11165   ≤ cle 11169   − cmin 11365   / cdiv 11795  ℕcn 12146  ℕ₀cn0 12402  ℤcz 12489  ℤ_≥cuz 12753  ℝ⁺crp 12911  (,)cioo 13266  ...cfz 13428  ⌊cfl 13712  ↑cexp 13986  !cfa 14198  abscabs 15159   ⇝_𝑟 crli 15410  Σcsu 15611   D cdv 25780  logclog 26479  ↑_𝑐ccxp 26480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-inf2 9556  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105  ax-pre-sup 11106  ax-addf 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-iin 4947  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7617  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8632  df-map 8762  df-pm 8763  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-fi 9320  df-sup 9351  df-inf 9352  df-oi 9421  df-card 9854  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-div 11796  df-nn 12147  df-2 12209  df-3 12210  df-4 12211  df-5 12212  df-6 12213  df-7 12214  df-8 12215  df-9 12216  df-n0 12403  df-z 12490  df-dec 12610  df-uz 12754  df-q 12868  df-rp 12912  df-xneg 13032  df-xadd 13033  df-xmul 13034  df-ioo 13270  df-ioc 13271  df-ico 13272  df-icc 13273  df-fz 13429  df-fzo 13576  df-fl 13714  df-mod 13792  df-seq 13927  df-exp 13987  df-fac 14199  df-bc 14228  df-hash 14256  df-shft 14992  df-cj 15024  df-re 15025  df-im 15026  df-sqrt 15160  df-abs 15161  df-limsup 15396  df-clim 15413  df-rlim 15414  df-sum 15612  df-ef 15992  df-e 15993  df-sin 15994  df-cos 15995  df-pi 15997  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17139  df-ress 17160  df-plusg 17192  df-mulr 17193  df-starv 17194  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-unif 17202  df-hom 17203  df-cco 17204  df-rest 17344  df-topn 17345  df-0g 17363  df-gsum 17364  df-topgen 17365  df-pt 17366  df-prds 17369  df-xrs 17424  df-qtop 17429  df-imas 17430  df-xps 17432  df-mre 17506  df-mrc 17507  df-acs 17509  df-mgm 18532  df-sgrp 18611  df-mnd 18627  df-submnd 18676  df-mulg 18965  df-cntz 19214  df-cmn 19679  df-psmet 21271  df-xmet 21272  df-met 21273  df-bl 21274  df-mopn 21275  df-fbas 21276  df-fg 21277  df-cnfld 21280  df-top 22797  df-topon 22814  df-topsp 22836  df-bases 22849  df-cld 22922  df-ntr 22923  df-cls 22924  df-nei 23001  df-lp 23039  df-perf 23040  df-cn 23130  df-cnp 23131  df-haus 23218  df-cmp 23290  df-tx 23465  df-hmeo 23658  df-fil 23749  df-fm 23841  df-flim 23842  df-flf 23843  df-xms 24224  df-ms 24225  df-tms 24226  df-cncf 24787  df-limc 25783  df-dv 25784  df-log 26481  df-cxp 26482

This theorem is referenced by:  logfacrlim2  27153  selberglem2  27473