MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  logexprlim Structured version   Visualization version   GIF version

Theorem logexprlim 26373
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.
StepHypRef Expression
1 fzfid 13693 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
2 simpr 485 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
3 elfznn 13285 . . . . . . . . . 10 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
43nnrpd 12770 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
5 rpdivcl 12755 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
62, 4, 5syl2an 596 . . . . . . . 8 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
76relogcld 25778 . . . . . . 7 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
8 simpll 764 . . . . . . 7 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
97, 8reexpcld 13881 . . . . . 6 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
101, 9fsumrecl 15446 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
11 relogcl 25731 . . . . . . 7 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
12 id 22 . . . . . . 7 (𝑁 ∈ ℕ0𝑁 ∈ ℕ0)
13 reexpcl 13799 . . . . . . 7 (((log‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℕ0) → ((log‘𝑥)↑𝑁) ∈ ℝ)
1411, 12, 13syl2anr 597 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℝ)
15 faccl 13997 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
1615adantr 481 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
1716nnred 11988 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
18 fzfid 13693 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (0...𝑁) ∈ Fin)
1911adantl 482 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
20 elfznn0 13349 . . . . . . . . . 10 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
21 reexpcl 13799 . . . . . . . . . 10 (((log‘𝑥) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑘) ∈ ℝ)
2219, 20, 21syl2an 596 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
2320adantl 482 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
2423faccld 13998 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
2522, 24nndivred 12027 . . . . . . . 8 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
2618, 25fsumrecl 15446 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
2717, 26remulcld 11005 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ)
2814, 27resubcld 11403 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ)
2910, 28resubcld 11403 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℝ)
3029, 2rerpdivcld 12803 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℝ)
31 rerpdivcl 12760 . . . 4 (((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
3228, 31sylancom 588 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
33 1red 10976 . . . 4 (𝑁 ∈ ℕ0 → 1 ∈ ℝ)
3415nncnd 11989 . . . 4 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℂ)
35 simpl 483 . . . . . . . . 9 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → 𝑘 = 𝑁)
3635oveq2d 7291 . . . . . . . 8 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑘) = ((log‘𝑥)↑𝑁))
3736oveq1d 7290 . . . . . . 7 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) = (((log‘𝑥)↑𝑁) / 𝑥))
3837mpteq2dva 5174 . . . . . 6 (𝑘 = 𝑁 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)))
3938breq1d 5084 . . . . 5 (𝑘 = 𝑁 → ((𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0 ↔ (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0))
4011recnd 11003 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℂ)
41 id 22 . . . . . . . . 9 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
42 cxpexp 25823 . . . . . . . . 9 (((log‘𝑥) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
4340, 41, 42syl2anr 597 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
44 rpcn 12740 . . . . . . . . . 10 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
4544adantl 482 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
4645cxp1d 25861 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → (𝑥𝑐1) = 𝑥)
4743, 46oveq12d 7293 . . . . . . 7 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1)) = (((log‘𝑥)↑𝑘) / 𝑥))
4847mpteq2dva 5174 . . . . . 6 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)))
49 nn0cn 12243 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
50 1rp 12734 . . . . . . 7 1 ∈ ℝ+
51 cxploglim2 26128 . . . . . . 7 ((𝑘 ∈ ℂ ∧ 1 ∈ ℝ+) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) ⇝𝑟 0)
5249, 50, 51sylancl 586 . . . . . 6 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) ⇝𝑟 0)
5348, 52eqbrtrrd 5098 . . . . 5 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
5439, 53vtoclga 3513 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0)
55 rerpdivcl 12760 . . . . . 6 ((((log‘𝑥)↑𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
5614, 55sylancom 588 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
5756recnd 11003 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
5810recnd 11003 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
5914recnd 11003 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℂ)
6034adantr 481 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
6126recnd 11003 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
6260, 61mulcld 10995 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
6359, 62subcld 11332 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
6458, 63subcld 11332 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
65 rpcnne0 12748 . . . . . . 7 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
6665adantl 482 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
6766simpld 495 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
6866simprd 496 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
6964, 67, 68divcld 11751 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
7069adantrr 714 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
7115adantr 481 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℕ)
7271nncnd 11989 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℂ)
7370, 72subcld 11332 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) ∈ ℂ)
7473abscld 15148 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ∈ ℝ)
7556adantrr 714 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
7675recnd 11003 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
7776abscld 15148 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥)↑𝑁) / 𝑥)) ∈ ℝ)
78 ioorp 13157 . . . . . . . . . 10 (0(,)+∞) = ℝ+
7978eqcomi 2747 . . . . . . . . 9 + = (0(,)+∞)
80 nnuz 12621 . . . . . . . . 9 ℕ = (ℤ‘1)
81 1z 12350 . . . . . . . . . 10 1 ∈ ℤ
8281a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℤ)
83 1red 10976 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ)
84 1re 10975 . . . . . . . . . . 11 1 ∈ ℝ
85 1nn0 12249 . . . . . . . . . . 11 1 ∈ ℕ0
8684, 85nn0addge1i 12281 . . . . . . . . . 10 1 ≤ (1 + 1)
8786a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ (1 + 1))
88 0red 10978 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ)
8971adantr 481 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
9089nnred 11988 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
91 rpre 12738 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
9291adantl 482 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
93 fzfid 13693 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (0...𝑁) ∈ Fin)
94 simprl 768 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
95 rpdivcl 12755 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
9694, 95sylan 580 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
9796relogcld 25778 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
98 reexpcl 13799 . . . . . . . . . . . . . 14 (((log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
9997, 20, 98syl2an 596 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
10020adantl 482 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
101100faccld 13998 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
10299, 101nndivred 12027 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
10393, 102fsumrecl 15446 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
10492, 103remulcld 11005 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℝ)
10590, 104remulcld 11005 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) ∈ ℝ)
106 simpll 764 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑁 ∈ ℕ0)
10797, 106reexpcld 13881 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
108 nnrp 12741 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
109108, 107sylan2 593 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℕ) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
110 reelprrecn 10963 . . . . . . . . . . . 12 ℝ ∈ {ℝ, ℂ}
111110a1i 11 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ℝ ∈ {ℝ, ℂ})
112104recnd 11003 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℂ)
113107, 89nndivred 12027 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)) ∈ ℝ)
114 simpl 483 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
115 advlogexp 25810 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
11694, 114, 115syl2anc 584 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
117111, 112, 113, 116, 72dvmptcmul 25128 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))))
118107recnd 11003 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℂ)
11972adantr 481 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
12071nnne0d 12023 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ≠ 0)
121120adantr 481 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ≠ 0)
122118, 119, 121divcan2d 11753 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))) = ((log‘(𝑥 / 𝑦))↑𝑁))
123122mpteq2dva 5174 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
124117, 123eqtrd 2778 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
125 oveq2 7283 . . . . . . . . . . 11 (𝑦 = 𝑛 → (𝑥 / 𝑦) = (𝑥 / 𝑛))
126125fveq2d 6778 . . . . . . . . . 10 (𝑦 = 𝑛 → (log‘(𝑥 / 𝑦)) = (log‘(𝑥 / 𝑛)))
127126oveq1d 7290 . . . . . . . . 9 (𝑦 = 𝑛 → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘(𝑥 / 𝑛))↑𝑁))
12894rpxrd 12773 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ*)
129 simp1rl 1237 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑥 ∈ ℝ+)
130 simp2r 1199 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛 ∈ ℝ+)
131129, 130rpdivcld 12789 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑛) ∈ ℝ+)
132131relogcld 25778 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
133 simp2l 1198 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑦 ∈ ℝ+)
134129, 133rpdivcld 12789 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
135134relogcld 25778 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
136 simp1l 1196 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑁 ∈ ℕ0)
137 log1 25741 . . . . . . . . . . 11 (log‘1) = 0
138130rpcnd 12774 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛 ∈ ℂ)
139138mulid2d 10993 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 · 𝑛) = 𝑛)
140 simp33 1210 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛𝑥)
141139, 140eqbrtrd 5096 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 · 𝑛) ≤ 𝑥)
142 1red 10976 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 1 ∈ ℝ)
143129rpred 12772 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑥 ∈ ℝ)
144142, 143, 130lemuldivd 12821 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
145141, 144mpbid 231 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 1 ≤ (𝑥 / 𝑛))
146 logleb 25758 . . . . . . . . . . . . 13 ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
14750, 131, 146sylancr 587 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
148145, 147mpbid 231 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
149137, 148eqbrtrrid 5110 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 0 ≤ (log‘(𝑥 / 𝑛)))
150 simp32 1209 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑦𝑛)
151133, 130, 129lediv2d 12796 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑦𝑛 ↔ (𝑥 / 𝑛) ≤ (𝑥 / 𝑦)))
152150, 151mpbid 231 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑛) ≤ (𝑥 / 𝑦))
153131, 134logled 25782 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((𝑥 / 𝑛) ≤ (𝑥 / 𝑦) ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦))))
154152, 153mpbid 231 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))
155 leexp1a 13893 . . . . . . . . . 10 ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ (log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ (log‘(𝑥 / 𝑛)) ∧ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
156132, 135, 136, 149, 154, 155syl32anc 1377 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
157 eqid 2738 . . . . . . . . 9 (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))
158963ad2antr1 1187 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
159158relogcld 25778 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
160 simpll 764 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑁 ∈ ℕ0)
161 rpcn 12740 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
162161adantl 482 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℂ)
1631623ad2antr1 1187 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦 ∈ ℂ)
164163mulid2d 10993 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 · 𝑦) = 𝑦)
165 simpr3 1195 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦𝑥)
166164, 165eqbrtrd 5096 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 · 𝑦) ≤ 𝑥)
167 1red 10976 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 1 ∈ ℝ)
16894rpred 12772 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
169168adantr 481 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑥 ∈ ℝ)
170 simpr1 1193 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦 ∈ ℝ+)
171167, 169, 170lemuldivd 12821 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → ((1 · 𝑦) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑦)))
172166, 171mpbid 231 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 1 ≤ (𝑥 / 𝑦))
173 logleb 25758 . . . . . . . . . . . . 13 ((1 ∈ ℝ+ ∧ (𝑥 / 𝑦) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
17450, 158, 173sylancr 587 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
175172, 174mpbid 231 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑦)))
176137, 175eqbrtrrid 5110 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 0 ≤ (log‘(𝑥 / 𝑦)))
177159, 160, 176expge0d 13882 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
17850a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ+)
179 1le1 11603 . . . . . . . . . 10 1 ≤ 1
180179a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 1)
181 simprr 770 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
182168leidd 11541 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥𝑥)
18379, 80, 82, 83, 87, 88, 105, 107, 109, 124, 127, 128, 156, 157, 177, 178, 94, 180, 181, 182dvfsumlem4 25193 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) ≤ 1 / 𝑦((log‘(𝑥 / 𝑦))↑𝑁))
184 fzfid 13693 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
18594, 4, 5syl2an 596 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
186185relogcld 25778 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
187 simpll 764 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
188186, 187reexpcld 13881 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
189184, 188fsumrecl 15446 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
190189recnd 11003 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
19194rpcnd 12774 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ)
19272, 191mulcld 10995 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · 𝑥) ∈ ℂ)
19311ad2antrl 725 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
194193recnd 11003 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ)
195194, 114expcld 13864 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℂ)
196 fzfid 13693 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (0...𝑁) ∈ Fin)
197193, 20, 21syl2an 596 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
19820adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
199198faccld 13998 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
200197, 199nndivred 12027 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
201200recnd 11003 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
202196, 201fsumcl 15445 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
20372, 202mulcld 10995 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
204195, 203subcld 11332 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
205190, 192, 204sub32d 11364 . . . . . . . . . . 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 485 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
208207fveq2d 6778 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (⌊‘𝑦) = (⌊‘𝑥))
209208oveq2d 7291 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (1...(⌊‘𝑦)) = (1...(⌊‘𝑥)))
210209sumeq1d 15413 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁))
211 oveq2 7283 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (𝑥 / 𝑦) = (𝑥 / 𝑥))
21265ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
213 divid 11662 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
214212, 213syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 𝑥) = 1)
215211, 214sylan9eqr 2800 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 / 𝑦) = 1)
216215adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 / 𝑦) = 1)
217216fveq2d 6778 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘1))
218217, 137eqtrdi 2794 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = 0)
219218oveq1d 7290 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = (0↑𝑘))
220219oveq1d 7290 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = ((0↑𝑘) / (!‘𝑘)))
221220sumeq2dv 15415 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
222 nn0uz 12620 . . . . . . . . . . . . . . . . . . . . . . . 24 0 = (ℤ‘0)
223114, 222eleqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ (ℤ‘0))
224 eluzfz1 13263 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘0) → 0 ∈ (0...𝑁))
225223, 224syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ (0...𝑁))
226225adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 0 ∈ (0...𝑁))
227226snssd 4742 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → {0} ⊆ (0...𝑁))
228 elsni 4578 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ {0} → 𝑘 = 0)
229228adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → 𝑘 = 0)
230 oveq2 7283 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 0 → (0↑𝑘) = (0↑0))
231 0exp0e1 13787 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0↑0) = 1
232230, 231eqtrdi 2794 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 0 → (0↑𝑘) = 1)
233 fveq2 6774 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 0 → (!‘𝑘) = (!‘0))
234 fac0 13990 . . . . . . . . . . . . . . . . . . . . . . . . 25 (!‘0) = 1
235233, 234eqtrdi 2794 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 0 → (!‘𝑘) = 1)
236232, 235oveq12d 7293 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = (1 / 1))
237 1div1e1 11665 . . . . . . . . . . . . . . . . . . . . . . 23 (1 / 1) = 1
238236, 237eqtrdi 2794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = 1)
239229, 238syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) = 1)
240 ax-1cn 10929 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
241239, 240eqeltrdi 2847 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) ∈ ℂ)
242 eldifi 4061 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ∈ (0...𝑁))
243242adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (0...𝑁))
244243, 20syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ0)
245 eldifsni 4723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ≠ 0)
246245adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ≠ 0)
247 eldifsn 4720 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (ℕ0 ∖ {0}) ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
248244, 246, 247sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (ℕ0 ∖ {0}))
249 dfn2 12246 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℕ0 ∖ {0})
250248, 249eleqtrrdi 2850 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ)
2512500expd 13857 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0↑𝑘) = 0)
252251oveq1d 7290 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = (0 / (!‘𝑘)))
253244faccld 13998 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℕ)
254253nncnd 11989 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℂ)
255253nnne0d 12023 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ≠ 0)
256254, 255div0d 11750 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0 / (!‘𝑘)) = 0)
257252, 256eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = 0)
258 fzfid 13693 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (0...𝑁) ∈ Fin)
259227, 241, 257, 258fsumss 15437 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
260221, 259eqtr4d 2781 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)))
261 0cn 10967 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℂ
262238sumsn 15458 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1)
263261, 240, 262mp2an 689 . . . . . . . . . . . . . . . . . 18 Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1
264260, 263eqtrdi 2794 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = 1)
265207, 264oveq12d 7293 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (𝑥 · 1))
266191mulid1d 10992 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥)
267266adantr 481 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 · 1) = 𝑥)
268265, 267eqtrd 2778 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = 𝑥)
269268oveq2d 7291 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · 𝑥))
270210, 269oveq12d 7293 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
271 ovexd 7310 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V)
272206, 270, 94, 271fvmptd 6882 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
273 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → 𝑦 = 1)
274273fveq2d 6778 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = (⌊‘1))
275 flid 13528 . . . . . . . . . . . . . . . . . . 19 (1 ∈ ℤ → (⌊‘1) = 1)
27681, 275ax-mp 5 . . . . . . . . . . . . . . . . . 18 (⌊‘1) = 1
277274, 276eqtrdi 2794 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = 1)
278277oveq2d 7291 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1...(⌊‘𝑦)) = (1...1))
279278sumeq1d 15413 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁))
280191div1d 11743 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 1) = 𝑥)
281280adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 1) = 𝑥)
282281fveq2d 6778 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 1)) = (log‘𝑥))
283282oveq1d 7290 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) = ((log‘𝑥)↑𝑁))
284195adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘𝑥)↑𝑁) ∈ ℂ)
285283, 284eqeltrd 2839 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ)
286 oveq2 7283 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑥 / 𝑛) = (𝑥 / 1))
287286fveq2d 6778 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (log‘(𝑥 / 𝑛)) = (log‘(𝑥 / 1)))
288287oveq1d 7290 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
289288fsum1 15459 . . . . . . . . . . . . . . . 16 ((1 ∈ ℤ ∧ ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
29081, 285, 289sylancr 587 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
291279, 290, 2833eqtrd 2782 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘𝑥)↑𝑁))
292273oveq2d 7291 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = (𝑥 / 1))
293292, 281eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = 𝑥)
294293fveq2d 6778 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
295294adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
296295oveq1d 7290 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = ((log‘𝑥)↑𝑘))
297296oveq1d 7290 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = (((log‘𝑥)↑𝑘) / (!‘𝑘)))
298297sumeq2dv 15415 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
299273, 298oveq12d 7293 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
300202adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
301300mulid2d 10993 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
302299, 301eqtrd 2778 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
303302oveq2d 7291 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
304291, 303oveq12d 7293 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
305 ovexd 7310 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V)
306206, 304, 178, 305fvmptd 6882 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
307272, 306oveq12d 7293 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
30870, 72, 191subdird 11432 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)))
30964adantrr 714 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
310212simprd 496 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0)
311309, 191, 310divcan1d 11752 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
312311oveq1d 7290 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
313308, 312eqtrd 2778 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
314205, 307, 3133eqtr4d 2788 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥))
315314fveq2d 6778 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)))
31673, 191absmuld 15166 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)))
317 rprege0 12745 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
318317ad2antrl 725 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
319 absid 15008 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
320318, 319syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥)
321320oveq2d 7291 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
322315, 316, 3213eqtrd 2782 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
323 1cnd 10970 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ)
324294oveq1d 7290 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
325323, 324csbied 3870 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 / 𝑦((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
326183, 322, 3253brtr3d 5105 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁))
32714adantrr 714 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℝ)
32874, 327, 94lemuldivd 12821 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁) ↔ (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥)))
329326, 328mpbid 231 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥))
33075leabsd 15126 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
33174, 75, 77, 329, 330letrd 11132 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
33257adantrr 714 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
333332subid1d 11321 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥)↑𝑁) / 𝑥) − 0) = (((log‘𝑥)↑𝑁) / 𝑥))
334333fveq2d 6778 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)) = (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
335331, 334breqtrrd 5102 . . . 4 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)))
33633, 34, 54, 57, 69, 335rlimsqzlem 15360 . . 3 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥)) ⇝𝑟 (!‘𝑁))
337 divsubdir 11669 . . . . . 6 ((((log‘𝑥)↑𝑁) ∈ ℂ ∧ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
33859, 62, 66, 337syl3anc 1370 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
339338mpteq2dva 5174 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))))
340 rerpdivcl 12760 . . . . . . 7 ((((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
34127, 340sylancom 588 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
342 divass 11651 . . . . . . . . . 10 (((!‘𝑁) ∈ ℂ ∧ Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
34360, 61, 66, 342syl3anc 1370 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
34425recnd 11003 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
34518, 67, 344, 68fsumdivc 15498 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))
34622recnd 11003 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℂ)
34724nnrpd 12770 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ+)
348347rpcnne0d 12781 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0))
34966adantr 481 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
350 divdiv32 11683 . . . . . . . . . . . . 13 ((((log‘𝑥)↑𝑘) ∈ ℂ ∧ ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
351346, 348, 349, 350syl3anc 1370 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
352351sumeq2dv 15415 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
353345, 352eqtrd 2778 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
354353oveq2d 7291 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
355343, 354eqtrd 2778 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
356355mpteq2dva 5174 . . . . . . 7 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))))
3572adantr 481 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℝ+)
35822, 357rerpdivcld 12803 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
359358, 24nndivred 12027 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
36018, 359fsumrecl 15446 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
361 rpssre 12737 . . . . . . . . . 10 + ⊆ ℝ
362 rlimconst 15253 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ (!‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
363361, 34, 362sylancr 587 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
364361a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → ℝ+ ⊆ ℝ)
365 fzfid 13693 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (0...𝑁) ∈ Fin)
366359anasss 467 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+𝑘 ∈ (0...𝑁))) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
367358an32s 649 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
36820adantl 482 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
369368faccld 13998 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
370369nnred 11988 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ)
371370adantr 481 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ∈ ℝ)
372368, 53syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
373369nncnd 11989 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℂ)
374 rlimconst 15253 . . . . . . . . . . . . . 14 ((ℝ+ ⊆ ℝ ∧ (!‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
375361, 373, 374sylancr 587 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
376369nnne0d 12023 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0)
377376adantr 481 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ≠ 0)
378367, 371, 372, 375, 376, 377rlimdiv 15357 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 (0 / (!‘𝑘)))
379373, 376div0d 11750 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (0 / (!‘𝑘)) = 0)
380378, 379breqtrd 5100 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
381364, 365, 366, 380fsumrlim 15523 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 Σ𝑘 ∈ (0...𝑁)0)
382 fzfi 13692 . . . . . . . . . . . 12 (0...𝑁) ∈ Fin
383382olci 863 . . . . . . . . . . 11 ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin)
384 sumz 15434 . . . . . . . . . . 11 (((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin) → Σ𝑘 ∈ (0...𝑁)0 = 0)
385383, 384ax-mp 5 . . . . . . . . . 10 Σ𝑘 ∈ (0...𝑁)0 = 0
386381, 385breqtrdi 5115 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
38717, 360, 363, 386rlimmul 15355 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 ((!‘𝑁) · 0))
38834mul01d 11174 . . . . . . . 8 (𝑁 ∈ ℕ0 → ((!‘𝑁) · 0) = 0)
389387, 388breqtrd 5100 . . . . . . 7 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 0)
390356, 389eqbrtrd 5096 . . . . . 6 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) ⇝𝑟 0)
39156, 341, 54, 390rlimsub 15354 . . . . 5 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 (0 − 0))
392 0m0e0 12093 . . . . 5 (0 − 0) = 0
393391, 392breqtrdi 5115 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 0)
394339, 393eqbrtrd 5096 . . 3 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) ⇝𝑟 0)
39530, 32, 336, 394rlimadd 15352 . 2 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) ⇝𝑟 ((!‘𝑁) + 0))
396 divsubdir 11669 . . . . . 6 ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ ∧ (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
39758, 63, 66, 396syl3anc 1370 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
398397oveq1d 7290 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
39910, 2rerpdivcld 12803 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℝ)
400399recnd 11003 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℂ)
40132recnd 11003 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℂ)
402400, 401npcand 11336 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
403398, 402eqtrd 2778 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
404403mpteq2dva 5174 . 2 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)))
40534addid1d 11175 . 2 (𝑁 ∈ ℕ0 → ((!‘𝑁) + 0) = (!‘𝑁))
406395, 404, 4053brtr3d 5105 1 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  wcel 2106  wne 2943  Vcvv 3432  csb 3832  cdif 3884  wss 3887  {csn 4561  {cpr 4563   class class class wbr 5074  cmpt 5157  cfv 6433  (class class class)co 7275  Fincfn 8733  cc 10869  cr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876  +∞cpnf 11006  cle 11010  cmin 11205   / cdiv 11632  cn 11973  0cn0 12233  cz 12319  cuz 12582  +crp 12730  (,)cioo 13079  ...cfz 13239  cfl 13510  cexp 13782  !cfa 13987  abscabs 14945  𝑟 crli 15194  Σcsu 15397   D cdv 25027  logclog 25710  𝑐ccxp 25711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949  ax-addf 10950  ax-mulf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-map 8617  df-pm 8618  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-fi 9170  df-sup 9201  df-inf 9202  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-q 12689  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-ioo 13083  df-ioc 13084  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-fl 13512  df-mod 13590  df-seq 13722  df-exp 13783  df-fac 13988  df-bc 14017  df-hash 14045  df-shft 14778  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-limsup 15180  df-clim 15197  df-rlim 15198  df-sum 15398  df-ef 15777  df-e 15778  df-sin 15779  df-cos 15780  df-pi 15782  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-hom 16986  df-cco 16987  df-rest 17133  df-topn 17134  df-0g 17152  df-gsum 17153  df-topgen 17154  df-pt 17155  df-prds 17158  df-xrs 17213  df-qtop 17218  df-imas 17219  df-xps 17221  df-mre 17295  df-mrc 17296  df-acs 17298  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-mulg 18701  df-cntz 18923  df-cmn 19388  df-psmet 20589  df-xmet 20590  df-met 20591  df-bl 20592  df-mopn 20593  df-fbas 20594  df-fg 20595  df-cnfld 20598  df-top 22043  df-topon 22060  df-topsp 22082  df-bases 22096  df-cld 22170  df-ntr 22171  df-cls 22172  df-nei 22249  df-lp 22287  df-perf 22288  df-cn 22378  df-cnp 22379  df-haus 22466  df-cmp 22538  df-tx 22713  df-hmeo 22906  df-fil 22997  df-fm 23089  df-flim 23090  df-flf 23091  df-xms 23473  df-ms 23474  df-tms 23475  df-cncf 24041  df-limc 25030  df-dv 25031  df-log 25712  df-cxp 25713
This theorem is referenced by:  logfacrlim2  26374  selberglem2  26694
  Copyright terms: Public domain W3C validator