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

Theorem logexprlim 25171
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 12987 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
2 simpr 479 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
3 elfznn 12584 . . . . . . . . . 10 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
43nnrpd 12084 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
5 rpdivcl 12070 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
62, 4, 5syl2an 495 . . . . . . . 8 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
76relogcld 24590 . . . . . . 7 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
8 simpll 807 . . . . . . 7 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
97, 8reexpcld 13240 . . . . . 6 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
101, 9fsumrecl 14685 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
11 relogcl 24543 . . . . . . 7 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
12 id 22 . . . . . . 7 (𝑁 ∈ ℕ0𝑁 ∈ ℕ0)
13 reexpcl 13092 . . . . . . 7 (((log‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℕ0) → ((log‘𝑥)↑𝑁) ∈ ℝ)
1411, 12, 13syl2anr 496 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℝ)
15 faccl 13285 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
1615adantr 472 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
1716nnred 11248 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
18 fzfid 12987 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (0...𝑁) ∈ Fin)
1911adantl 473 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
20 elfznn0 12647 . . . . . . . . . 10 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
21 reexpcl 13092 . . . . . . . . . 10 (((log‘𝑥) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑘) ∈ ℝ)
2219, 20, 21syl2an 495 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
2320adantl 473 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
24 faccl 13285 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
2523, 24syl 17 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
2622, 25nndivred 11282 . . . . . . . 8 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
2718, 26fsumrecl 14685 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
2817, 27remulcld 10283 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ)
2914, 28resubcld 10671 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ)
3010, 29resubcld 10671 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℝ)
3130, 2rerpdivcld 12117 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℝ)
32 rerpdivcl 12075 . . . 4 (((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
3329, 32sylancom 704 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ)
34 1red 10268 . . . 4 (𝑁 ∈ ℕ0 → 1 ∈ ℝ)
3515nncnd 11249 . . . 4 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℂ)
36 simpl 474 . . . . . . . . 9 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → 𝑘 = 𝑁)
3736oveq2d 6831 . . . . . . . 8 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑘) = ((log‘𝑥)↑𝑁))
3837oveq1d 6830 . . . . . . 7 ((𝑘 = 𝑁𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) = (((log‘𝑥)↑𝑁) / 𝑥))
3938mpteq2dva 4897 . . . . . 6 (𝑘 = 𝑁 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)))
4039breq1d 4815 . . . . 5 (𝑘 = 𝑁 → ((𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0 ↔ (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0))
4111recnd 10281 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℂ)
42 id 22 . . . . . . . . 9 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
43 cxpexp 24635 . . . . . . . . 9 (((log‘𝑥) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
4441, 42, 43syl2anr 496 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘))
45 rpcn 12055 . . . . . . . . . 10 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
4645adantl 473 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
4746cxp1d 24673 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → (𝑥𝑐1) = 𝑥)
4844, 47oveq12d 6833 . . . . . . 7 ((𝑘 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1)) = (((log‘𝑥)↑𝑘) / 𝑥))
4948mpteq2dva 4897 . . . . . 6 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) = (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)))
50 nn0cn 11515 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
51 1rp 12050 . . . . . . 7 1 ∈ ℝ+
52 cxploglim2 24926 . . . . . . 7 ((𝑘 ∈ ℂ ∧ 1 ∈ ℝ+) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) ⇝𝑟 0)
5350, 51, 52sylancl 697 . . . . . 6 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥𝑐1))) ⇝𝑟 0)
5449, 53eqbrtrrd 4829 . . . . 5 (𝑘 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
5540, 54vtoclga 3413 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟 0)
56 rerpdivcl 12075 . . . . . 6 ((((log‘𝑥)↑𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
5714, 56sylancom 704 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
5857recnd 10281 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
5910recnd 10281 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
6014recnd 10281 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℂ)
6135adantr 472 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
6227recnd 10281 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
6361, 62mulcld 10273 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
6460, 63subcld 10605 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
6559, 64subcld 10605 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
66 rpcnne0 12064 . . . . . . 7 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
6766adantl 473 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
6867simpld 477 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
6967simprd 482 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
7065, 68, 69divcld 11014 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
7170adantrr 755 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ)
7215adantr 472 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℕ)
7372nncnd 11249 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℂ)
7471, 73subcld 10605 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) ∈ ℂ)
7574abscld 14395 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ∈ ℝ)
7657adantrr 755 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ)
7776recnd 10281 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
7877abscld 14395 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥)↑𝑁) / 𝑥)) ∈ ℝ)
79 ioorp 12465 . . . . . . . . . 10 (0(,)+∞) = ℝ+
8079eqcomi 2770 . . . . . . . . 9 + = (0(,)+∞)
81 nnuz 11937 . . . . . . . . 9 ℕ = (ℤ‘1)
82 1z 11620 . . . . . . . . . 10 1 ∈ ℤ
8382a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℤ)
84 1red 10268 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ)
85 1re 10252 . . . . . . . . . . 11 1 ∈ ℝ
86 1nn0 11521 . . . . . . . . . . 11 1 ∈ ℕ0
8785, 86nn0addge1i 11554 . . . . . . . . . 10 1 ≤ (1 + 1)
8887a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ (1 + 1))
89 0red 10254 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ)
9072adantr 472 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
9190nnred 11248 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℝ)
92 rpre 12053 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
9392adantl 473 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
94 fzfid 12987 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (0...𝑁) ∈ Fin)
95 simprl 811 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
96 rpdivcl 12070 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
9795, 96sylan 489 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈ ℝ+)
9897relogcld 24590 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
99 reexpcl 13092 . . . . . . . . . . . . . 14 (((log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
10098, 20, 99syl2an 495 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ)
10120adantl 473 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
102101, 24syl 17 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
103100, 102nndivred 11282 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
10494, 103fsumrecl 14685 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ)
10593, 104remulcld 10283 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℝ)
10691, 105remulcld 10283 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) ∈ ℝ)
107 simpll 807 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑁 ∈ ℕ0)
10898, 107reexpcld 13240 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
109 nnrp 12056 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
110109, 108sylan2 492 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℕ) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ)
111 reelprrecn 10241 . . . . . . . . . . . 12 ℝ ∈ {ℝ, ℂ}
112111a1i 11 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ℝ ∈ {ℝ, ℂ})
113105recnd 10281 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℂ)
114108, 90nndivred 11282 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)) ∈ ℝ)
115 simpl 474 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ ℕ0)
116 advlogexp 24622 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
11795, 115, 116syl2anc 696 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦ (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))
118112, 113, 114, 117, 73dvmptcmul 23947 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))))
119108recnd 10281 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℂ)
12073adantr 472 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
12172nnne0d 11278 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ≠ 0)
122121adantr 472 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (!‘𝑁) ≠ 0)
123119, 120, 122divcan2d 11016 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))) = ((log‘(𝑥 / 𝑦))↑𝑁))
124123mpteq2dva 4897 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
125118, 124eqtrd 2795 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ ((log‘(𝑥 / 𝑦))↑𝑁)))
126 oveq2 6823 . . . . . . . . . . 11 (𝑦 = 𝑛 → (𝑥 / 𝑦) = (𝑥 / 𝑛))
127126fveq2d 6358 . . . . . . . . . 10 (𝑦 = 𝑛 → (log‘(𝑥 / 𝑦)) = (log‘(𝑥 / 𝑛)))
128127oveq1d 6830 . . . . . . . . 9 (𝑦 = 𝑛 → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘(𝑥 / 𝑛))↑𝑁))
12995rpxrd 12087 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ*)
130 simp1rl 1305 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑥 ∈ ℝ+)
131 simp2r 1243 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛 ∈ ℝ+)
132130, 131rpdivcld 12103 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑛) ∈ ℝ+)
133132relogcld 24590 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
134 simp2l 1242 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑦 ∈ ℝ+)
135130, 134rpdivcld 12103 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
136135relogcld 24590 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
137 simp1l 1240 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑁 ∈ ℕ0)
138 log1 24553 . . . . . . . . . . 11 (log‘1) = 0
139131rpcnd 12088 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛 ∈ ℂ)
140139mulid2d 10271 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 · 𝑛) = 𝑛)
141 simp33 1254 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑛𝑥)
142140, 141eqbrtrd 4827 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 · 𝑛) ≤ 𝑥)
143 1red 10268 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 1 ∈ ℝ)
144130rpred 12086 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑥 ∈ ℝ)
145143, 144, 131lemuldivd 12135 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
146142, 145mpbid 222 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 1 ≤ (𝑥 / 𝑛))
147 logleb 24570 . . . . . . . . . . . . 13 ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
14851, 132, 147sylancr 698 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
149146, 148mpbid 222 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
150138, 149syl5eqbrr 4841 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 0 ≤ (log‘(𝑥 / 𝑛)))
151 simp32 1253 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → 𝑦𝑛)
152134, 131, 130lediv2d 12110 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑦𝑛 ↔ (𝑥 / 𝑛) ≤ (𝑥 / 𝑦)))
153151, 152mpbid 222 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (𝑥 / 𝑛) ≤ (𝑥 / 𝑦))
154132, 135logled 24594 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((𝑥 / 𝑛) ≤ (𝑥 / 𝑦) ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦))))
155153, 154mpbid 222 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))
156 leexp1a 13134 . . . . . . . . . 10 ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ (log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ (log‘(𝑥 / 𝑛)) ∧ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
157133, 136, 137, 150, 155, 156syl32anc 1485 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑦𝑦𝑛𝑛𝑥)) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
158 eqid 2761 . . . . . . . . 9 (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))
159973ad2antr1 1204 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (𝑥 / 𝑦) ∈ ℝ+)
160159relogcld 24590 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ)
161 simpll 807 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑁 ∈ ℕ0)
162 rpcn 12055 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
163162adantl 473 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℂ)
1641633ad2antr1 1204 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦 ∈ ℂ)
165164mulid2d 10271 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 · 𝑦) = 𝑦)
166 simpr3 1238 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦𝑥)
167165, 166eqbrtrd 4827 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 · 𝑦) ≤ 𝑥)
168 1red 10268 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 1 ∈ ℝ)
16995rpred 12086 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
170169adantr 472 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑥 ∈ ℝ)
171 simpr1 1234 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 𝑦 ∈ ℝ+)
172168, 170, 171lemuldivd 12135 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → ((1 · 𝑦) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑦)))
173167, 172mpbid 222 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 1 ≤ (𝑥 / 𝑦))
174 logleb 24570 . . . . . . . . . . . . 13 ((1 ∈ ℝ+ ∧ (𝑥 / 𝑦) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
17551, 159, 174sylancr 698 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦))))
176173, 175mpbid 222 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → (log‘1) ≤ (log‘(𝑥 / 𝑦)))
177138, 176syl5eqbrr 4841 . . . . . . . . . 10 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 0 ≤ (log‘(𝑥 / 𝑦)))
178160, 161, 177expge0d 13241 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦𝑦𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑦))↑𝑁))
17951a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ+)
180 1le1 10868 . . . . . . . . . 10 1 ≤ 1
181180a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 1)
182 simprr 813 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
183169leidd 10807 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥𝑥)
18480, 81, 83, 84, 88, 89, 106, 108, 110, 125, 128, 129, 157, 158, 178, 179, 95, 181, 182, 183dvfsumlem4 24012 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) ≤ 1 / 𝑦((log‘(𝑥 / 𝑦))↑𝑁))
185 fzfid 12987 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
18695, 4, 5syl2an 495 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
187186relogcld 24590 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
188 simpll 807 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ0)
189187, 188reexpcld 13240 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
190185, 189fsumrecl 14685 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ)
191190recnd 10281 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ)
19295rpcnd 12088 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ)
19373, 192mulcld 10273 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · 𝑥) ∈ ℂ)
19411ad2antrl 766 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
195194recnd 10281 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ)
196195, 115expcld 13223 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℂ)
197 fzfid 12987 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (0...𝑁) ∈ Fin)
198194, 20, 21syl2an 495 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ)
19920adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
200199, 24syl 17 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
201198, 200nndivred 11282 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ)
202201recnd 10281 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
203197, 202fsumcl 14684 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
20473, 203mulcld 10273 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ)
205196, 204subcld 10605 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ)
206191, 193, 205sub32d 10637 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
207 eqidd 2762 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))))
208 simpr 479 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
209208fveq2d 6358 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (⌊‘𝑦) = (⌊‘𝑥))
210209oveq2d 6831 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (1...(⌊‘𝑦)) = (1...(⌊‘𝑥)))
211210sumeq1d 14651 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁))
212 oveq2 6823 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (𝑥 / 𝑦) = (𝑥 / 𝑥))
21366ad2antrl 766 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
214 divid 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 𝑥) = 1)
216212, 215sylan9eqr 2817 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 / 𝑦) = 1)
217216adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 / 𝑦) = 1)
218217fveq2d 6358 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘1))
219218, 138syl6eq 2811 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = 0)
220219oveq1d 6830 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = (0↑𝑘))
221220oveq1d 6830 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = ((0↑𝑘) / (!‘𝑘)))
222221sumeq2dv 14653 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
223 nn0uz 11936 . . . . . . . . . . . . . . . . . . . . . . . 24 0 = (ℤ‘0)
224115, 223syl6eleq 2850 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈ (ℤ‘0))
225 eluzfz1 12562 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘0) → 0 ∈ (0...𝑁))
226224, 225syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ (0...𝑁))
227226adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 0 ∈ (0...𝑁))
228227snssd 4486 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → {0} ⊆ (0...𝑁))
229 elsni 4339 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ {0} → 𝑘 = 0)
230229adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → 𝑘 = 0)
231 oveq2 6823 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 0 → (0↑𝑘) = (0↑0))
232 0exp0e1 13080 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0↑0) = 1
233231, 232syl6eq 2811 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 0 → (0↑𝑘) = 1)
234 fveq2 6354 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 0 → (!‘𝑘) = (!‘0))
235 fac0 13278 . . . . . . . . . . . . . . . . . . . . . . . . 25 (!‘0) = 1
236234, 235syl6eq 2811 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 0 → (!‘𝑘) = 1)
237233, 236oveq12d 6833 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = (1 / 1))
238 1div1e1 10930 . . . . . . . . . . . . . . . . . . . . . . 23 (1 / 1) = 1
239237, 238syl6eq 2811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = 1)
240230, 239syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) = 1)
241 ax-1cn 10207 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
242240, 241syl6eqel 2848 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) ∈ ℂ)
243 eldifi 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ∈ (0...𝑁))
244243adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (0...𝑁))
245244, 20syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ0)
246 eldifsni 4467 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ≠ 0)
247246adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ≠ 0)
248 eldifsn 4463 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (ℕ0 ∖ {0}) ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
249245, 247, 248sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (ℕ0 ∖ {0}))
250 dfn2 11518 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℕ0 ∖ {0})
251249, 250syl6eleqr 2851 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ)
2522510expd 13239 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0↑𝑘) = 0)
253252oveq1d 6830 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = (0 / (!‘𝑘)))
254245, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℕ)
255254nncnd 11249 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈ ℂ)
256254nnne0d 11278 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ≠ 0)
257255, 256div0d 11013 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0 / (!‘𝑘)) = 0)
258253, 257eqtrd 2795 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = 0)
259 fzfid 12987 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (0...𝑁) ∈ Fin)
260228, 242, 258, 259fsumss 14676 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘)))
261222, 260eqtr4d 2798 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)))
262 0cn 10245 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℂ
263239sumsn 14695 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1)
264262, 241, 263mp2an 710 . . . . . . . . . . . . . . . . . 18 Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1
265261, 264syl6eq 2811 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = 1)
266208, 265oveq12d 6833 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (𝑥 · 1))
267192mulid1d 10270 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥)
268267adantr 472 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 · 1) = 𝑥)
269266, 268eqtrd 2795 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = 𝑥)
270269oveq2d 6831 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · 𝑥))
271211, 270oveq12d 6833 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
272 ovexd 6845 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V)
273207, 271, 95, 272fvmptd 6452 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)))
274 simpr 479 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → 𝑦 = 1)
275274fveq2d 6358 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = (⌊‘1))
276 flid 12824 . . . . . . . . . . . . . . . . . . 19 (1 ∈ ℤ → (⌊‘1) = 1)
27782, 276ax-mp 5 . . . . . . . . . . . . . . . . . 18 (⌊‘1) = 1
278275, 277syl6eq 2811 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = 1)
279278oveq2d 6831 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1...(⌊‘𝑦)) = (1...1))
280279sumeq1d 14651 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁))
281192div1d 11006 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 1) = 𝑥)
282281adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 1) = 𝑥)
283282fveq2d 6358 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 1)) = (log‘𝑥))
284283oveq1d 6830 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) = ((log‘𝑥)↑𝑁))
285196adantr 472 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘𝑥)↑𝑁) ∈ ℂ)
286284, 285eqeltrd 2840 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ)
287 oveq2 6823 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑥 / 𝑛) = (𝑥 / 1))
288287fveq2d 6358 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (log‘(𝑥 / 𝑛)) = (log‘(𝑥 / 1)))
289288oveq1d 6830 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
290289fsum1 14696 . . . . . . . . . . . . . . . 16 ((1 ∈ ℤ ∧ ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
29182, 286, 290sylancr 698 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁))
292280, 291, 2843eqtrd 2799 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘𝑥)↑𝑁))
293274oveq2d 6831 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = (𝑥 / 1))
294293, 282eqtrd 2795 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = 𝑥)
295294fveq2d 6358 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
296295adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘𝑥))
297296oveq1d 6830 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = ((log‘𝑥)↑𝑘))
298297oveq1d 6830 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = (((log‘𝑥)↑𝑘) / (!‘𝑘)))
299298sumeq2dv 14653 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
300274, 299oveq12d 6833 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
301203adantr 472 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
302301mulid2d 10271 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
303300, 302eqtrd 2795 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))
304303oveq2d 6831 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))
305292, 304oveq12d 6833 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
306 ovexd 6845 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V)
307207, 305, 179, 306fvmptd 6452 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))
308273, 307oveq12d 6833 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
30971, 73, 192subdird 10700 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)))
31065adantrr 755 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ)
311213simprd 482 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0)
312310, 192, 311divcan1d 11015 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))))
313312oveq1d 6830 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
314309, 313eqtrd 2795 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥)))
315206, 308, 3143eqtr4d 2805 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥))
316315fveq2d 6358 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)))
31774, 192absmuld 14413 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)))
318 rprege0 12061 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
319318ad2antrl 766 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
320 absid 14256 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
321319, 320syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥)
322321oveq2d 6831 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
323316, 317, 3223eqtrd 2799 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥))
324 1cnd 10269 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ)
325295oveq1d 6830 . . . . . . . . 9 (((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
326324, 325csbied 3702 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 / 𝑦((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁))
327184, 323, 3263brtr3d 4836 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁))
32814adantrr 755 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℝ)
32975, 328, 95lemuldivd 12135 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁) ↔ (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥)))
330327, 329mpbid 222 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥))
33176leabsd 14373 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
33275, 76, 78, 330, 331letrd 10407 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
33358adantrr 755 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ)
334333subid1d 10594 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥)↑𝑁) / 𝑥) − 0) = (((log‘𝑥)↑𝑁) / 𝑥))
335334fveq2d 6358 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)) = (abs‘(((log‘𝑥)↑𝑁) / 𝑥)))
336332, 335breqtrrd 4833 . . . 4 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)))
33734, 35, 55, 58, 70, 336rlimsqzlem 14599 . . 3 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥)) ⇝𝑟 (!‘𝑁))
338 divsubdir 10934 . . . . . 6 ((((log‘𝑥)↑𝑁) ∈ ℂ ∧ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
33960, 63, 67, 338syl3anc 1477 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))
340339mpteq2dva 4897 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))))
341 rerpdivcl 12075 . . . . . . 7 ((((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
34228, 341sylancom 704 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ)
343 divass 10916 . . . . . . . . . 10 (((!‘𝑁) ∈ ℂ ∧ Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
34461, 62, 67, 343syl3anc 1477 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)))
34526recnd 10281 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ)
34618, 68, 345, 69fsumdivc 14738 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))
34722recnd 10281 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℂ)
34825nnrpd 12084 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ+)
349348rpcnne0d 12095 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0))
35067adantr 472 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
351 divdiv32 10946 . . . . . . . . . . . . 13 ((((log‘𝑥)↑𝑘) ∈ ℂ ∧ ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
352347, 349, 350, 351syl3anc 1477 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
353352sumeq2dv 14653 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
354346, 353eqtrd 2795 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))
355354oveq2d 6831 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
356344, 355eqtrd 2795 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))
357356mpteq2dva 4897 . . . . . . 7 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))))
3582adantr 472 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℝ+)
35922, 358rerpdivcld 12117 . . . . . . . . . . 11 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
360359, 25nndivred 11282 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
36118, 360fsumrecl 14685 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
362 rpssre 12057 . . . . . . . . . 10 + ⊆ ℝ
363 rlimconst 14495 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ (!‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
364362, 35, 363sylancr 698 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (!‘𝑁)) ⇝𝑟 (!‘𝑁))
365362a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → ℝ+ ⊆ ℝ)
366 fzfid 12987 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (0...𝑁) ∈ Fin)
367360anasss 682 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ ℝ+𝑘 ∈ (0...𝑁))) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ)
368359an32s 881 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ)
36920adantl 473 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
370369, 24syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
371370nnred 11248 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℝ)
372371adantr 472 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ∈ ℝ)
373369, 54syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0)
374370nncnd 11249 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℂ)
375 rlimconst 14495 . . . . . . . . . . . . . 14 ((ℝ+ ⊆ ℝ ∧ (!‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
376362, 374, 375sylancr 698 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ (!‘𝑘)) ⇝𝑟 (!‘𝑘))
377370nnne0d 11278 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0)
378377adantr 472 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) → (!‘𝑘) ≠ 0)
379368, 372, 373, 376, 377, 378rlimdiv 14596 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 (0 / (!‘𝑘)))
380374, 377div0d 11013 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (0 / (!‘𝑘)) = 0)
381379, 380breqtrd 4831 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
382365, 366, 367, 381fsumrlim 14763 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 Σ𝑘 ∈ (0...𝑁)0)
383 fzfi 12986 . . . . . . . . . . . 12 (0...𝑁) ∈ Fin
384383olci 405 . . . . . . . . . . 11 ((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin)
385 sumz 14673 . . . . . . . . . . 11 (((0...𝑁) ⊆ (ℤ‘0) ∨ (0...𝑁) ∈ Fin) → Σ𝑘 ∈ (0...𝑁)0 = 0)
386384, 385ax-mp 5 . . . . . . . . . 10 Σ𝑘 ∈ (0...𝑁)0 = 0
387382, 386syl6breq 4846 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 0)
38817, 361, 364, 387rlimmul 14595 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 ((!‘𝑁) · 0))
38935mul01d 10448 . . . . . . . 8 (𝑁 ∈ ℕ0 → ((!‘𝑁) · 0) = 0)
390388, 389breqtrd 4831 . . . . . . 7 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟 0)
391357, 390eqbrtrd 4827 . . . . . 6 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) ⇝𝑟 0)
39257, 342, 55, 391rlimsub 14594 . . . . 5 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 (0 − 0))
393 0m0e0 11343 . . . . 5 (0 − 0) = 0
394392, 393syl6breq 4846 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 0)
395340, 394eqbrtrd 4827 . . 3 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) ⇝𝑟 0)
39631, 33, 337, 395rlimadd 14593 . 2 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) ⇝𝑟 ((!‘𝑁) + 0))
397 divsubdir 10934 . . . . . 6 ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ ∧ (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
39859, 64, 67, 397syl3anc 1477 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
399398oveq1d 6830 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)))
40010, 2rerpdivcld 12117 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℝ)
401400recnd 10281 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℂ)
40233recnd 10281 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℂ)
403401, 402npcand 10609 . . . 4 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
404399, 403eqtrd 2795 . . 3 ((𝑁 ∈ ℕ0𝑥 ∈ ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))
405404mpteq2dva 4897 . 2 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)))
40635addid1d 10449 . 2 (𝑁 ∈ ℕ0 → ((!‘𝑁) + 0) = (!‘𝑁))
407396, 405, 4063brtr3d 4836 1 (𝑁 ∈ ℕ0 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wcel 2140  wne 2933  Vcvv 3341  csb 3675  cdif 3713  wss 3716  {csn 4322  {cpr 4324   class class class wbr 4805  cmpt 4882  cfv 6050  (class class class)co 6815  Fincfn 8124  cc 10147  cr 10148  0cc0 10149  1c1 10150   + caddc 10152   · cmul 10154  +∞cpnf 10284  cle 10288  cmin 10479   / cdiv 10897  cn 11233  0cn0 11505  cz 11590  cuz 11900  +crp 12046  (,)cioo 12389  ...cfz 12540  cfl 12806  cexp 13075  !cfa 13275  abscabs 14194  𝑟 crli 14436  Σcsu 14636   D cdv 23847  logclog 24522  𝑐ccxp 24523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-inf2 8714  ax-cnex 10205  ax-resscn 10206  ax-1cn 10207  ax-icn 10208  ax-addcl 10209  ax-addrcl 10210  ax-mulcl 10211  ax-mulrcl 10212  ax-mulcom 10213  ax-addass 10214  ax-mulass 10215  ax-distr 10216  ax-i2m1 10217  ax-1ne0 10218  ax-1rid 10219  ax-rnegex 10220  ax-rrecex 10221  ax-cnre 10222  ax-pre-lttri 10223  ax-pre-lttrn 10224  ax-pre-ltadd 10225  ax-pre-mulgt0 10226  ax-pre-sup 10227  ax-addf 10228  ax-mulf 10229
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-int 4629  df-iun 4675  df-iin 4676  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-se 5227  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-isom 6059  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-of 7064  df-om 7233  df-1st 7335  df-2nd 7336  df-supp 7466  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-1o 7731  df-2o 7732  df-oadd 7735  df-er 7914  df-map 8028  df-pm 8029  df-ixp 8078  df-en 8125  df-dom 8126  df-sdom 8127  df-fin 8128  df-fsupp 8444  df-fi 8485  df-sup 8516  df-inf 8517  df-oi 8583  df-card 8976  df-cda 9203  df-pnf 10289  df-mnf 10290  df-xr 10291  df-ltxr 10292  df-le 10293  df-sub 10481  df-neg 10482  df-div 10898  df-nn 11234  df-2 11292  df-3 11293  df-4 11294  df-5 11295  df-6 11296  df-7 11297  df-8 11298  df-9 11299  df-n0 11506  df-z 11591  df-dec 11707  df-uz 11901  df-q 12003  df-rp 12047  df-xneg 12160  df-xadd 12161  df-xmul 12162  df-ioo 12393  df-ioc 12394  df-ico 12395  df-icc 12396  df-fz 12541  df-fzo 12681  df-fl 12808  df-mod 12884  df-seq 13017  df-exp 13076  df-fac 13276  df-bc 13305  df-hash 13333  df-shft 14027  df-cj 14059  df-re 14060  df-im 14061  df-sqrt 14195  df-abs 14196  df-limsup 14422  df-clim 14439  df-rlim 14440  df-sum 14637  df-ef 15018  df-e 15019  df-sin 15020  df-cos 15021  df-pi 15023  df-struct 16082  df-ndx 16083  df-slot 16084  df-base 16086  df-sets 16087  df-ress 16088  df-plusg 16177  df-mulr 16178  df-starv 16179  df-sca 16180  df-vsca 16181  df-ip 16182  df-tset 16183  df-ple 16184  df-ds 16187  df-unif 16188  df-hom 16189  df-cco 16190  df-rest 16306  df-topn 16307  df-0g 16325  df-gsum 16326  df-topgen 16327  df-pt 16328  df-prds 16331  df-xrs 16385  df-qtop 16390  df-imas 16391  df-xps 16393  df-mre 16469  df-mrc 16470  df-acs 16472  df-mgm 17464  df-sgrp 17506  df-mnd 17517  df-submnd 17558  df-mulg 17763  df-cntz 17971  df-cmn 18416  df-psmet 19961  df-xmet 19962  df-met 19963  df-bl 19964  df-mopn 19965  df-fbas 19966  df-fg 19967  df-cnfld 19970  df-top 20922  df-topon 20939  df-topsp 20960  df-bases 20973  df-cld 21046  df-ntr 21047  df-cls 21048  df-nei 21125  df-lp 21163  df-perf 21164  df-cn 21254  df-cnp 21255  df-haus 21342  df-cmp 21413  df-tx 21588  df-hmeo 21781  df-fil 21872  df-fm 21964  df-flim 21965  df-flf 21966  df-xms 22347  df-ms 22348  df-tms 22349  df-cncf 22903  df-limc 23850  df-dv 23851  df-log 24524  df-cxp 24525
This theorem is referenced by:  logfacrlim2  25172  selberglem2  25456
  Copyright terms: Public domain W3C validator