Metamath Proof Explorer

Theorem logexprlim

Description: The sum sum_ n <_ x , log ^ N ( x / n ) has the asymptotic expansion ( N ! ) x + o ( x ) . (More precisely, the omitted term has order O ( log ^ N ( x ) / x ) .) (Contributed by Mario Carneiro, 22-May-2016)

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

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
2 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
3 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
4 3 nnrpd ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
5 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
6 2 4 5 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
7 6 relogcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
8 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ0 )
9 7 8 reexpcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ∈ ℝ )
10 1 9 fsumrecl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ∈ ℝ )
11 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
12 id ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
13 reexpcl ⊢ ( ( ( log ‘ 𝑥 ) ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℝ )
14 11 12 13 syl2anr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℝ )
15 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
16 15 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ! ‘ 𝑁 ) ∈ ℕ )
17 16 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ! ‘ 𝑁 ) ∈ ℝ )
18 fzfid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( 0 ... 𝑁 ) ∈ Fin )
19 11 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
20 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
21 reexpcl ⊢ ( ( ( log ‘ 𝑥 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( log ‘ 𝑥 ) ↑ 𝑘 ) ∈ ℝ )
22 19 20 21 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( log ‘ 𝑥 ) ↑ 𝑘 ) ∈ ℝ )
23 20 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
24 23 faccld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
25 22 24 nndivred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
26 18 25 fsumrecl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
27 17 26 remulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℝ )
28 14 27 resubcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ∈ ℝ )
29 10 28 resubcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ∈ ℝ )
30 29 2 rerpdivcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) ∈ ℝ )
31 rerpdivcl ⊢ ( ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ∈ ℝ )
32 28 31 sylancom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ∈ ℝ )
33 1red ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ )
34 15 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℂ )
35 simpl ⊢ ( ( 𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+ ) → 𝑘 = 𝑁 )
36 35 oveq2d ⊢ ( ( 𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) ↑ 𝑘 ) = ( ( log ‘ 𝑥 ) ↑ 𝑁 ) )
37 36 oveq1d ⊢ ( ( 𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) = ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) )
38 37 mpteq2dva ⊢ ( 𝑘 = 𝑁 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ) )
39 38 breq1d ⊢ ( 𝑘 = 𝑁 → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) ) ⇝𝑟 0 ↔ ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ) ⇝𝑟 0 ) )
40 11 recnd ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℂ )
41 id ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℕ0 )
42 cxpexp ⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( log ‘ 𝑥 ) ↑𝑐 𝑘 ) = ( ( log ‘ 𝑥 ) ↑ 𝑘 ) )
43 40 41 42 syl2anr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) ↑𝑐 𝑘 ) = ( ( log ‘ 𝑥 ) ↑ 𝑘 ) )
44 rpcn ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
45 44 adantl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
46 45 cxp1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 1 ) = 𝑥 )
47 43 46 oveq12d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) ↑𝑐 𝑘 ) / ( 𝑥 ↑𝑐 1 ) ) = ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) )
48 47 mpteq2dva ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑𝑐 𝑘 ) / ( 𝑥 ↑𝑐 1 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) ) )
49 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
50 1rp ⊢ 1 ∈ ℝ+
51 cxploglim2 ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑𝑐 𝑘 ) / ( 𝑥 ↑𝑐 1 ) ) ) ⇝𝑟 0 )
52 49 50 51 sylancl ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑𝑐 𝑘 ) / ( 𝑥 ↑𝑐 1 ) ) ) ⇝𝑟 0 )
53 48 52 eqbrtrrd ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) ) ⇝𝑟 0 )
54 39 53 vtoclga ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ) ⇝𝑟 0 )
55 rerpdivcl ⊢ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ∈ ℝ )
56 14 55 sylancom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ∈ ℝ )
57 56 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ∈ ℂ )
58 10 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ∈ ℂ )
59 14 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℂ )
60 34 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ! ‘ 𝑁 ) ∈ ℂ )
61 26 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
62 60 61 mulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℂ )
63 59 62 subcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ∈ ℂ )
64 58 63 subcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ∈ ℂ )
65 rpcnne0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
66 65 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
67 66 simpld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
68 66 simprd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
69 64 67 68 divcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) ∈ ℂ )
70 69 adantrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) ∈ ℂ )
71 15 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ! ‘ 𝑁 ) ∈ ℕ )
72 71 nncnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
73 70 72 subcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ∈ ℂ )
74 73 abscld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) ∈ ℝ )
75 56 adantrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ∈ ℝ )
76 75 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ∈ ℂ )
77 76 abscld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ) ∈ ℝ )
78 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
79 78 eqcomi ⊢ ℝ+ = ( 0 (,) +∞ )
80 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
81 1z ⊢ 1 ∈ ℤ
82 81 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℤ )
83 1red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℝ )
84 1re ⊢ 1 ∈ ℝ
85 1nn0 ⊢ 1 ∈ ℕ0
86 84 85 nn0addge1i ⊢ 1 ≤ ( 1 + 1 )
87 86 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ ( 1 + 1 ) )
88 0red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ∈ ℝ )
89 71 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ! ‘ 𝑁 ) ∈ ℕ )
90 89 nnred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ! ‘ 𝑁 ) ∈ ℝ )
91 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
92 91 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
93 fzfid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 0 ... 𝑁 ) ∈ Fin )
94 simprl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
95 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 / 𝑦 ) ∈ ℝ+ )
96 94 95 sylan ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 / 𝑦 ) ∈ ℝ+ )
97 96 relogcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( log ‘ ( 𝑥 / 𝑦 ) ) ∈ ℝ )
98 reexpcl ⊢ ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) ∈ ℝ )
99 97 20 98 syl2an ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) ∈ ℝ )
100 20 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
101 100 faccld ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
102 99 101 nndivred ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
103 93 102 fsumrecl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
104 92 103 remulcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℝ )
105 90 104 remulcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ∈ ℝ )
106 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑁 ∈ ℕ0 )
107 97 106 reexpcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) ∈ ℝ )
108 nnrp ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ+ )
109 108 107 sylan2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) ∈ ℝ )
110 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
111 110 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ℝ ∈ { ℝ , ℂ } )
112 104 recnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℂ )
113 107 89 nndivred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ∈ ℝ )
114 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑁 ∈ ℕ0 )
115 advlogexp ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) )
116 94 114 115 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) )
117 111 112 113 116 72 dvmptcmul ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( ! ‘ 𝑁 ) · ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) ) )
118 107 recnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) ∈ ℂ )
119 72 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ! ‘ 𝑁 ) ∈ ℂ )
120 71 nnne0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ! ‘ 𝑁 ) ≠ 0 )
121 120 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ! ‘ 𝑁 ) ≠ 0 )
122 118 119 121 divcan2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) · ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) = ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) )
123 122 mpteq2dva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑦 ∈ ℝ+ ↦ ( ( ! ‘ 𝑁 ) · ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) ) )
124 117 123 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) ) )
125 oveq2 ⊢ ( 𝑦 = 𝑛 → ( 𝑥 / 𝑦 ) = ( 𝑥 / 𝑛 ) )
126 125 fveq2d ⊢ ( 𝑦 = 𝑛 → ( log ‘ ( 𝑥 / 𝑦 ) ) = ( log ‘ ( 𝑥 / 𝑛 ) ) )
127 126 oveq1d ⊢ ( 𝑦 = 𝑛 → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) = ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) )
128 94 rpxrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ* )
129 simp1rl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
130 simp2r ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
131 129 130 rpdivcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
132 131 relogcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
133 simp2l ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑦 ∈ ℝ+ )
134 129 133 rpdivcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑥 / 𝑦 ) ∈ ℝ+ )
135 134 relogcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( log ‘ ( 𝑥 / 𝑦 ) ) ∈ ℝ )
136 simp1l ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑁 ∈ ℕ0 )
137 log1 ⊢ ( log ‘ 1 ) = 0
138 130 rpcnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℂ )
139 138 mulid2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 1 · 𝑛 ) = 𝑛 )
140 simp33 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ≤ 𝑥 )
141 139 140 eqbrtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 1 · 𝑛 ) ≤ 𝑥 )
142 1red ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 1 ∈ ℝ )
143 129 rpred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
144 142 143 130 lemuldivd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( ( 1 · 𝑛 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑛 ) ) )
145 141 144 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 1 ≤ ( 𝑥 / 𝑛 ) )
146 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ ( 𝑥 / 𝑛 ) ∈ ℝ+ ) → ( 1 ≤ ( 𝑥 / 𝑛 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( 𝑥 / 𝑛 ) ) ) )
147 50 131 146 sylancr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 1 ≤ ( 𝑥 / 𝑛 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( 𝑥 / 𝑛 ) ) ) )
148 145 147 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( log ‘ 1 ) ≤ ( log ‘ ( 𝑥 / 𝑛 ) ) )
149 137 148 eqbrtrrid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 0 ≤ ( log ‘ ( 𝑥 / 𝑛 ) ) )
150 simp32 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑦 ≤ 𝑛 )
151 133 130 129 lediv2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑦 ≤ 𝑛 ↔ ( 𝑥 / 𝑛 ) ≤ ( 𝑥 / 𝑦 ) ) )
152 150 151 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑥 / 𝑛 ) ≤ ( 𝑥 / 𝑦 ) )
153 131 134 logled ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( ( 𝑥 / 𝑛 ) ≤ ( 𝑥 / 𝑦 ) ↔ ( log ‘ ( 𝑥 / 𝑛 ) ) ≤ ( log ‘ ( 𝑥 / 𝑦 ) ) ) )
154 152 153 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ≤ ( log ‘ ( 𝑥 / 𝑦 ) ) )
155 leexp1a ⊢ ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ∧ ( log ‘ ( 𝑥 / 𝑦 ) ) ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ ( log ‘ ( 𝑥 / 𝑛 ) ) ∧ ( log ‘ ( 𝑥 / 𝑛 ) ) ≤ ( log ‘ ( 𝑥 / 𝑦 ) ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ≤ ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) )
156 132 135 136 149 154 155 syl32anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ≤ ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) )
157 eqid ⊢ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) )
158 96 3ad2antr1 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( 𝑥 / 𝑦 ) ∈ ℝ+ )
159 158 relogcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( log ‘ ( 𝑥 / 𝑦 ) ) ∈ ℝ )
160 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 𝑁 ∈ ℕ0 )
161 rpcn ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ )
162 161 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℂ )
163 162 3ad2antr1 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 𝑦 ∈ ℂ )
164 163 mulid2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( 1 · 𝑦 ) = 𝑦 )
165 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 𝑦 ≤ 𝑥 )
166 164 165 eqbrtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( 1 · 𝑦 ) ≤ 𝑥 )
167 1red ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 1 ∈ ℝ )
168 94 rpred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
169 168 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
170 simpr1 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 𝑦 ∈ ℝ+ )
171 167 169 170 lemuldivd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( ( 1 · 𝑦 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑦 ) ) )
172 166 171 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 1 ≤ ( 𝑥 / 𝑦 ) )
173 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ ( 𝑥 / 𝑦 ) ∈ ℝ+ ) → ( 1 ≤ ( 𝑥 / 𝑦 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( 𝑥 / 𝑦 ) ) ) )
174 50 158 173 sylancr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( 1 ≤ ( 𝑥 / 𝑦 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( 𝑥 / 𝑦 ) ) ) )
175 172 174 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( log ‘ 1 ) ≤ ( log ‘ ( 𝑥 / 𝑦 ) ) )
176 137 175 eqbrtrrid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 0 ≤ ( log ‘ ( 𝑥 / 𝑦 ) ) )
177 159 160 176 expge0d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 0 ≤ ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) )
178 50 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℝ+ )
179 1le1 ⊢ 1 ≤ 1
180 179 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 1 )
181 simprr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
182 168 leidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ≤ 𝑥 )
183 79 80 82 83 87 88 105 107 109 124 127 128 156 157 177 178 94 180 181 182 dvfsumlem4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑥 ) − ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 1 ) ) ) ≤ ⦋ 1 / 𝑦 ⦌ ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) )
184 fzfid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
185 94 4 5 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
186 185 relogcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
187 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ0 )
188 186 187 reexpcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ∈ ℝ )
189 184 188 fsumrecl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ∈ ℝ )
190 189 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ∈ ℂ )
191 94 rpcnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℂ )
192 72 191 mulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ! ‘ 𝑁 ) · 𝑥 ) ∈ ℂ )
193 11 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
194 193 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
195 194 114 expcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℂ )
196 fzfid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 0 ... 𝑁 ) ∈ Fin )
197 193 20 21 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( log ‘ 𝑥 ) ↑ 𝑘 ) ∈ ℝ )
198 20 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
199 198 faccld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
200 197 199 nndivred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
201 200 recnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
202 196 201 fsumcl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
203 72 202 mulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℂ )
204 195 203 subcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ∈ ℂ )
205 190 192 204 sub32d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) )
206 eqidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) )
207 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
208 207 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( ⌊ ‘ 𝑦 ) = ( ⌊ ‘ 𝑥 ) )
209 208 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) = ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
210 209 sumeq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) )
211 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑥 / 𝑦 ) = ( 𝑥 / 𝑥 ) )
212 65 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
213 divid ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 𝑥 / 𝑥 ) = 1 )
214 212 213 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 / 𝑥 ) = 1 )
215 211 214 sylan9eqr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( 𝑥 / 𝑦 ) = 1 )
216 215 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 / 𝑦 ) = 1 )
217 216 fveq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( log ‘ ( 𝑥 / 𝑦 ) ) = ( log ‘ 1 ) )
218 217 137 eqtrdi ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( log ‘ ( 𝑥 / 𝑦 ) ) = 0 )
219 218 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) = ( 0 ↑ 𝑘 ) )
220 219 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
221 220 sumeq2dv ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
222 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
223 114 222 eleqtrdi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
224 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑁 ) )
225 223 224 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ∈ ( 0 ... 𝑁 ) )
226 225 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → 0 ∈ ( 0 ... 𝑁 ) )
227 226 snssd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → { 0 } ⊆ ( 0 ... 𝑁 ) )
228 elsni ⊢ ( 𝑘 ∈ { 0 } → 𝑘 = 0 )
229 228 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ { 0 } ) → 𝑘 = 0 )
230 oveq2 ⊢ ( 𝑘 = 0 → ( 0 ↑ 𝑘 ) = ( 0 ↑ 0 ) )
231 0exp0e1 ⊢ ( 0 ↑ 0 ) = 1
232 230 231 eqtrdi ⊢ ( 𝑘 = 0 → ( 0 ↑ 𝑘 ) = 1 )
233 fveq2 ⊢ ( 𝑘 = 0 → ( ! ‘ 𝑘 ) = ( ! ‘ 0 ) )
234 fac0 ⊢ ( ! ‘ 0 ) = 1
235 233 234 eqtrdi ⊢ ( 𝑘 = 0 → ( ! ‘ 𝑘 ) = 1 )
236 232 235 oveq12d ⊢ ( 𝑘 = 0 → ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( 1 / 1 ) )
237 1div1e1 ⊢ ( 1 / 1 ) = 1
238 236 237 eqtrdi ⊢ ( 𝑘 = 0 → ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = 1 )
239 229 238 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ { 0 } ) → ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = 1 )
240 ax-1cn ⊢ 1 ∈ ℂ
241 239 240 eqeltrdi ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ { 0 } ) → ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
242 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
243 242 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
244 243 20 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → 𝑘 ∈ ℕ0 )
245 eldifsni ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) → 𝑘 ≠ 0 )
246 245 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → 𝑘 ≠ 0 )
247 eldifsn ⊢ ( 𝑘 ∈ ( ℕ0 ∖ { 0 } ) ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0 ) )
248 244 246 247 sylanbrc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → 𝑘 ∈ ( ℕ0 ∖ { 0 } ) )
249 dfn2 ⊢ ℕ = ( ℕ0 ∖ { 0 } )
250 248 249 eleqtrrdi ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → 𝑘 ∈ ℕ )
251 250 0expd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → ( 0 ↑ 𝑘 ) = 0 )
252 251 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( 0 / ( ! ‘ 𝑘 ) ) )
253 244 faccld ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
254 253 nncnd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
255 253 nnne0d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
256 254 255 div0d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → ( 0 / ( ! ‘ 𝑘 ) ) = 0 )
257 252 256 eqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) → ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = 0 )
258 fzfid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( 0 ... 𝑁 ) ∈ Fin )
259 227 241 257 258 fsumss ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → Σ 𝑘 ∈ { 0 } ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
260 221 259 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = Σ 𝑘 ∈ { 0 } ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
261 0cn ⊢ 0 ∈ ℂ
262 238 sumsn ⊢ ( ( 0 ∈ ℂ ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ { 0 } ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = 1 )
263 261 240 262 mp2an ⊢ Σ 𝑘 ∈ { 0 } ( ( 0 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = 1
264 260 263 eqtrdi ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = 1 )
265 207 264 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( 𝑥 · 1 ) )
266 191 mulid1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 · 1 ) = 𝑥 )
267 266 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( 𝑥 · 1 ) = 𝑥 )
268 265 267 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = 𝑥 )
269 268 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) = ( ( ! ‘ 𝑁 ) · 𝑥 ) )
270 210 269 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 𝑥 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) )
271 ovexd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) ∈ V )
272 206 270 94 271 fvmptd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑥 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) )
273 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → 𝑦 = 1 )
274 273 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( ⌊ ‘ 𝑦 ) = ( ⌊ ‘ 1 ) )
275 flid ⊢ ( 1 ∈ ℤ → ( ⌊ ‘ 1 ) = 1 )
276 81 275 ax-mp ⊢ ( ⌊ ‘ 1 ) = 1
277 274 276 eqtrdi ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( ⌊ ‘ 𝑦 ) = 1 )
278 277 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) = ( 1 ... 1 ) )
279 278 sumeq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) = Σ 𝑛 ∈ ( 1 ... 1 ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) )
280 191 div1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 / 1 ) = 𝑥 )
281 280 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( 𝑥 / 1 ) = 𝑥 )
282 281 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( log ‘ ( 𝑥 / 1 ) ) = ( log ‘ 𝑥 ) )
283 282 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( ( log ‘ ( 𝑥 / 1 ) ) ↑ 𝑁 ) = ( ( log ‘ 𝑥 ) ↑ 𝑁 ) )
284 195 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℂ )
285 283 284 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( ( log ‘ ( 𝑥 / 1 ) ) ↑ 𝑁 ) ∈ ℂ )
286 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑥 / 𝑛 ) = ( 𝑥 / 1 ) )
287 286 fveq2d ⊢ ( 𝑛 = 1 → ( log ‘ ( 𝑥 / 𝑛 ) ) = ( log ‘ ( 𝑥 / 1 ) ) )
288 287 oveq1d ⊢ ( 𝑛 = 1 → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) = ( ( log ‘ ( 𝑥 / 1 ) ) ↑ 𝑁 ) )
289 288 fsum1 ⊢ ( ( 1 ∈ ℤ ∧ ( ( log ‘ ( 𝑥 / 1 ) ) ↑ 𝑁 ) ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... 1 ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) = ( ( log ‘ ( 𝑥 / 1 ) ) ↑ 𝑁 ) )
290 81 285 289 sylancr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → Σ 𝑛 ∈ ( 1 ... 1 ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) = ( ( log ‘ ( 𝑥 / 1 ) ) ↑ 𝑁 ) )
291 279 290 283 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) = ( ( log ‘ 𝑥 ) ↑ 𝑁 ) )
292 273 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( 𝑥 / 𝑦 ) = ( 𝑥 / 1 ) )
293 292 281 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( 𝑥 / 𝑦 ) = 𝑥 )
294 293 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( log ‘ ( 𝑥 / 𝑦 ) ) = ( log ‘ 𝑥 ) )
295 294 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( log ‘ ( 𝑥 / 𝑦 ) ) = ( log ‘ 𝑥 ) )
296 295 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) = ( ( log ‘ 𝑥 ) ↑ 𝑘 ) )
297 296 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
298 297 sumeq2dv ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
299 273 298 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( 1 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
300 202 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
301 300 mulid2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( 1 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
302 299 301 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
303 302 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) = ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
304 291 303 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) = ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) )
305 ovexd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ∈ V )
306 206 304 178 305 fvmptd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 1 ) = ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) )
307 272 306 oveq12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑥 ) − ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 1 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) )
308 70 72 191 subdird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) · 𝑥 ) = ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) · 𝑥 ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) )
309 64 adantrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ∈ ℂ )
310 212 simprd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ≠ 0 )
311 309 191 310 divcan1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) · 𝑥 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) )
312 311 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) · 𝑥 ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) )
313 308 312 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) · 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) − ( ( ! ‘ 𝑁 ) · 𝑥 ) ) )
314 205 307 313 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑥 ) − ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 1 ) ) = ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) · 𝑥 ) )
315 314 fveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑥 ) − ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 1 ) ) ) = ( abs ‘ ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) · 𝑥 ) ) )
316 73 191 absmuld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) · 𝑥 ) ) = ( ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) · ( abs ‘ 𝑥 ) ) )
317 rprege0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
318 317 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
319 absid ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( abs ‘ 𝑥 ) = 𝑥 )
320 318 319 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ 𝑥 ) = 𝑥 )
321 320 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) · ( abs ‘ 𝑥 ) ) = ( ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) · 𝑥 ) )
322 315 316 321 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑥 ) − ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · ( 𝑦 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) ) ‘ 1 ) ) ) = ( ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) · 𝑥 ) )
323 1cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℂ )
324 294 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑦 = 1 ) → ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) = ( ( log ‘ 𝑥 ) ↑ 𝑁 ) )
325 323 324 csbied ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ⦋ 1 / 𝑦 ⦌ ( ( log ‘ ( 𝑥 / 𝑦 ) ) ↑ 𝑁 ) = ( ( log ‘ 𝑥 ) ↑ 𝑁 ) )
326 183 322 325 3brtr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) · 𝑥 ) ≤ ( ( log ‘ 𝑥 ) ↑ 𝑁 ) )
327 14 adantrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℝ )
328 74 327 94 lemuldivd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) · 𝑥 ) ≤ ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ↔ ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) ≤ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ) )
329 326 328 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) ≤ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) )
330 75 leabsd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ≤ ( abs ‘ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ) )
331 74 75 77 329 330 letrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) ≤ ( abs ‘ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ) )
332 57 adantrr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ∈ ℂ )
333 332 subid1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) − 0 ) = ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) )
334 333 fveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) − 0 ) ) = ( abs ‘ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) ) )
335 331 334 breqtrrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) − ( ! ‘ 𝑁 ) ) ) ≤ ( abs ‘ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) − 0 ) ) )
336 33 34 54 57 69 335 rlimsqzlem ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) ) ⇝𝑟 ( ! ‘ 𝑁 ) )
337 divsubdir ⊢ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℂ ∧ ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) = ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ) )
338 59 62 66 337 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) = ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ) )
339 338 mpteq2dva ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ) ) )
340 rerpdivcl ⊢ ( ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ∈ ℝ )
341 27 340 sylancom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ∈ ℝ )
342 divass ⊢ ( ( ( ! ‘ 𝑁 ) ∈ ℂ ∧ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) = ( ( ! ‘ 𝑁 ) · ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) ) )
343 60 61 66 342 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) = ( ( ! ‘ 𝑁 ) · ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) ) )
344 25 recnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
345 18 67 344 68 fsumdivc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) )
346 22 recnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( log ‘ 𝑥 ) ↑ 𝑘 ) ∈ ℂ )
347 24 nnrpd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℝ+ )
348 347 rpcnne0d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ! ‘ 𝑘 ) ∈ ℂ ∧ ( ! ‘ 𝑘 ) ≠ 0 ) )
349 66 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
350 divdiv32 ⊢ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) ∈ ℂ ∧ ( ( ! ‘ 𝑘 ) ∈ ℂ ∧ ( ! ‘ 𝑘 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) = ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) )
351 346 348 349 350 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) = ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) )
352 351 sumeq2dv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) )
353 345 352 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) )
354 353 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) · ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) / 𝑥 ) ) = ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) )
355 343 354 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) = ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) )
356 355 mpteq2dva ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) ) )
357 2 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑥 ∈ ℝ+ )
358 22 357 rerpdivcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) ∈ ℝ )
359 358 24 nndivred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
360 18 359 fsumrecl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
361 rpssre ⊢ ℝ+ ⊆ ℝ
362 rlimconst ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( ! ‘ 𝑁 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( ! ‘ 𝑁 ) ) ⇝𝑟 ( ! ‘ 𝑁 ) )
363 361 34 362 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ! ‘ 𝑁 ) ) ⇝𝑟 ( ! ‘ 𝑁 ) )
364 361 a1i ⊢ ( 𝑁 ∈ ℕ0 → ℝ+ ⊆ ℝ )
365 fzfid ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) ∈ Fin )
366 359 anasss ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
367 358 an32s ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) ∈ ℝ )
368 20 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
369 368 faccld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
370 369 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℝ )
371 370 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ! ‘ 𝑘 ) ∈ ℝ )
372 368 53 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) ) ⇝𝑟 0 )
373 369 nncnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
374 rlimconst ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( ! ‘ 𝑘 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( ! ‘ 𝑘 ) ) ⇝𝑟 ( ! ‘ 𝑘 ) )
375 361 373 374 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ! ‘ 𝑘 ) ) ⇝𝑟 ( ! ‘ 𝑘 ) )
376 369 nnne0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
377 376 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ! ‘ 𝑘 ) ≠ 0 )
378 367 371 372 375 376 377 rlimdiv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) ⇝𝑟 ( 0 / ( ! ‘ 𝑘 ) ) )
379 373 376 div0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 0 / ( ! ‘ 𝑘 ) ) = 0 )
380 378 379 breqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) ⇝𝑟 0 )
381 364 365 366 380 fsumrlim ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) ⇝𝑟 Σ 𝑘 ∈ ( 0 ... 𝑁 ) 0 )
382 fzfi ⊢ ( 0 ... 𝑁 ) ∈ Fin
383 382 olci ⊢ ( ( 0 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑁 ) ∈ Fin )
384 sumz ⊢ ( ( ( 0 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑁 ) ∈ Fin ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) 0 = 0 )
385 383 384 ax-mp ⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) 0 = 0
386 381 385 breqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) ⇝𝑟 0 )
387 17 360 363 386 rlimmul ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) ) ⇝𝑟 ( ( ! ‘ 𝑁 ) · 0 ) )
388 34 mul01d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) · 0 ) = 0 )
389 387 388 breqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / 𝑥 ) / ( ! ‘ 𝑘 ) ) ) ) ⇝𝑟 0 )
390 356 389 eqbrtrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ) ⇝𝑟 0 )
391 56 341 54 390 rlimsub ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ) ) ⇝𝑟 ( 0 − 0 ) )
392 0m0e0 ⊢ ( 0 − 0 ) = 0
393 391 392 breqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) / 𝑥 ) ) ) ⇝𝑟 0 )
394 339 393 eqbrtrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) ⇝𝑟 0 )
395 30 32 336 394 rlimadd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) + ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) ) ⇝𝑟 ( ( ! ‘ 𝑁 ) + 0 ) )
396 divsubdir ⊢ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) ∈ ℂ ∧ ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) )
397 58 63 66 396 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) )
398 397 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) + ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) + ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) )
399 10 2 rerpdivcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) ∈ ℝ )
400 399 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) ∈ ℂ )
401 32 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ∈ ℂ )
402 400 401 npcand ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) − ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) + ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) )
403 398 402 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) + ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) )
404 403 mpteq2dva ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) − ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) / 𝑥 ) + ( ( ( ( log ‘ 𝑥 ) ↑ 𝑁 ) − ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ 𝑥 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) ) )
405 34 addid1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) + 0 ) = ( ! ‘ 𝑁 ) )
406 395 404 405 3brtr3d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 𝑁 ) / 𝑥 ) ) ⇝𝑟 ( ! ‘ 𝑁 ) )