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

Theorem advlogexp 24600
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 12966 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0...𝑁) ∈ Fin)
2 rpcn 12034 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
32adantl 473 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
4 rpdivcl 12049 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈ ℝ+)
54adantlr 753 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈ ℝ+)
65relogcld 24568 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℝ)
7 elfznn0 12626 . . . . . . . . 9 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
8 reexpcl 13071 . . . . . . . . 9 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ)
96, 7, 8syl2an 495 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ)
107adantl 473 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
11 faccl 13264 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
1210, 11syl 17 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
139, 12nndivred 11261 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℝ)
1413recnd 10260 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℂ)
151, 3, 14fsummulc2 14715 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))
16 simplr 809 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ ℕ0)
17 nn0uz 11915 . . . . . . 7 0 = (ℤ‘0)
1816, 17syl6eleq 2849 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ‘0))
193adantr 472 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℂ)
2019, 14mulcld 10252 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ)
21 oveq2 6821 . . . . . . . 8 (𝑘 = 0 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑0))
22 fveq2 6352 . . . . . . . . 9 (𝑘 = 0 → (!‘𝑘) = (!‘0))
23 fac0 13257 . . . . . . . . 9 (!‘0) = 1
2422, 23syl6eq 2810 . . . . . . . 8 (𝑘 = 0 → (!‘𝑘) = 1)
2521, 24oveq12d 6831 . . . . . . 7 (𝑘 = 0 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑0) / 1))
2625oveq2d 6829 . . . . . 6 (𝑘 = 0 → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)))
2718, 20, 26fsum1p 14681 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))))
286recnd 10260 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℂ)
2928exp0d 13196 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((log‘(𝐴 / 𝑥))↑0) = 1)
3029oveq1d 6828 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑0) / 1) = (1 / 1))
31 1div1e1 10909 . . . . . . . . 9 (1 / 1) = 1
3230, 31syl6eq 2810 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑0) / 1) = 1)
3332oveq2d 6829 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = (𝑥 · 1))
343mulid1d 10249 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥)
3533, 34eqtrd 2794 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = 𝑥)
36 1zzd 11600 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℤ)
37 nn0z 11592 . . . . . . . . 9 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
3837ad2antlr 765 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ ℤ)
39 fz1ssfz0 12629 . . . . . . . . . 10 (1...𝑁) ⊆ (0...𝑁)
4039sseli 3740 . . . . . . . . 9 (𝑘 ∈ (1...𝑁) → 𝑘 ∈ (0...𝑁))
4140, 20sylan2 492 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ)
42 oveq2 6821 . . . . . . . . . 10 (𝑘 = (𝑗 + 1) → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)))
43 fveq2 6352 . . . . . . . . . 10 (𝑘 = (𝑗 + 1) → (!‘𝑘) = (!‘(𝑗 + 1)))
4442, 43oveq12d 6831 . . . . . . . . 9 (𝑘 = (𝑗 + 1) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
4544oveq2d 6829 . . . . . . . 8 (𝑘 = (𝑗 + 1) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
4636, 36, 38, 41, 45fsumshftm 14712 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
47 0p1e1 11324 . . . . . . . . . 10 (0 + 1) = 1
4847oveq1i 6823 . . . . . . . . 9 ((0 + 1)...𝑁) = (1...𝑁)
4948sumeq1i 14627 . . . . . . . 8 Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))
5049a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))
51 1m1e0 11281 . . . . . . . . . 10 (1 − 1) = 0
5251oveq1i 6823 . . . . . . . . 9 ((1 − 1)..^𝑁) = (0..^𝑁)
53 fzoval 12665 . . . . . . . . . 10 (𝑁 ∈ ℤ → ((1 − 1)..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5438, 53syl 17 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((1 − 1)..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5552, 54syl5eqr 2808 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5655sumeq1d 14630 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
5746, 50, 563eqtr4d 2804 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
5835, 57oveq12d 6831 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))
5915, 27, 583eqtrd 2798 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))
6059mpteq2dva 4896 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))))
6160oveq2d 6829 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))))
62 reelprrecn 10220 . . . 4 ℝ ∈ {ℝ, ℂ}
6362a1i 11 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ ∈ {ℝ, ℂ})
64 1cnd 10248 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
65 recn 10218 . . . . 5 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
6665adantl 473 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
67 1cnd 10248 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
6863dvmptid 23919 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
69 rpssre 12036 . . . . 5 + ⊆ ℝ
7069a1i 11 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ+ ⊆ ℝ)
71 eqid 2760 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
7271tgioo2 22807 . . . 4 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
73 ioorp 12444 . . . . . 6 (0(,)+∞) = ℝ+
74 iooretop 22770 . . . . . 6 (0(,)+∞) ∈ (topGen‘ran (,))
7573, 74eqeltrri 2836 . . . . 5 + ∈ (topGen‘ran (,))
7675a1i 11 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ+ ∈ (topGen‘ran (,)))
7763, 66, 67, 68, 70, 72, 71, 76dvmptres 23925 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+𝑥)) = (𝑥 ∈ ℝ+ ↦ 1))
78 fzofi 12967 . . . . 5 (0..^𝑁) ∈ Fin
7978a1i 11 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0..^𝑁) ∈ Fin)
803adantr 472 . . . . 5 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℂ)
81 elfzonn0 12707 . . . . . . . . 9 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℕ0)
82 peano2nn0 11525 . . . . . . . . 9 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ0)
8381, 82syl 17 . . . . . . . 8 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ ℕ0)
84 reexpcl 13071 . . . . . . . 8 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ (𝑗 + 1) ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ)
856, 83, 84syl2an 495 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ)
8683adantl 473 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ0)
87 faccl 13264 . . . . . . . 8 ((𝑗 + 1) ∈ ℕ0 → (!‘(𝑗 + 1)) ∈ ℕ)
8886, 87syl 17 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ)
8985, 88nndivred 11261 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℝ)
9089recnd 10260 . . . . 5 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
9180, 90mulcld 10252 . . . 4 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
9279, 91fsumcl 14663 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
936, 16reexpcld 13219 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((log‘(𝐴 / 𝑥))↑𝑁) ∈ ℝ)
94 faccl 13264 . . . . . . 7 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
9594ad2antlr 765 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
9693, 95nndivred 11261 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℝ)
9796recnd 10260 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ)
98 ax-1cn 10186 . . . 4 1 ∈ ℂ
99 subcl 10472 . . . 4 (((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈ ℂ)
10097, 98, 99sylancl 697 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈ ℂ)
10178a1i 11 . . . . 5 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (0..^𝑁) ∈ Fin)
10291an32s 881 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
1031023impa 1101 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
104 reexpcl 13071 . . . . . . . . . . 11 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ)
1056, 81, 104syl2an 495 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ)
10681adantl 473 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0)
107 faccl 13264 . . . . . . . . . . 11 (𝑗 ∈ ℕ0 → (!‘𝑗) ∈ ℕ)
108106, 107syl 17 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ)
109105, 108nndivred 11261 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℝ)
110109recnd 10260 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ)
11190, 110subcld 10584 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
112111an32s 881 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
1131123impa 1101 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
11462a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ ∈ {ℝ, ℂ})
1152adantl 473 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
116 1cnd 10248 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
11777adantr 472 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+𝑥)) = (𝑥 ∈ ℝ+ ↦ 1))
11890an32s 881 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
119 negex 10471 . . . . . . . 8 -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V
120119a1i 11 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V)
121 cnelprrecn 10221 . . . . . . . . . 10 ℂ ∈ {ℝ, ℂ}
122121a1i 11 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℂ ∈ {ℝ, ℂ})
12328adantlr 753 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℂ)
124 negex 10471 . . . . . . . . . 10 -(1 / 𝑥) ∈ V
125124a1i 11 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -(1 / 𝑥) ∈ V)
126 id 22 . . . . . . . . . . 11 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
12781adantl 473 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0)
128127, 82syl 17 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ0)
129 expcl 13072 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ (𝑗 + 1) ∈ ℕ0) → (𝑦↑(𝑗 + 1)) ∈ ℂ)
130126, 128, 129syl2anr 496 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑(𝑗 + 1)) ∈ ℂ)
131128, 87syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ)
132131nncnd 11228 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℂ)
133132adantr 472 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ∈ ℂ)
134131nnne0d 11257 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ≠ 0)
135134adantr 472 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ≠ 0)
136130, 133, 135divcld 10993 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
137 expcl 13072 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝑦𝑗) ∈ ℂ)
138126, 127, 137syl2anr 496 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦𝑗) ∈ ℂ)
139127, 107syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ)
140139nncnd 11228 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℂ)
141140adantr 472 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈ ℂ)
142127adantr 472 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℕ0)
143142, 107syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈ ℕ)
144143nnne0d 11257 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ≠ 0)
145138, 141, 144divcld 10993 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦𝑗) / (!‘𝑗)) ∈ ℂ)
146 simplll 815 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝐴 ∈ ℝ+)
147 simpr 479 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
148146, 147relogdivd 24571 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) = ((log‘𝐴) − (log‘𝑥)))
149148mpteq2dva 4896 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥))))
150149oveq2d 6829 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (ℝ D (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥)))))
151 relogcl 24521 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
152151ad2antrr 764 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℝ)
153152recnd 10260 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℂ)
154153adantr 472 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝐴) ∈ ℂ)
155 0cnd 10225 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 0 ∈ ℂ)
156153adantr 472 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (log‘𝐴) ∈ ℂ)
157 0cnd 10225 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℂ)
158114, 153dvmptc 23920 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ ↦ (log‘𝐴))) = (𝑥 ∈ ℝ ↦ 0))
15969a1i 11 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ+ ⊆ ℝ)
16075a1i 11 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ+ ∈ (topGen‘ran (,)))
161114, 156, 157, 158, 159, 72, 71, 160dvmptres 23925 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝐴))) = (𝑥 ∈ ℝ+ ↦ 0))
162147relogcld 24568 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
163162recnd 10260 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
164147rpreccld 12075 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
165 dvrelog 24582 . . . . . . . . . . . . 13 (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))
166 relogf1o 24512 . . . . . . . . . . . . . . . . 17 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
167 f1of 6298 . . . . . . . . . . . . . . . . 17 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
168166, 167mp1i 13 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+):ℝ+⟶ℝ)
169168feqmptd 6411 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)))
170 fvres 6368 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ+ → ((log ↾ ℝ+)‘𝑥) = (log‘𝑥))
171170mpteq2ia 4892 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥))
172169, 171syl6eq 2810 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)))
173172oveq2d 6829 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (log ↾ ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝑥))))
174165, 173syl5reqr 2809 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
175114, 154, 155, 161, 163, 164, 174dvmptsub 23929 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥))))
176150, 175eqtrd 2794 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥))))
177 df-neg 10461 . . . . . . . . . . 11 -(1 / 𝑥) = (0 − (1 / 𝑥))
178177mpteq2i 4893 . . . . . . . . . 10 (𝑥 ∈ ℝ+ ↦ -(1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥)))
179176, 178syl6eqr 2812 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ -(1 / 𝑥)))
180 ovexd 6843 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) ∈ V)
181 nn0p1nn 11524 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
182127, 181syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ)
183 dvexp 23915 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1)))))
184182, 183syl 17 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1)))))
185122, 130, 180, 184, 132, 134dvmptdivc 23927 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))))
186127nn0cnd 11545 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℂ)
187186adantr 472 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℂ)
188 pncan 10479 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
189187, 98, 188sylancl 697 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
190189oveq2d 6829 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑((𝑗 + 1) − 1)) = (𝑦𝑗))
191190oveq2d 6829 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑦𝑗)))
192 facp1 13259 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1)))
193142, 192syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1)))
194 peano2cn 10400 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → (𝑗 + 1) ∈ ℂ)
195187, 194syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ∈ ℂ)
196141, 195mulcomd 10253 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((!‘𝑗) · (𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗)))
197193, 196eqtrd 2794 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗)))
198191, 197oveq12d 6831 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = (((𝑗 + 1) · (𝑦𝑗)) / ((𝑗 + 1) · (!‘𝑗))))
199182nnne0d 11257 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ≠ 0)
200199adantr 472 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ≠ 0)
201138, 141, 195, 144, 200divcan5d 11019 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦𝑗)) / ((𝑗 + 1) · (!‘𝑗))) = ((𝑦𝑗) / (!‘𝑗)))
202198, 201eqtrd 2794 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = ((𝑦𝑗) / (!‘𝑗)))
203202mpteq2dva 4896 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑦𝑗) / (!‘𝑗))))
204185, 203eqtrd 2794 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ ((𝑦𝑗) / (!‘𝑗))))
205 oveq1 6820 . . . . . . . . . 10 (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑(𝑗 + 1)) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)))
206205oveq1d 6828 . . . . . . . . 9 (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
207 oveq1 6820 . . . . . . . . . 10 (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦𝑗) = ((log‘(𝐴 / 𝑥))↑𝑗))
208207oveq1d 6828 . . . . . . . . 9 (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦𝑗) / (!‘𝑗)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
209114, 122, 123, 125, 136, 145, 179, 204, 206, 208dvmptco 23934 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))))
210110an32s 881 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ)
211164rpcnd 12067 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℂ)
212210, 211mulneg2d 10676 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
213 rpne0 12041 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+𝑥 ≠ 0)
214213adantl 473 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
215210, 115, 214divrecd 10996 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
216215negeqd 10467 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
217212, 216eqtr4d 2797 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))
218217mpteq2dva 4896 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)))
219209, 218eqtrd 2794 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦ -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)))
220114, 115, 116, 117, 118, 120, 219dvmptmul 23923 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))))
22190mulid2d 10250 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
222 simplr 809 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℝ+)
223109, 222rerpdivcld 12096 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℝ)
224223recnd 10260 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℂ)
225224, 80mulneg1d 10675 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))
226214an32s 881 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ≠ 0)
227110, 80, 226divcan1d 10994 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
228227negeqd 10467 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
229225, 228eqtrd 2794 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
230221, 229oveq12d 6831 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
23190, 110negsubd 10590 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
232230, 231eqtrd 2794 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
233232an32s 881 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
234233mpteq2dva 4896 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
235220, 234eqtrd 2794 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
23672, 71, 63, 76, 101, 103, 113, 235dvmptfsum 23937 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
237 oveq2 6821 . . . . . . . 8 (𝑘 = 𝑗 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑗))
238 fveq2 6352 . . . . . . . 8 (𝑘 = 𝑗 → (!‘𝑘) = (!‘𝑗))
239237, 238oveq12d 6831 . . . . . . 7 (𝑘 = 𝑗 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
240 oveq2 6821 . . . . . . . 8 (𝑘 = 𝑁 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑁))
241 fveq2 6352 . . . . . . . 8 (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
242240, 241oveq12d 6831 . . . . . . 7 (𝑘 = 𝑁 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
243239, 44, 25, 242, 18, 14telfsumo2 14734 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)))
24432oveq2d 6829 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))
245243, 244eqtrd 2794 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))
246245mpteq2dva 4896 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))
247236, 246eqtrd 2794 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))
24863, 3, 64, 77, 92, 100, 247dvmptadd 23922 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) = (𝑥 ∈ ℝ+ ↦ (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))))
249 pncan3 10481 . . . 4 ((1 ∈ ℂ ∧ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) → (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
25098, 97, 249sylancr 698 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
251250mpteq2dva 4896 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))))
25261, 248, 2513eqtrd 2798 1 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2139  wne 2932  Vcvv 3340  wss 3715  {cpr 4323  cmpt 4881  ran crn 5267  cres 5268  wf 6045  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6813  Fincfn 8121  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133  +∞cpnf 10263  cmin 10458  -cneg 10459   / cdiv 10876  cn 11212  0cn0 11484  cz 11569  cuz 11879  +crp 12025  (,)cioo 12368  ...cfz 12519  ..^cfzo 12659  cexp 13054  !cfa 13254  Σcsu 14615  TopOpenctopn 16284  topGenctg 16300  fldccnfld 19948   D cdv 23826  logclog 24500
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 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208
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 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ioc 12373  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-shft 14006  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-limsup 14401  df-clim 14418  df-rlim 14419  df-sum 14616  df-ef 14997  df-sin 14999  df-cos 15000  df-pi 15002  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-rest 16285  df-topn 16286  df-0g 16304  df-gsum 16305  df-topgen 16306  df-pt 16307  df-prds 16310  df-xrs 16364  df-qtop 16369  df-imas 16370  df-xps 16372  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20901  df-topon 20918  df-topsp 20939  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-nei 21104  df-lp 21142  df-perf 21143  df-cn 21233  df-cnp 21234  df-haus 21321  df-cmp 21392  df-tx 21567  df-hmeo 21760  df-fil 21851  df-fm 21943  df-flim 21944  df-flf 21945  df-xms 22326  df-ms 22327  df-tms 22328  df-cncf 22882  df-limc 23829  df-dv 23830  df-log 24502
This theorem is referenced by:  logexprlim  25149
  Copyright terms: Public domain W3C validator