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

Theorem advlogexp 24695
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 12983 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0...𝑁) ∈ Fin)
2 rpcn 12043 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
32adantl 473 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
4 rpdivcl 12057 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈ ℝ+)
54adantlr 706 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈ ℝ+)
65relogcld 24663 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℝ)
7 elfznn0 12643 . . . . . . . . 9 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
8 reexpcl 13087 . . . . . . . . 9 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ)
96, 7, 8syl2an 589 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ)
107adantl 473 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
11 faccl 13277 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
1210, 11syl 17 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
139, 12nndivred 11328 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℝ)
1413recnd 10324 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℂ)
151, 3, 14fsummulc2 14803 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))
16 simplr 785 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ ℕ0)
17 nn0uz 11925 . . . . . . 7 0 = (ℤ‘0)
1816, 17syl6eleq 2854 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ‘0))
193adantr 472 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℂ)
2019, 14mulcld 10316 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ)
21 oveq2 6852 . . . . . . . 8 (𝑘 = 0 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑0))
22 fveq2 6377 . . . . . . . . 9 (𝑘 = 0 → (!‘𝑘) = (!‘0))
23 fac0 13270 . . . . . . . . 9 (!‘0) = 1
2422, 23syl6eq 2815 . . . . . . . 8 (𝑘 = 0 → (!‘𝑘) = 1)
2521, 24oveq12d 6862 . . . . . . 7 (𝑘 = 0 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑0) / 1))
2625oveq2d 6860 . . . . . 6 (𝑘 = 0 → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)))
2718, 20, 26fsum1p 14770 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))))
286recnd 10324 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℂ)
2928exp0d 13212 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((log‘(𝐴 / 𝑥))↑0) = 1)
3029oveq1d 6859 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑0) / 1) = (1 / 1))
31 1div1e1 10973 . . . . . . . . 9 (1 / 1) = 1
3230, 31syl6eq 2815 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑0) / 1) = 1)
3332oveq2d 6860 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = (𝑥 · 1))
343mulid1d 10313 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥)
3533, 34eqtrd 2799 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = 𝑥)
36 1zzd 11658 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℤ)
37 nn0z 11650 . . . . . . . . 9 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
3837ad2antlr 718 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈ ℤ)
39 fz1ssfz0 12646 . . . . . . . . . 10 (1...𝑁) ⊆ (0...𝑁)
4039sseli 3759 . . . . . . . . 9 (𝑘 ∈ (1...𝑁) → 𝑘 ∈ (0...𝑁))
4140, 20sylan2 586 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ)
42 oveq2 6852 . . . . . . . . . 10 (𝑘 = (𝑗 + 1) → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)))
43 fveq2 6377 . . . . . . . . . 10 (𝑘 = (𝑗 + 1) → (!‘𝑘) = (!‘(𝑗 + 1)))
4442, 43oveq12d 6862 . . . . . . . . 9 (𝑘 = (𝑗 + 1) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
4544oveq2d 6860 . . . . . . . 8 (𝑘 = (𝑗 + 1) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
4636, 36, 38, 41, 45fsumshftm 14800 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
47 0p1e1 11403 . . . . . . . . . 10 (0 + 1) = 1
4847oveq1i 6854 . . . . . . . . 9 ((0 + 1)...𝑁) = (1...𝑁)
4948sumeq1i 14716 . . . . . . . 8 Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))
5049a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))
51 1m1e0 11346 . . . . . . . . . 10 (1 − 1) = 0
5251oveq1i 6854 . . . . . . . . 9 ((1 − 1)..^𝑁) = (0..^𝑁)
53 fzoval 12682 . . . . . . . . . 10 (𝑁 ∈ ℤ → ((1 − 1)..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5438, 53syl 17 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((1 − 1)..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5552, 54syl5eqr 2813 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0..^𝑁) = ((1 − 1)...(𝑁 − 1)))
5655sumeq1d 14719 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
5746, 50, 563eqtr4d 2809 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))
5835, 57oveq12d 6862 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))
5915, 27, 583eqtrd 2803 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))
6059mpteq2dva 4905 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))))
6160oveq2d 6860 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))))
62 reelprrecn 10283 . . . 4 ℝ ∈ {ℝ, ℂ}
6362a1i 11 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ ∈ {ℝ, ℂ})
64 1cnd 10290 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
65 recn 10281 . . . . 5 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
6665adantl 473 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
67 1cnd 10290 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
6863dvmptid 24014 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
69 rpssre 12038 . . . . 5 + ⊆ ℝ
7069a1i 11 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ+ ⊆ ℝ)
71 eqid 2765 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
7271tgioo2 22888 . . . 4 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
73 ioorp 12456 . . . . . 6 (0(,)+∞) = ℝ+
74 iooretop 22851 . . . . . 6 (0(,)+∞) ∈ (topGen‘ran (,))
7573, 74eqeltrri 2841 . . . . 5 + ∈ (topGen‘ran (,))
7675a1i 11 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → ℝ+ ∈ (topGen‘ran (,)))
7763, 66, 67, 68, 70, 72, 71, 76dvmptres 24020 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+𝑥)) = (𝑥 ∈ ℝ+ ↦ 1))
78 fzofi 12984 . . . . 5 (0..^𝑁) ∈ Fin
7978a1i 11 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (0..^𝑁) ∈ Fin)
803adantr 472 . . . . 5 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℂ)
81 elfzonn0 12724 . . . . . . . . 9 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℕ0)
82 peano2nn0 11582 . . . . . . . . 9 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ0)
8381, 82syl 17 . . . . . . . 8 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ ℕ0)
84 reexpcl 13087 . . . . . . . 8 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ (𝑗 + 1) ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ)
856, 83, 84syl2an 589 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ)
8683adantl 473 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ0)
87 faccl 13277 . . . . . . . 8 ((𝑗 + 1) ∈ ℕ0 → (!‘(𝑗 + 1)) ∈ ℕ)
8886, 87syl 17 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ)
8985, 88nndivred 11328 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℝ)
9089recnd 10324 . . . . 5 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
9180, 90mulcld 10316 . . . 4 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
9279, 91fsumcl 14752 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
936, 16reexpcld 13235 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((log‘(𝐴 / 𝑥))↑𝑁) ∈ ℝ)
94 faccl 13277 . . . . . . 7 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
9594ad2antlr 718 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (!‘𝑁) ∈ ℕ)
9693, 95nndivred 11328 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℝ)
9796recnd 10324 . . . 4 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ)
98 ax-1cn 10249 . . . 4 1 ∈ ℂ
99 subcl 10536 . . . 4 (((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈ ℂ)
10097, 98, 99sylancl 580 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈ ℂ)
10178a1i 11 . . . . 5 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (0..^𝑁) ∈ Fin)
10291an32s 642 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
1031023impa 1136 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ)
104 reexpcl 13087 . . . . . . . . . . 11 (((log‘(𝐴 / 𝑥)) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ)
1056, 81, 104syl2an 589 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ)
10681adantl 473 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0)
107 faccl 13277 . . . . . . . . . . 11 (𝑗 ∈ ℕ0 → (!‘𝑗) ∈ ℕ)
108106, 107syl 17 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ)
109105, 108nndivred 11328 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℝ)
110109recnd 10324 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ)
11190, 110subcld 10648 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
112111an32s 642 . . . . . 6 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
1131123impa 1136 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ)
11462a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ ∈ {ℝ, ℂ})
1152adantl 473 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
116 1cnd 10290 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
11777adantr 472 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+𝑥)) = (𝑥 ∈ ℝ+ ↦ 1))
11890an32s 642 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
119 negex 10535 . . . . . . . 8 -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V
120119a1i 11 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V)
121 cnelprrecn 10284 . . . . . . . . . 10 ℂ ∈ {ℝ, ℂ}
122121a1i 11 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℂ ∈ {ℝ, ℂ})
12328adantlr 706 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) ∈ ℂ)
124 negex 10535 . . . . . . . . . 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 13088 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ (𝑗 + 1) ∈ ℕ0) → (𝑦↑(𝑗 + 1)) ∈ ℂ)
130126, 128, 129syl2anr 590 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑(𝑗 + 1)) ∈ ℂ)
131128, 87syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ)
132131nncnd 11294 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℂ)
133132adantr 472 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ∈ ℂ)
134131nnne0d 11324 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ≠ 0)
135134adantr 472 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ≠ 0)
136130, 133, 135divcld 11057 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ)
137 expcl 13088 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝑦𝑗) ∈ ℂ)
138126, 127, 137syl2anr 590 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦𝑗) ∈ ℂ)
139127, 107syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ)
140139nncnd 11294 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℂ)
141140adantr 472 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈ ℂ)
142127adantr 472 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℕ0)
143142, 107syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈ ℕ)
144143nnne0d 11324 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ≠ 0)
145138, 141, 144divcld 11057 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦𝑗) / (!‘𝑗)) ∈ ℂ)
146 simplll 791 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝐴 ∈ ℝ+)
147 simpr 477 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
148146, 147relogdivd 24666 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘(𝐴 / 𝑥)) = ((log‘𝐴) − (log‘𝑥)))
149148mpteq2dva 4905 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥))))
150149oveq2d 6860 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (ℝ D (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥)))))
151 relogcl 24616 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
152151ad2antrr 717 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℝ)
153152recnd 10324 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℂ)
154153adantr 472 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝐴) ∈ ℂ)
155 0cnd 10288 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 0 ∈ ℂ)
156153adantr 472 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (log‘𝐴) ∈ ℂ)
157 0cnd 10288 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℂ)
158114, 153dvmptc 24015 . . . . . . . . . . . . 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 24020 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝐴))) = (𝑥 ∈ ℝ+ ↦ 0))
162147relogcld 24663 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
163162recnd 10324 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
164147rpreccld 12083 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
165 dvrelog 24677 . . . . . . . . . . . . 13 (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))
166 relogf1o 24607 . . . . . . . . . . . . . . . . 17 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
167 f1of 6322 . . . . . . . . . . . . . . . . 17 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
168166, 167mp1i 13 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+):ℝ+⟶ℝ)
169168feqmptd 6440 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)))
170 fvres 6396 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ+ → ((log ↾ ℝ+)‘𝑥) = (log‘𝑥))
171170mpteq2ia 4901 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥))
172169, 171syl6eq 2815 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)))
173172oveq2d 6860 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (log ↾ ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝑥))))
174165, 173syl5reqr 2814 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
175114, 154, 155, 161, 163, 164, 174dvmptsub 24024 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ ((log‘𝐴) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥))))
176150, 175eqtrd 2799 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥))))
177 df-neg 10525 . . . . . . . . . . 11 -(1 / 𝑥) = (0 − (1 / 𝑥))
178177mpteq2i 4902 . . . . . . . . . 10 (𝑥 ∈ ℝ+ ↦ -(1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (0 − (1 / 𝑥)))
179176, 178syl6eqr 2817 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ -(1 / 𝑥)))
180 ovexd 6878 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) ∈ V)
181 nn0p1nn 11581 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
182127, 181syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ)
183 dvexp 24010 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1)))))
184182, 183syl 17 . . . . . . . . . . 11 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1)))))
185122, 130, 180, 184, 132, 134dvmptdivc 24022 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))))
186127nn0cnd 11602 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℂ)
187186adantr 472 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℂ)
188 pncan 10543 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
189187, 98, 188sylancl 580 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
190189oveq2d 6860 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑((𝑗 + 1) − 1)) = (𝑦𝑗))
191190oveq2d 6860 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑦𝑗)))
192 facp1 13272 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1)))
193142, 192syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1)))
194 peano2cn 10464 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℂ → (𝑗 + 1) ∈ ℂ)
195187, 194syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ∈ ℂ)
196141, 195mulcomd 10317 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((!‘𝑗) · (𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗)))
197193, 196eqtrd 2799 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗)))
198191, 197oveq12d 6862 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = (((𝑗 + 1) · (𝑦𝑗)) / ((𝑗 + 1) · (!‘𝑗))))
199182nnne0d 11324 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ≠ 0)
200199adantr 472 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ≠ 0)
201138, 141, 195, 144, 200divcan5d 11083 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦𝑗)) / ((𝑗 + 1) · (!‘𝑗))) = ((𝑦𝑗) / (!‘𝑗)))
202198, 201eqtrd 2799 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = ((𝑦𝑗) / (!‘𝑗)))
203202mpteq2dva 4905 . . . . . . . . . 10 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑦𝑗) / (!‘𝑗))))
204185, 203eqtrd 2799 . . . . . . . . 9 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ ((𝑦𝑗) / (!‘𝑗))))
205 oveq1 6851 . . . . . . . . . 10 (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑(𝑗 + 1)) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)))
206205oveq1d 6859 . . . . . . . . 9 (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
207 oveq1 6851 . . . . . . . . . 10 (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦𝑗) = ((log‘(𝐴 / 𝑥))↑𝑗))
208207oveq1d 6859 . . . . . . . . 9 (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦𝑗) / (!‘𝑗)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
209114, 122, 123, 125, 136, 145, 179, 204, 206, 208dvmptco 24029 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))))
210110an32s 642 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ)
211164rpcnd 12075 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℂ)
212210, 211mulneg2d 10740 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
213 rpne0 12049 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+𝑥 ≠ 0)
214213adantl 473 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
215210, 115, 214divrecd 11060 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
216215negeqd 10531 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥)))
217212, 216eqtr4d 2802 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))
218217mpteq2dva 4905 . . . . . . . 8 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)))
219209, 218eqtrd 2799 . . . . . . 7 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦ -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)))
220114, 115, 116, 117, 118, 120, 219dvmptmul 24018 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))))
22190mulid2d 10314 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))
222 simplr 785 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℝ+)
223109, 222rerpdivcld 12104 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℝ)
224223recnd 10324 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℂ)
225224, 80mulneg1d 10739 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))
226214an32s 642 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ≠ 0)
227110, 80, 226divcan1d 11058 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
228227negeqd 10531 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
229225, 228eqtrd 2799 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
230221, 229oveq12d 6862 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
23190, 110negsubd 10654 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
232230, 231eqtrd 2799 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
233232an32s 642 . . . . . . 7 ((((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))
234233mpteq2dva 4905 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
235220, 234eqtrd 2799 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
23672, 71, 63, 76, 101, 103, 113, 235dvmptfsum 24032 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))))
237 oveq2 6852 . . . . . . . 8 (𝑘 = 𝑗 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑗))
238 fveq2 6377 . . . . . . . 8 (𝑘 = 𝑗 → (!‘𝑘) = (!‘𝑗))
239237, 238oveq12d 6862 . . . . . . 7 (𝑘 = 𝑗 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))
240 oveq2 6852 . . . . . . . 8 (𝑘 = 𝑁 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑁))
241 fveq2 6377 . . . . . . . 8 (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
242240, 241oveq12d 6862 . . . . . . 7 (𝑘 = 𝑁 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
243239, 44, 25, 242, 18, 14telfsumo2 14822 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)))
24432oveq2d 6860 . . . . . 6 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))
245243, 244eqtrd 2799 . . . . 5 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))
246245mpteq2dva 4905 . . . 4 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))
247236, 246eqtrd 2799 . . 3 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))
24863, 3, 64, 77, 92, 100, 247dvmptadd 24017 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) = (𝑥 ∈ ℝ+ ↦ (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))))
249 pncan3 10545 . . . 4 ((1 ∈ ℂ ∧ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) → (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
25098, 97, 249sylancr 581 . . 3 (((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) ∧ 𝑥 ∈ ℝ+) → (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))
251250mpteq2dva 4905 . 2 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (𝑥 ∈ ℝ+ ↦ (1 + ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))))
25261, 248, 2513eqtrd 2803 1 ((𝐴 ∈ ℝ+𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wne 2937  Vcvv 3350  wss 3734  {cpr 4338  cmpt 4890  ran crn 5280  cres 5281  wf 6066  1-1-ontowf1o 6069  cfv 6070  (class class class)co 6844  Fincfn 8162  cc 10189  cr 10190  0cc0 10191  1c1 10192   + caddc 10194   · cmul 10196  +∞cpnf 10327  cmin 10522  -cneg 10523   / cdiv 10940  cn 11276  0cn0 11540  cz 11626  cuz 11889  +crp 12031  (,)cioo 12380  ...cfz 12536  ..^cfzo 12676  cexp 13070  !cfa 13267  Σcsu 14704  TopOpenctopn 16351  topGenctg 16367  fldccnfld 20022   D cdv 23921  logclog 24595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-inf2 8755  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269  ax-addf 10270  ax-mulf 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097  df-om 7266  df-1st 7368  df-2nd 7369  df-supp 7500  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-pm 8065  df-ixp 8116  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-fsupp 8485  df-fi 8526  df-sup 8557  df-inf 8558  df-oi 8624  df-card 9018  df-cda 9245  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-z 11627  df-dec 11744  df-uz 11890  df-q 11993  df-rp 12032  df-xneg 12149  df-xadd 12150  df-xmul 12151  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12537  df-fzo 12677  df-fl 12804  df-mod 12880  df-seq 13012  df-exp 13071  df-fac 13268  df-bc 13297  df-hash 13325  df-shft 14095  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-limsup 14490  df-clim 14507  df-rlim 14508  df-sum 14705  df-ef 15083  df-sin 15085  df-cos 15086  df-pi 15088  df-struct 16135  df-ndx 16136  df-slot 16137  df-base 16139  df-sets 16140  df-ress 16141  df-plusg 16230  df-mulr 16231  df-starv 16232  df-sca 16233  df-vsca 16234  df-ip 16235  df-tset 16236  df-ple 16237  df-ds 16239  df-unif 16240  df-hom 16241  df-cco 16242  df-rest 16352  df-topn 16353  df-0g 16371  df-gsum 16372  df-topgen 16373  df-pt 16374  df-prds 16377  df-xrs 16431  df-qtop 16436  df-imas 16437  df-xps 16439  df-mre 16515  df-mrc 16516  df-acs 16518  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-submnd 17605  df-mulg 17811  df-cntz 18016  df-cmn 18464  df-psmet 20014  df-xmet 20015  df-met 20016  df-bl 20017  df-mopn 20018  df-fbas 20019  df-fg 20020  df-cnfld 20023  df-top 20981  df-topon 20998  df-topsp 21020  df-bases 21033  df-cld 21106  df-ntr 21107  df-cls 21108  df-nei 21185  df-lp 21223  df-perf 21224  df-cn 21314  df-cnp 21315  df-haus 21402  df-cmp 21473  df-tx 21648  df-hmeo 21841  df-fil 21932  df-fm 22024  df-flim 22025  df-flf 22026  df-xms 22407  df-ms 22408  df-tms 22409  df-cncf 22963  df-limc 23924  df-dv 23925  df-log 24597
This theorem is referenced by:  logexprlim  25244
  Copyright terms: Public domain W3C validator