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

Theorem logexprlim 24694
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 12591 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
2 simpr 475 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
3 elfznn 12198 . . . . . . . . . 10 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
43nnrpd 11704 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
5 rpdivcl 11690 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
62, 4, 5syl2an 492 . . . . . . . 8 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
76relogcld 24117 . . . . . . 7 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
8 simpll 785 . . . . . . 7 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
97, 8reexpcld 12844 . . . . . 6 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
101, 9fsumrecl 14260 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
11 relogcl 24070 . . . . . . 7 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
12 id 22 . . . . . . 7 (𝑁 ∈ ℕ0𝑁 ∈ ℕ0)
13 reexpcl 12696 . . . . . . 7 (((log‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℕ0) → ((log‘𝑥)↑𝑁) ∈ ℝ)
1411, 12, 13syl2anr 493 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℝ)
15 faccl 12889 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
1615adantr 479 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
1716nnred 10884 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
18 fzfid 12591 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (0...𝑁) ∈ Fin)
1911adantl 480 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
20 elfznn0 12259 . . . . . . . . . 10 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
21 reexpcl 12696 . . . . . . . . . 10 (((log‘𝑥) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑘) ∈ ℝ)
2219, 20, 21syl2an 492 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
2320adantl 480 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
24 faccl 12889 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
2523, 24syl 17 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
2622, 25nndivred 10918 . . . . . . . 8 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
2718, 26fsumrecl 14260 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
2817, 27remulcld 9926 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ)
2914, 28resubcld 10309 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ)
3010, 29resubcld 10309 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℝ)
3130, 2rerpdivcld 11737 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℝ)
32 rerpdivcl 11695 . . . 4 (((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
3329, 32sylancom 697 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
34 1red 9911 . . . 4 (𝑁 ∈ ℕ0 → 1 ∈ ℝ)
3515nncnd 10885 . . . 4 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℂ)
36 simpl 471 . . . . . . . . 9 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → 𝑘 = 𝑁)
3736oveq2d 6542 . . . . . . . 8 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑘) = ((log‘𝑥)↑𝑁))
3837oveq1d 6541 . . . . . . 7 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) = (((log‘𝑥)↑𝑁) / 𝑥))
3938mpteq2dva 4666 . . . . . 6 (𝑘 = 𝑁 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)))
4039breq1d 4587 . . . . 5 (𝑘 = 𝑁 → ((𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0 ↔ (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0))
4111recnd 9924 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℂ)
42 id 22 . . . . . . . . 9 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
43 cxpexp 24158 . . . . . . . . 9 (((log‘𝑥) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
4441, 42, 43syl2anr 493 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
45 rpcn 11675 . . . . . . . . . 10 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
4645adantl 480 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
4746cxp1d 24196 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → (𝑥𝑐1) = 𝑥)
4844, 47oveq12d 6544 . . . . . . 7 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1)) = (((log‘𝑥)↑𝑘) / 𝑥))
4948mpteq2dva 4666 . . . . . 6 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)))
50 nn0cn 11151 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
51 1rp 11670 . . . . . . 7 1 ∈ ℝ+
52 cxploglim2 24449 . . . . . . 7 ((𝑘 ∈ ℂ ∧ 1 ∈ ℝ+) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) ⇝𝑟 0)
5350, 51, 52sylancl 692 . . . . . 6 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) ⇝𝑟 0)
5449, 53eqbrtrrd 4601 . . . . 5 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
5540, 54vtoclga 3244 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0)
56 rerpdivcl 11695 . . . . . 6 ((((log‘𝑥)↑𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
5714, 56sylancom 697 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
5857recnd 9924 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
5910recnd 9924 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
6014recnd 9924 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℂ)
6135adantr 479 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
6227recnd 9924 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
6361, 62mulcld 9916 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
6460, 63subcld 10243 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
6559, 64subcld 10243 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
66 rpcnne0 11684 . . . . . . 7 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
6766adantl 480 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
6867simpld 473 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
6967simprd 477 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
7065, 68, 69divcld 10652 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
7170adantrr 748 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
7215adantr 479 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℕ)
7372nncnd 10885 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℂ)
7471, 73subcld 10243 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) ∈ ℂ)
7574abscld 13971 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ∈ ℝ)
7657adantrr 748 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
7776recnd 9924 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
7877abscld 13971 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥)↑𝑁) / 𝑥)) ∈ ℝ)
79 ioorp 12080 . . . . . . . . . 10 (0(,)+∞) = ℝ+
8079eqcomi 2618 . . . . . . . . 9 + = (0(,)+∞)
81 nnuz 11557 . . . . . . . . 9 ℕ = (ℤ‘1)
82 1z 11242 . . . . . . . . . 10 1 ∈ ℤ
8382a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℤ)
84 1red 9911 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ)
85 1re 9895 . . . . . . . . . . 11 1 ∈ ℝ
86 1nn0 11157 . . . . . . . . . . 11 1 ∈ ℕ0
8785, 86nn0addge1i 11190 . . . . . . . . . 10 1 ≤ (1 + 1)
8887a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ (1 + 1))
89 0red 9897 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ)
9072adantr 479 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
9190nnred 10884 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
92 rpre 11673 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
9392adantl 480 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
94 fzfid 12591 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (0...𝑁) ∈ Fin)
95 simprl 789 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
96 rpdivcl 11690 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
9795, 96sylan 486 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
9897relogcld 24117 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
99 reexpcl 12696 . . . . . . . . . . . . . 14 (((log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
10098, 20, 99syl2an 492 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
10120adantl 480 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
102101, 24syl 17 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
103100, 102nndivred 10918 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
10494, 103fsumrecl 14260 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
10593, 104remulcld 9926 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℝ)
10691, 105remulcld 9926 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) ∈ ℝ)
107 simpll 785 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑁 ∈ ℕ0)
10898, 107reexpcld 12844 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
109 nnrp 11676 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
110109, 108sylan2 489 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℕ) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
111 reelprrecn 9884 . . . . . . . . . . . 12 ℝ ∈ {ℝ, ℂ}
112111a1i 11 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ℝ ∈ {ℝ, ℂ})
113105recnd 9924 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℂ)
114108, 90nndivred 10918 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)) ∈ ℝ)
115 simpl 471 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
116 advlogexp 24145 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
11795, 115, 116syl2anc 690 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
118112, 113, 114, 117, 73dvmptcmul 23477 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))))
119108recnd 9924 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℂ)
12073adantr 479 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
12172nnne0d 10914 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ≠ 0)
122121adantr 479 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ≠ 0)
123119, 120, 122divcan2d 10654 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))) = ((log‘(𝑥 / 𝑦))↑𝑁))
124123mpteq2dva 4666 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
125118, 124eqtrd 2643 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
126 oveq2 6534 . . . . . . . . . . 11 (𝑦 = 𝑛 → (𝑥 / 𝑦) = (𝑥 / 𝑛))
127126fveq2d 6091 . . . . . . . . . 10 (𝑦 = 𝑛 → (log‘(𝑥 / 𝑦)) = (log‘(𝑥 / 𝑛)))
128127oveq1d 6541 . . . . . . . . 9 (𝑦 = 𝑛 → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘(𝑥 / 𝑛))↑𝑁))
12995rpxrd 11707 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ*)
130 simp1rl 1118 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑥 ∈ ℝ+)
131 simp2r 1080 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛 ∈ ℝ+)
132130, 131rpdivcld 11723 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑛) ∈ ℝ+)
133132relogcld 24117 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
134 simp2l 1079 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑦 ∈ ℝ+)
135130, 134rpdivcld 11723 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
136135relogcld 24117 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
137 simp1l 1077 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑁 ∈ ℕ0)
138 log1 24080 . . . . . . . . . . 11 (log‘1) = 0
139131rpcnd 11708 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛 ∈ ℂ)
140139mulid2d 9914 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 · 𝑛) = 𝑛)
141 simp33 1091 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛𝑥)
142140, 141eqbrtrd 4599 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 · 𝑛) ≤ 𝑥)
143 1red 9911 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 1 ∈ ℝ)
144130rpred 11706 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑥 ∈ ℝ)
145143, 144, 131lemuldivd 11755 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
146142, 145mpbid 220 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 1 ≤ (𝑥 / 𝑛))
147 logleb 24097 . . . . . . . . . . . . 13 ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
14851, 132, 147sylancr 693 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
149146, 148mpbid 220 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
150138, 149syl5eqbrr 4613 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 0 ≤ (log‘(𝑥 / 𝑛)))
151 simp32 1090 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑦𝑛)
152134, 131, 130lediv2d 11730 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑦𝑛 ↔ (𝑥 / 𝑛) ≤ (𝑥 / 𝑦)))
153151, 152mpbid 220 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑛) ≤ (𝑥 / 𝑦))
154132, 135logled 24121 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((𝑥 / 𝑛) ≤ (𝑥 / 𝑦) ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦))))
155153, 154mpbid 220 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))
156 leexp1a 12738 . . . . . . . . . 10 ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ (log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ (log‘(𝑥 / 𝑛)) ∧ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
157133, 136, 137, 150, 155, 156syl32anc 1325 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
158 eqid 2609 . . . . . . . . 9 (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))
159973ad2antr1 1218 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
160159relogcld 24117 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
161 simpll 785 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑁 ∈ ℕ0)
162 rpcn 11675 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
163162adantl 480 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℂ)
1641633ad2antr1 1218 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦 ∈ ℂ)
165164mulid2d 9914 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 · 𝑦) = 𝑦)
166 simpr3 1061 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦𝑥)
167165, 166eqbrtrd 4599 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 · 𝑦) ≤ 𝑥)
168 1red 9911 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 1 ∈ ℝ)
16995rpred 11706 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
170169adantr 479 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑥 ∈ ℝ)
171 simpr1 1059 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦 ∈ ℝ+)
172168, 170, 171lemuldivd 11755 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → ((1 · 𝑦) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑦)))
173167, 172mpbid 220 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 1 ≤ (𝑥 / 𝑦))
174 logleb 24097 . . . . . . . . . . . . 13 ((1 ∈ ℝ+ ∧ (𝑥 / 𝑦) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
17551, 159, 174sylancr 693 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
176173, 175mpbid 220 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑦)))
177138, 176syl5eqbrr 4613 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 0 ≤ (log‘(𝑥 / 𝑦)))
178160, 161, 177expge0d 12845 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
17951a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ+)
180 1le1 10506 . . . . . . . . . 10 1 ≤ 1
181180a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 1)
182 simprr 791 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
183169leidd 10445 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥𝑥)
18480, 81, 83, 84, 88, 89, 106, 108, 110, 125, 128, 129, 157, 158, 178, 179, 95, 181, 182, 183dvfsumlem4 23540 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) ≤ 1 / 𝑦((log‘(𝑥 / 𝑦))↑𝑁))
185 fzfid 12591 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
18695, 4, 5syl2an 492 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
187186relogcld 24117 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
188 simpll 785 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
189187, 188reexpcld 12844 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
190185, 189fsumrecl 14260 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
191190recnd 9924 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
19295rpcnd 11708 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ)
19373, 192mulcld 9916 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · 𝑥) ∈ ℂ)
19411ad2antrl 759 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
195194recnd 9924 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ)
196195, 115expcld 12827 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℂ)
197 fzfid 12591 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (0...𝑁) ∈ Fin)
198194, 20, 21syl2an 492 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
19920adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
200199, 24syl 17 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
201198, 200nndivred 10918 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
202201recnd 9924 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
203197, 202fsumcl 14259 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
20473, 203mulcld 9916 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
205196, 204subcld 10243 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
206191, 193, 205sub32d 10275 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
207 eqidd 2610 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))))
208 simpr 475 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
209208fveq2d 6091 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (⌊‘𝑦) = (⌊‘𝑥))
210209oveq2d 6542 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (1...(⌊‘𝑦)) = (1...(⌊‘𝑥)))
211210sumeq1d 14227 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁))
212 oveq2 6534 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (𝑥 / 𝑦) = (𝑥 / 𝑥))
21366ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
214 divid 10565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 𝑥) = 1)
216212, 215sylan9eqr 2665 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 / 𝑦) = 1)
217216adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 / 𝑦) = 1)
218217fveq2d 6091 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘1))
219218, 138syl6eq 2659 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = 0)
220219oveq1d 6541 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = (0↑𝑘))
221220oveq1d 6541 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = ((0↑𝑘) / (!‘𝑘)))
222221sumeq2dv 14229 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
223 nn0uz 11556 . . . . . . . . . . . . . . . . . . . . . . . 24 0 = (ℤ‘0)
224115, 223syl6eleq 2697 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ (ℤ‘0))
225 eluzfz1 12176 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘0) → 0 ∈ (0...𝑁))
226224, 225syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ (0...𝑁))
227226adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 0 ∈ (0...𝑁))
228227snssd 4280 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → {0} ⊆ (0...𝑁))
229 elsni 4141 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ {0} → 𝑘 = 0)
230229adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → 𝑘 = 0)
231 oveq2 6534 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 0 → (0↑𝑘) = (0↑0))
232 0exp0e1 12684 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0↑0) = 1
233231, 232syl6eq 2659 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 0 → (0↑𝑘) = 1)
234 fveq2 6087 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 0 → (!‘𝑘) = (!‘0))
235 fac0 12882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (!‘0) = 1
236234, 235syl6eq 2659 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 0 → (!‘𝑘) = 1)
237233, 236oveq12d 6544 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = (1 / 1))
238 1div1e1 10568 . . . . . . . . . . . . . . . . . . . . . . 23 (1 / 1) = 1
239237, 238syl6eq 2659 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = 1)
240230, 239syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) = 1)
241 ax-1cn 9850 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
242240, 241syl6eqel 2695 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) ∈ ℂ)
243 eldifi 3693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ∈ (0...𝑁))
244243adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (0...𝑁))
245244, 20syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ0)
246 eldifsni 4260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ≠ 0)
247246adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ≠ 0)
248 eldifsn 4259 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (ℕ0 ∖ {0}) ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
249245, 247, 248sylanbrc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (ℕ0 ∖ {0}))
250 dfn2 11154 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℕ0 ∖ {0})
251249, 250syl6eleqr 2698 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ)
2522510expd 12843 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0↑𝑘) = 0)
253252oveq1d 6541 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = (0 / (!‘𝑘)))
254245, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℕ)
255254nncnd 10885 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℂ)
256254nnne0d 10914 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ≠ 0)
257255, 256div0d 10651 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0 / (!‘𝑘)) = 0)
258253, 257eqtrd 2643 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = 0)
259 fzfid 12591 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (0...𝑁) ∈ Fin)
260228, 242, 258, 259fsumss 14251 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
261222, 260eqtr4d 2646 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)))
262 0cn 9888 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℂ
263239sumsn 14267 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1)
264262, 241, 263mp2an 703 . . . . . . . . . . . . . . . . . 18 Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1
265261, 264syl6eq 2659 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = 1)
266208, 265oveq12d 6544 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (𝑥 · 1))
267192mulid1d 9913 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥)
268267adantr 479 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 · 1) = 𝑥)
269266, 268eqtrd 2643 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = 𝑥)
270269oveq2d 6542 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · 𝑥))
271211, 270oveq12d 6544 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
272 ovex 6554 . . . . . . . . . . . . . 14 𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V
273272a1i 11 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V)
274207, 271, 95, 273fvmptd 6181 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
275 simpr 475 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → 𝑦 = 1)
276275fveq2d 6091 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = (⌊‘1))
277 flid 12428 . . . . . . . . . . . . . . . . . . 19 (1 ∈ ℤ → (⌊‘1) = 1)
27882, 277ax-mp 5 . . . . . . . . . . . . . . . . . 18 (⌊‘1) = 1
279276, 278syl6eq 2659 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = 1)
280279oveq2d 6542 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1...(⌊‘𝑦)) = (1...1))
281280sumeq1d 14227 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁))
282192div1d 10644 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 1) = 𝑥)
283282adantr 479 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 1) = 𝑥)
284283fveq2d 6091 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 1)) = (log‘𝑥))
285284oveq1d 6541 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) = ((log‘𝑥)↑𝑁))
286196adantr 479 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘𝑥)↑𝑁) ∈ ℂ)
287285, 286eqeltrd 2687 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ)
288 oveq2 6534 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑥 / 𝑛) = (𝑥 / 1))
289288fveq2d 6091 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (log‘(𝑥 / 𝑛)) = (log‘(𝑥 / 1)))
290289oveq1d 6541 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
291290fsum1 14268 . . . . . . . . . . . . . . . 16 ((1 ∈ ℤ ∧ ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
29282, 287, 291sylancr 693 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
293281, 292, 2853eqtrd 2647 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘𝑥)↑𝑁))
294275oveq2d 6542 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = (𝑥 / 1))
295294, 283eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = 𝑥)
296295fveq2d 6091 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
297296adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
298297oveq1d 6541 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = ((log‘𝑥)↑𝑘))
299298oveq1d 6541 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = (((log‘𝑥)↑𝑘) / (!‘𝑘)))
300299sumeq2dv 14229 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
301275, 300oveq12d 6544 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
302203adantr 479 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
303302mulid2d 9914 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
304301, 303eqtrd 2643 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
305304oveq2d 6542 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
306293, 305oveq12d 6544 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
307 ovex 6554 . . . . . . . . . . . . . 14 (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V
308307a1i 11 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V)
309207, 306, 179, 308fvmptd 6181 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
310274, 309oveq12d 6544 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
31171, 73, 192subdird 10338 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)))
31265adantrr 748 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
313213simprd 477 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0)
314312, 192, 313divcan1d 10653 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
315314oveq1d 6541 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
316311, 315eqtrd 2643 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
317206, 310, 3163eqtr4d 2653 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥))
318317fveq2d 6091 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)))
31974, 192absmuld 13989 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)))
320 rprege0 11681 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
321320ad2antrl 759 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
322 absid 13832 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
323321, 322syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥)
324323oveq2d 6542 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
325318, 319, 3243eqtrd 2647 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
326 1cnd 9912 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ)
327296oveq1d 6541 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
328326, 327csbied 3525 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 / 𝑦((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
329184, 325, 3283brtr3d 4608 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁))
33014adantrr 748 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℝ)
33175, 330, 95lemuldivd 11755 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁) ↔ (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥)))
332329, 331mpbid 220 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥))
33376leabsd 13949 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
33475, 76, 78, 332, 333letrd 10045 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
33558adantrr 748 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
336335subid1d 10232 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥)↑𝑁) / 𝑥) − 0) = (((log‘𝑥)↑𝑁) / 𝑥))
337336fveq2d 6091 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)) = (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
338334, 337breqtrrd 4605 . . . 4 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)))
33934, 35, 55, 58, 70, 338rlimsqzlem 14175 . . 3 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥)) ⇝𝑟 (!‘𝑁))
340 divsubdir 10572 . . . . . 6 ((((log‘𝑥)↑𝑁) ∈ ℂ ∧ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
34160, 63, 67, 340syl3anc 1317 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
342341mpteq2dva 4666 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))))
343 rerpdivcl 11695 . . . . . . 7 ((((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
34428, 343sylancom 697 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
345 divass 10554 . . . . . . . . . 10 (((!‘𝑁) ∈ ℂ ∧ Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
34661, 62, 67, 345syl3anc 1317 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
34726recnd 9924 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
34818, 68, 347, 69fsumdivc 14308 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))
34922recnd 9924 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℂ)
35025nnrpd 11704 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ+)
351350rpcnne0d 11715 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0))
35267adantr 479 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
353 divdiv32 10584 . . . . . . . . . . . . 13 ((((log‘𝑥)↑𝑘) ∈ ℂ ∧ ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
354349, 351, 352, 353syl3anc 1317 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
355354sumeq2dv 14229 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
356348, 355eqtrd 2643 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
357356oveq2d 6542 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
358346, 357eqtrd 2643 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
359358mpteq2dva 4666 . . . . . . 7 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))))
3602adantr 479 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℝ+)
36122, 360rerpdivcld 11737 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
362361, 25nndivred 10918 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
36318, 362fsumrecl 14260 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
364 rpssre 11677 . . . . . . . . . 10 + ⊆ ℝ
365 rlimconst 14071 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ (!‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
366364, 35, 365sylancr 693 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
367364a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → ℝ+ ⊆ ℝ)
368 fzfid 12591 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (0...𝑁) ∈ Fin)
369362anasss 676 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+𝑘 ∈ (0...𝑁))) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
370361an32s 841 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
37120adantl 480 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
372371, 24syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
373372nnred 10884 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ)
374373adantr 479 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ∈ ℝ)
375371, 54syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
376372nncnd 10885 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℂ)
377 rlimconst 14071 . . . . . . . . . . . . . 14 ((ℝ+ ⊆ ℝ ∧ (!‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
378364, 376, 377sylancr 693 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
379372nnne0d 10914 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0)
380379adantr 479 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ≠ 0)
381370, 374, 375, 378, 379, 380rlimdiv 14172 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 (0 / (!‘𝑘)))
382376, 379div0d 10651 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (0 / (!‘𝑘)) = 0)
383381, 382breqtrd 4603 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
384367, 368, 369, 383fsumrlim 14332 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 Σ𝑘 ∈ (0...𝑁)0)
385 fzfi 12590 . . . . . . . . . . . 12 (0...𝑁) ∈ Fin
386385olci 404 . . . . . . . . . . 11 ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin)
387 sumz 14248 . . . . . . . . . . 11 (((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin) → Σ𝑘 ∈ (0...𝑁)0 = 0)
388386, 387ax-mp 5 . . . . . . . . . 10 Σ𝑘 ∈ (0...𝑁)0 = 0
389384, 388syl6breq 4618 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
39017, 363, 366, 389rlimmul 14171 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 ((!‘𝑁) · 0))
39135mul01d 10086 . . . . . . . 8 (𝑁 ∈ ℕ0 → ((!‘𝑁) · 0) = 0)
392390, 391breqtrd 4603 . . . . . . 7 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 0)
393359, 392eqbrtrd 4599 . . . . . 6 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) ⇝𝑟 0)
39457, 344, 55, 393rlimsub 14170 . . . . 5 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 (0 − 0))
395 0m0e0 10979 . . . . 5 (0 − 0) = 0
396394, 395syl6breq 4618 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 0)
397342, 396eqbrtrd 4599 . . 3 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) ⇝𝑟 0)
39831, 33, 339, 397rlimadd 14169 . 2 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) ⇝𝑟 ((!‘𝑁) + 0))
399 divsubdir 10572 . . . . . 6 ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ ∧ (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
40059, 64, 67, 399syl3anc 1317 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
401400oveq1d 6541 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
40210, 2rerpdivcld 11737 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℝ)
403402recnd 9924 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℂ)
40433recnd 9924 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℂ)
405403, 404npcand 10247 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
406401, 405eqtrd 2643 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
407406mpteq2dva 4666 . 2 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)))
40835addid1d 10087 . 2 (𝑁 ∈ ℕ0 → ((!‘𝑁) + 0) = (!‘𝑁))
409398, 407, 4083brtr3d 4608 1 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  Vcvv 3172  csb 3498  cdif 3536  wss 3539  {csn 4124  {cpr 4126   class class class wbr 4577  cmpt 4637  cfv 5789  (class class class)co 6526  Fincfn 7818  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797  +∞cpnf 9927  cle 9931  cmin 10117   / cdiv 10535  cn 10869  0cn0 11141  cz 11212  cuz 11521  +crp 11666  (,)cioo 12004  ...cfz 12154  cfl 12410  cexp 12679  !cfa 12879  abscabs 13770  𝑟 crli 14012  Σcsu 14212   D cdv 23377  logclog 24049  𝑐ccxp 24050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-se 4987  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-isom 5798  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-4 10930  df-5 10931  df-6 10932  df-7 10933  df-8 10934  df-9 10935  df-n0 11142  df-z 11213  df-dec 11328  df-uz 11522  df-q 11623  df-rp 11667  df-xneg 11780  df-xadd 11781  df-xmul 11782  df-ioo 12008  df-ioc 12009  df-ico 12010  df-icc 12011  df-fz 12155  df-fzo 12292  df-fl 12412  df-mod 12488  df-seq 12621  df-exp 12680  df-fac 12880  df-bc 12909  df-hash 12937  df-shft 13603  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772  df-limsup 13998  df-clim 14015  df-rlim 14016  df-sum 14213  df-ef 14585  df-e 14586  df-sin 14587  df-cos 14588  df-pi 14590  df-struct 15645  df-ndx 15646  df-slot 15647  df-base 15648  df-sets 15649  df-ress 15650  df-plusg 15729  df-mulr 15730  df-starv 15731  df-sca 15732  df-vsca 15733  df-ip 15734  df-tset 15735  df-ple 15736  df-ds 15739  df-unif 15740  df-hom 15741  df-cco 15742  df-rest 15854  df-topn 15855  df-0g 15873  df-gsum 15874  df-topgen 15875  df-pt 15876  df-prds 15879  df-xrs 15933  df-qtop 15938  df-imas 15939  df-xps 15941  df-mre 16017  df-mrc 16018  df-acs 16020  df-mgm 17013  df-sgrp 17055  df-mnd 17066  df-submnd 17107  df-mulg 17312  df-cntz 17521  df-cmn 17966  df-psmet 19507  df-xmet 19508  df-met 19509  df-bl 19510  df-mopn 19511  df-fbas 19512  df-fg 19513  df-cnfld 19516  df-top 20468  df-bases 20469  df-topon 20470  df-topsp 20471  df-cld 20580  df-ntr 20581  df-cls 20582  df-nei 20659  df-lp 20697  df-perf 20698  df-cn 20788  df-cnp 20789  df-haus 20876  df-cmp 20947  df-tx 21122  df-hmeo 21315  df-fil 21407  df-fm 21499  df-flim 21500  df-flf 21501  df-xms 21882  df-ms 21883  df-tms 21884  df-cncf 22436  df-limc 23380  df-dv 23381  df-log 24051  df-cxp 24052
This theorem is referenced by:  logfacrlim2  24695  selberglem2  24979
  Copyright terms: Public domain W3C validator