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

Theorem advlogexp 25170
Description: The antiderivative of a power of the logarithm. (Set 𝐴 = 1 and multiply by (-1)↑𝑁 · 𝑁! to get the antiderivative of log(𝑥)↑𝑁 itself.) (Contributed by Mario Carneiro, 22-May-2016.)
Assertion
Ref Expression
advlogexp ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))))
Distinct variable groups:   𝑥,𝑘,𝐴   𝑘,𝑁,𝑥

Proof of Theorem advlogexp
Dummy variables 𝑗 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 13336 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0...𝑁) ∈ Fin)
2 rpcn 12394 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
32adantl 482 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
4 rpdivcl 12409 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈ ℝ+)
54adantlr 711 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈ ℝ+)
65relogcld 25138 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℝ)
7 elfznn0 12995 . . . . . . . . 9 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
8 reexpcl 13441 . . . . . . . . 9 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ)
96, 7, 8syl2an 595 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ)
107adantl 482 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
1110faccld 13639 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
129, 11nndivred 11685 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℝ)
1312recnd 10663 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℂ)
141, 3, 13fsummulc2 15134 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))
15 simplr 765 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ ℕ0)
16 nn0uz 12274 . . . . . . 7 0 = (ℤ‘0)
1715, 16syl6eleq 2928 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ‘0))
183adantr 481 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℂ)
1918, 13mulcld 10655 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ)
20 oveq2 7158 . . . . . . . 8 (𝑘 = 0 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑0))
21 fveq2 6669 . . . . . . . . 9 (𝑘 = 0 → (!‘𝑘) = (!‘0))
22 fac0 13631 . . . . . . . . 9 (!‘0) = 1
2321, 22syl6eq 2877 . . . . . . . 8 (𝑘 = 0 → (!‘𝑘) = 1)
2420, 23oveq12d 7168 . . . . . . 7 (𝑘 = 0 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑0) / 1))
2524oveq2d 7166 . . . . . 6 (𝑘 = 0 → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)))
2617, 19, 25fsum1p 15103 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))))
276recnd 10663 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℂ)
2827exp0d 13499 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((log‘(𝐴 / 𝑥))↑0) = 1)
2928oveq1d 7165 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑0) / 1) = (1 / 1))
30 1div1e1 11324 . . . . . . . . 9 (1 / 1) = 1
3129, 30syl6eq 2877 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑0) / 1) = 1)
3231oveq2d 7166 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = (𝑥 · 1))
333mulid1d 10652 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥)
3432, 33eqtrd 2861 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = 𝑥)
35 1zzd 12007 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℤ)
36 nn0z 11999 . . . . . . . . 9 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
3736ad2antlr 723 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ ℤ)
38 fz1ssfz0 12998 . . . . . . . . . 10 (1...𝑁) ⊆ (0...𝑁)
3938sseli 3967 . . . . . . . . 9 (𝑘 ∈ (1...𝑁) → 𝑘 ∈ (0...𝑁))
4039, 19sylan2 592 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ)
41 oveq2 7158 . . . . . . . . . 10 (𝑘 = (𝑗 + 1) → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)))
42 fveq2 6669 . . . . . . . . . 10 (𝑘 = (𝑗 + 1) → (!‘𝑘) = (!‘(𝑗 + 1)))
4341, 42oveq12d 7168 . . . . . . . . 9 (𝑘 = (𝑗 + 1) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
4443oveq2d 7166 . . . . . . . 8 (𝑘 = (𝑗 + 1) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
4535, 35, 37, 40, 44fsumshftm 15131 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
46 0p1e1 11753 . . . . . . . . . 10 (0 + 1) = 1
4746oveq1i 7160 . . . . . . . . 9 ((0 + 1)...𝑁) = (1...𝑁)
4847sumeq1i 15050 . . . . . . . 8 Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))
4948a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))
50 1m1e0 11703 . . . . . . . . . 10 (1 − 1) = 0
5150oveq1i 7160 . . . . . . . . 9 ((1 − 1)..^𝑁) = (0..^𝑁)
52 fzoval 13034 . . . . . . . . . 10 (𝑁 ∈ ℤ → ((1 − 1)..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5337, 52syl 17 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((1 − 1)..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5451, 53syl5eqr 2875 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5554sumeq1d 15053 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
5645, 49, 553eqtr4d 2871 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
5734, 56oveq12d 7168 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))
5814, 26, 573eqtrd 2865 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))
5958mpteq2dva 5158 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))))
6059oveq2d 7166 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))))
61 reelprrecn 10623 . . . 4 ℝ ∈ {ℝ, ℂ}
6261a1i 11 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ ∈ {ℝ, ℂ})
63 1cnd 10630 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
64 recn 10621 . . . . 5 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
6564adantl 482 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
66 1cnd 10630 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
6762dvmptid 24488 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
68 rpssre 12391 . . . . 5 + ⊆ ℝ
6968a1i 11 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ+ ⊆ ℝ)
70 eqid 2826 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
7170tgioo2 23345 . . . 4 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
72 ioorp 12809 . . . . . 6 (0(,)+∞) = ℝ+
73 iooretop 23308 . . . . . 6 (0(,)+∞) ∈ (topGen‘ran (,))
7472, 73eqeltrri 2915 . . . . 5 + ∈ (topGen‘ran (,))
7574a1i 11 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ+ ∈ (topGen‘ran (,)))
7662, 65, 66, 67, 69, 71, 70, 75dvmptres 24494 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+𝑥)) = (𝑥 ∈ ℝ+ ↦ 1))
77 fzofi 13337 . . . . 5 (0..^𝑁) ∈ Fin
7877a1i 11 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0..^𝑁) ∈ Fin)
793adantr 481 . . . . 5 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℂ)
80 elfzonn0 13077 . . . . . . . . 9 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℕ0)
81 peano2nn0 11931 . . . . . . . . 9 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ0)
8280, 81syl 17 . . . . . . . 8 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ ℕ0)
83 reexpcl 13441 . . . . . . . 8 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ (𝑗 + 1) ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ)
846, 82, 83syl2an 595 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ)
8582adantl 482 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ0)
8685faccld 13639 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ)
8784, 86nndivred 11685 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℝ)
8887recnd 10663 . . . . 5 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
8979, 88mulcld 10655 . . . 4 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
9078, 89fsumcl 15085 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
916, 15reexpcld 13522 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((log‘(𝐴 / 𝑥))↑𝑁) ∈ ℝ)
92 faccl 13638 . . . . . . 7 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
9392ad2antlr 723 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
9491, 93nndivred 11685 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℝ)
9594recnd 10663 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ)
96 ax-1cn 10589 . . . 4 1 ∈ ℂ
97 subcl 10879 . . . 4 (((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈ ℂ)
9895, 96, 97sylancl 586 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈ ℂ)
9977a1i 11 . . . . 5 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (0..^𝑁) ∈ Fin)
10089an32s 648 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
1011003impa 1104 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
102 reexpcl 13441 . . . . . . . . . . 11 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ)
1036, 80, 102syl2an 595 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ)
10480adantl 482 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0)
105104faccld 13639 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ)
106103, 105nndivred 11685 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℝ)
107106recnd 10663 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ)
10888, 107subcld 10991 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
109108an32s 648 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
1101093impa 1104 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
11161a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ ∈ {ℝ, ℂ})
1122adantl 482 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
113 1cnd 10630 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
11476adantr 481 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+𝑥)) = (𝑥 ∈ ℝ+ ↦ 1))
11588an32s 648 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
116 negex 10878 . . . . . . . 8 -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V
117116a1i 11 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V)
118 cnelprrecn 10624 . . . . . . . . . 10 ℂ ∈ {ℝ, ℂ}
119118a1i 11 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℂ ∈ {ℝ, ℂ})
12027adantlr 711 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℂ)
121 negex 10878 . . . . . . . . . 10 -(1 / 𝑥) ∈ V
122121a1i 11 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -(1 / 𝑥) ∈ V)
123 id 22 . . . . . . . . . . 11 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
12480adantl 482 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0)
125124, 81syl 17 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ0)
126 expcl 13442 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ (𝑗 + 1) ∈ ℕ0) → (𝑦↑(𝑗 + 1)) ∈ ℂ)
127123, 125, 126syl2anr 596 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑(𝑗 + 1)) ∈ ℂ)
128125faccld 13639 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ)
129128nncnd 11648 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℂ)
130129adantr 481 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ∈ ℂ)
131128nnne0d 11681 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ≠ 0)
132131adantr 481 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ≠ 0)
133127, 130, 132divcld 11410 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
134 expcl 13442 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝑦𝑗) ∈ ℂ)
135123, 124, 134syl2anr 596 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦𝑗) ∈ ℂ)
136124faccld 13639 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ)
137136nncnd 11648 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℂ)
138137adantr 481 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈ ℂ)
139124adantr 481 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℕ0)
140139faccld 13639 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈ ℕ)
141140nnne0d 11681 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ≠ 0)
142135, 138, 141divcld 11410 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦𝑗) / (!‘𝑗)) ∈ ℂ)
143 simplll 771 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝐴 ∈ ℝ+)
144 simpr 485 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
145143, 144relogdivd 25141 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) = ((log‘𝐴) − (log‘𝑥)))
146145mpteq2dva 5158 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥))))
147146oveq2d 7166 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (ℝ D (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥)))))
148 relogcl 25091 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
149148ad2antrr 722 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℝ)
150149recnd 10663 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℂ)
151150adantr 481 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝐴) ∈ ℂ)
152 0cnd 10628 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 0 ∈ ℂ)
153150adantr 481 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (log‘𝐴) ∈ ℂ)
154 0cnd 10628 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℂ)
155111, 150dvmptc 24489 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ ↦ (log‘𝐴))) = (𝑥 ∈ ℝ ↦ 0))
15668a1i 11 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ+ ⊆ ℝ)
15774a1i 11 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ+ ∈ (topGen‘ran (,)))
158111, 153, 154, 155, 156, 71, 70, 157dvmptres 24494 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝐴))) = (𝑥 ∈ ℝ+ ↦ 0))
159144relogcld 25138 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
160159recnd 10663 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
161144rpreccld 12436 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
162 dvrelog 25152 . . . . . . . . . . . . 13 (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))
163 relogf1o 25082 . . . . . . . . . . . . . . . . 17 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
164 f1of 6614 . . . . . . . . . . . . . . . . 17 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
165163, 164mp1i 13 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+):ℝ+⟶ℝ)
166165feqmptd 6732 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)))
167 fvres 6688 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ+ → ((log ↾ ℝ+)‘𝑥) = (log‘𝑥))
168167mpteq2ia 5154 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥))
169166, 168syl6eq 2877 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)))
170169oveq2d 7166 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (log ↾ ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝑥))))
171162, 170syl5reqr 2876 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
172111, 151, 152, 158, 160, 161, 171dvmptsub 24498 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥))))
173147, 172eqtrd 2861 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥))))
174 df-neg 10867 . . . . . . . . . . 11 -(1 / 𝑥) = (0 − (1 / 𝑥))
175174mpteq2i 5155 . . . . . . . . . 10 (𝑥 ∈ ℝ+ ↦ -(1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥)))
176173, 175syl6eqr 2879 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ -(1 / 𝑥)))
177 ovexd 7185 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) ∈ V)
178 nn0p1nn 11930 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
179124, 178syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ)
180 dvexp 24484 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1)))))
181179, 180syl 17 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1)))))
182119, 127, 177, 181, 129, 131dvmptdivc 24496 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))))
183124nn0cnd 11951 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℂ)
184183adantr 481 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℂ)
185 pncan 10886 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
186184, 96, 185sylancl 586 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
187186oveq2d 7166 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑((𝑗 + 1) − 1)) = (𝑦𝑗))
188187oveq2d 7166 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑦𝑗)))
189 facp1 13633 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1)))
190139, 189syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1)))
191 peano2cn 10806 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → (𝑗 + 1) ∈ ℂ)
192184, 191syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ∈ ℂ)
193138, 192mulcomd 10656 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((!‘𝑗) · (𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗)))
194190, 193eqtrd 2861 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗)))
195188, 194oveq12d 7168 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = (((𝑗 + 1) · (𝑦𝑗)) / ((𝑗 + 1) · (!‘𝑗))))
196179nnne0d 11681 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ≠ 0)
197196adantr 481 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ≠ 0)
198135, 138, 192, 141, 197divcan5d 11436 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦𝑗)) / ((𝑗 + 1) · (!‘𝑗))) = ((𝑦𝑗) / (!‘𝑗)))
199195, 198eqtrd 2861 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = ((𝑦𝑗) / (!‘𝑗)))
200199mpteq2dva 5158 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑦𝑗) / (!‘𝑗))))
201182, 200eqtrd 2861 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ ((𝑦𝑗) / (!‘𝑗))))
202 oveq1 7157 . . . . . . . . . 10 (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑(𝑗 + 1)) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)))
203202oveq1d 7165 . . . . . . . . 9 (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
204 oveq1 7157 . . . . . . . . . 10 (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦𝑗) = ((log‘(𝐴 / 𝑥))↑𝑗))
205204oveq1d 7165 . . . . . . . . 9 (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦𝑗) / (!‘𝑗)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
206111, 119, 120, 122, 133, 142, 176, 201, 203, 205dvmptco 24503 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))))
207107an32s 648 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ)
208161rpcnd 12428 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℂ)
209207, 208mulneg2d 11088 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
210 rpne0 12400 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+𝑥 ≠ 0)
211210adantl 482 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
212207, 112, 211divrecd 11413 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
213212negeqd 10874 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
214209, 213eqtr4d 2864 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))
215214mpteq2dva 5158 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)))
216206, 215eqtrd 2861 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦ -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)))
217111, 112, 113, 114, 115, 117, 216dvmptmul 24492 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))))
21888mulid2d 10653 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
219 simplr 765 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℝ+)
220106, 219rerpdivcld 12457 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℝ)
221220recnd 10663 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℂ)
222221, 79mulneg1d 11087 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))
223211an32s 648 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ≠ 0)
224107, 79, 223divcan1d 11411 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
225224negeqd 10874 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
226222, 225eqtrd 2861 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
227218, 226oveq12d 7168 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
22888, 107negsubd 10997 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
229227, 228eqtrd 2861 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
230229an32s 648 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
231230mpteq2dva 5158 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
232217, 231eqtrd 2861 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
23371, 70, 62, 75, 99, 101, 110, 232dvmptfsum 24506 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
234 oveq2 7158 . . . . . . . 8 (𝑘 = 𝑗 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑗))
235 fveq2 6669 . . . . . . . 8 (𝑘 = 𝑗 → (!‘𝑘) = (!‘𝑗))
236234, 235oveq12d 7168 . . . . . . 7 (𝑘 = 𝑗 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
237 oveq2 7158 . . . . . . . 8 (𝑘 = 𝑁 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑁))
238 fveq2 6669 . . . . . . . 8 (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
239237, 238oveq12d 7168 . . . . . . 7 (𝑘 = 𝑁 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
240236, 43, 24, 239, 17, 13telfsumo2 15153 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)))
24131oveq2d 7166 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))
242240, 241eqtrd 2861 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))
243242mpteq2dva 5158 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))
244233, 243eqtrd 2861 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))
24562, 3, 63, 76, 90, 98, 244dvmptadd 24491 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) = (𝑥 ∈ ℝ+ ↦ (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))))
246 pncan3 10888 . . . 4 ((1 ∈ ℂ ∧ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) → (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
24796, 95, 246sylancr 587 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
248247mpteq2dva 5158 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))))
24960, 245, 2483eqtrd 2865 1 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  wne 3021  Vcvv 3500  wss 3940  {cpr 4566  cmpt 5143  ran crn 5555  cres 5556  wf 6350  1-1-ontowf1o 6353  cfv 6354  (class class class)co 7150  Fincfn 8503  cc 10529  cr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536  +∞cpnf 10666  cmin 10864  -cneg 10865   / cdiv 11291  cn 11632  0cn0 11891  cz 11975  cuz 12237  +crp 12384  (,)cioo 12733  ...cfz 12887  ..^cfzo 13028  cexp 13424  !cfa 13628  Σcsu 15037  TopOpenctopn 16690  topGenctg 16706  fldccnfld 20480   D cdv 24395  logclog 25070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609  ax-addf 10610  ax-mulf 10611
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-om 7574  df-1st 7685  df-2nd 7686  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8284  df-map 8403  df-pm 8404  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-fi 8869  df-sup 8900  df-inf 8901  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-q 12343  df-rp 12385  df-xneg 12502  df-xadd 12503  df-xmul 12504  df-ioo 12737  df-ioc 12738  df-ico 12739  df-icc 12740  df-fz 12888  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13425  df-fac 13629  df-bc 13658  df-hash 13686  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-ef 15416  df-sin 15418  df-cos 15419  df-pi 15421  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18170  df-cntz 18392  df-cmn 18844  df-psmet 20472  df-xmet 20473  df-met 20474  df-bl 20475  df-mopn 20476  df-fbas 20477  df-fg 20478  df-cnfld 20481  df-top 21437  df-topon 21454  df-topsp 21476  df-bases 21489  df-cld 21562  df-ntr 21563  df-cls 21564  df-nei 21641  df-lp 21679  df-perf 21680  df-cn 21770  df-cnp 21771  df-haus 21858  df-cmp 21930  df-tx 22105  df-hmeo 22298  df-fil 22389  df-fm 22481  df-flim 22482  df-flf 22483  df-xms 22864  df-ms 22865  df-tms 22866  df-cncf 23420  df-limc 24398  df-dv 24399  df-log 25072
This theorem is referenced by:  logexprlim  25734
  Copyright terms: Public domain W3C validator