Metamath Proof Explorer

Theorem advlogexp

Description: The antiderivative of a power of the logarithm. (Set A = 1 and multiply by ( -u 1 ) ^ N x. N ! to get the antiderivative of log ( x ) ^ N itself.) (Contributed by Mario Carneiro, 22-May-2016)

Ref Expression
Assertion advlogexp ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 0 ... 𝑁 ) ∈ Fin )
2 rpcn ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
3 2 adantl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
4 rpdivcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 / 𝑥 ) ∈ ℝ+ )
5 4 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 / 𝑥 ) ∈ ℝ+ )
6 5 relogcld ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ ( 𝐴 / 𝑥 ) ) ∈ ℝ )
7 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
8 reexpcl ⊢ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) ∈ ℝ )
9 6 7 8 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) ∈ ℝ )
10 7 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
11 10 faccld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
12 9 11 nndivred ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
13 12 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
14 1 3 13 fsummulc2 ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
15 simplr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑁 ∈ ℕ0 )
16 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
17 15 16 eleqtrdi ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
18 3 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑥 ∈ ℂ )
19 18 13 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℂ )
20 oveq2 ⊢ ( 𝑘 = 0 → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) = ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) )
21 fveq2 ⊢ ( 𝑘 = 0 → ( ! ‘ 𝑘 ) = ( ! ‘ 0 ) )
22 fac0 ⊢ ( ! ‘ 0 ) = 1
23 21 22 eqtrdi ⊢ ( 𝑘 = 0 → ( ! ‘ 𝑘 ) = 1 )
24 20 23 oveq12d ⊢ ( 𝑘 = 0 → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) )
25 24 oveq2d ⊢ ( 𝑘 = 0 → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) ) )
26 17 19 25 fsum1p ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) )
27 6 recnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ ( 𝐴 / 𝑥 ) ) ∈ ℂ )
28 27 exp0d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) = 1 )
29 28 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) = ( 1 / 1 ) )
30 1div1e1 ⊢ ( 1 / 1 ) = 1
31 29 30 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) = 1 )
32 31 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) ) = ( 𝑥 · 1 ) )
33 3 mulridd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · 1 ) = 𝑥 )
34 32 33 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) ) = 𝑥 )
35 1zzd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℤ )
36 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
37 36 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑁 ∈ ℤ )
38 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
39 38 sseli ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
40 39 19 sylan2 ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ∈ ℂ )
41 oveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) = ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) )
42 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ! ‘ 𝑘 ) = ( ! ‘ ( 𝑗 + 1 ) ) )
43 41 42 oveq12d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) )
44 43 oveq2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) )
45 35 35 37 40 44 fsumshftm ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) )
46 0p1e1 ⊢ ( 0 + 1 ) = 1
47 46 oveq1i ⊢ ( ( 0 + 1 ) ... 𝑁 ) = ( 1 ... 𝑁 )
48 47 sumeq1i ⊢ Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
49 48 a1i ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
50 1m1e0 ⊢ ( 1 − 1 ) = 0
51 50 oveq1i ⊢ ( ( 1 − 1 ) ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
52 fzoval ⊢ ( 𝑁 ∈ ℤ → ( ( 1 − 1 ) ..^ 𝑁 ) = ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) )
53 37 52 syl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 − 1 ) ..^ 𝑁 ) = ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) )
54 51 53 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 0 ..^ 𝑁 ) = ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) )
55 54 sumeq1d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) = Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) )
56 45 49 55 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) )
57 34 56 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) = ( 𝑥 + Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) )
58 14 26 57 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( 𝑥 + Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) )
59 58 mpteq2dva ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 + Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) ) )
60 59 oveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 + Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) ) ) )
61 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
62 61 a1i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ℝ ∈ { ℝ , ℂ } )
63 1cnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
64 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
65 64 adantl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
66 1cnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℂ )
67 62 dvmptid ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) )
68 rpssre ⊢ ℝ+ ⊆ ℝ
69 68 a1i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ℝ+ ⊆ ℝ )
70 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
71 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
72 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
73 iooretop ⊢ ( 0 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
74 72 73 eqeltrri ⊢ ℝ+ ∈ ( topGen ‘ ran (,) )
75 74 a1i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ℝ+ ∈ ( topGen ‘ ran (,) ) )
76 62 65 66 67 69 70 71 75 dvmptres ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ 1 ) )
77 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
78 77 a1i ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 0 ..^ 𝑁 ) ∈ Fin )
79 3 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑥 ∈ ℂ )
80 elfzonn0 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℕ0 )
81 peano2nn0 ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ0 )
82 80 81 syl ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ℕ0 )
83 reexpcl ⊢ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ∈ ℝ ∧ ( 𝑗 + 1 ) ∈ ℕ0 ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) ∈ ℝ )
84 6 82 83 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) ∈ ℝ )
85 82 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ℕ0 )
86 85 faccld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℕ )
87 84 86 nndivred ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
88 87 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ∈ ℂ )
89 79 88 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℂ )
90 78 89 fsumcl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℂ )
91 6 15 reexpcld ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) ∈ ℝ )
92 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
93 92 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ! ‘ 𝑁 ) ∈ ℕ )
94 91 93 nndivred ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ∈ ℝ )
95 94 recnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ∈ ℂ )
96 ax-1cn ⊢ 1 ∈ ℂ
97 subcl ⊢ ( ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) ∈ ℂ )
98 95 96 97 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) ∈ ℂ )
99 77 a1i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ..^ 𝑁 ) ∈ Fin )
100 89 an32s ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℂ )
101 100 3impa ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℂ )
102 reexpcl ⊢ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ∈ ℝ ∧ 𝑗 ∈ ℕ0 ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) ∈ ℝ )
103 6 80 102 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) ∈ ℝ )
104 80 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ℕ0 )
105 104 faccld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ! ‘ 𝑗 ) ∈ ℕ )
106 103 105 nndivred ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ∈ ℝ )
107 106 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ∈ ℂ )
108 88 107 subcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) ∈ ℂ )
109 108 an32s ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) ∈ ℂ )
110 109 3impa ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) ∈ ℂ )
111 61 a1i ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ℝ ∈ { ℝ , ℂ } )
112 2 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
113 1cnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
114 76 adantr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ 1 ) )
115 88 an32s ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ∈ ℂ )
116 negex ⊢ - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) ∈ V
117 116 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) ∈ V )
118 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
119 118 a1i ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ℂ ∈ { ℝ , ℂ } )
120 27 adantlr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ ( 𝐴 / 𝑥 ) ) ∈ ℂ )
121 negex ⊢ - ( 1 / 𝑥 ) ∈ V
122 121 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → - ( 1 / 𝑥 ) ∈ V )
123 id ⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ )
124 80 adantl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ℕ0 )
125 124 81 syl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ℕ0 )
126 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑗 + 1 ) ∈ ℕ0 ) → ( 𝑦 ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
127 123 125 126 syl2anr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
128 125 faccld ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℕ )
129 128 nncnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
130 129 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ! ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
131 128 nnne0d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ! ‘ ( 𝑗 + 1 ) ) ≠ 0 )
132 131 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ! ‘ ( 𝑗 + 1 ) ) ≠ 0 )
133 127 130 132 divcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝑦 ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ∈ ℂ )
134 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑗 ) ∈ ℂ )
135 123 124 134 syl2anr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝑗 ) ∈ ℂ )
136 124 faccld ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ! ‘ 𝑗 ) ∈ ℕ )
137 136 nncnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ! ‘ 𝑗 ) ∈ ℂ )
138 137 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ! ‘ 𝑗 ) ∈ ℂ )
139 124 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → 𝑗 ∈ ℕ0 )
140 139 faccld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ! ‘ 𝑗 ) ∈ ℕ )
141 140 nnne0d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ! ‘ 𝑗 ) ≠ 0 )
142 135 138 141 divcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝑦 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ∈ ℂ )
143 simplll ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
144 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
145 143 144 relogdivd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ ( 𝐴 / 𝑥 ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝑥 ) ) )
146 145 mpteq2dva ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ ( 𝐴 / 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝐴 ) − ( log ‘ 𝑥 ) ) ) )
147 146 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ ( 𝐴 / 𝑥 ) ) ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝐴 ) − ( log ‘ 𝑥 ) ) ) ) )
148 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
149 148 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
150 149 recnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
151 150 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℂ )
152 0cnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → 0 ∈ ℂ )
153 150 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ ) → ( log ‘ 𝐴 ) ∈ ℂ )
154 0cnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℂ )
155 111 150 dvmptc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( log ‘ 𝐴 ) ) ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
156 68 a1i ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ℝ+ ⊆ ℝ )
157 74 a1i ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ℝ+ ∈ ( topGen ‘ ran (,) ) )
158 111 153 154 155 156 70 71 157 dvmptres ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝐴 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ 0 ) )
159 144 relogcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
160 159 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
161 144 rpreccld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ+ )
162 relogf1o ⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ
163 f1of ⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
164 162 163 mp1i ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
165 164 feqmptd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) ) )
166 fvres ⊢ ( 𝑥 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
167 166 mpteq2ia ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) )
168 165 167 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
169 168 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( log ↾ ℝ+ ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) )
170 dvrelog ⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
171 169 170 eqtr3di ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
172 111 151 152 158 160 161 171 dvmptsub ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝐴 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 0 − ( 1 / 𝑥 ) ) ) )
173 147 172 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ ( 𝐴 / 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 0 − ( 1 / 𝑥 ) ) ) )
174 df-neg ⊢ - ( 1 / 𝑥 ) = ( 0 − ( 1 / 𝑥 ) )
175 174 mpteq2i ⊢ ( 𝑥 ∈ ℝ+ ↦ - ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 0 − ( 1 / 𝑥 ) ) )
176 173 175 eqtr4di ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ ( 𝐴 / 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ - ( 1 / 𝑥 ) ) )
177 ovexd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝑗 + 1 ) · ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ∈ V )
178 nn0p1nn ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ )
179 124 178 syl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ℕ )
180 dvexp ⊢ ( ( 𝑗 + 1 ) ∈ ℕ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( 𝑗 + 1 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑗 + 1 ) · ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) )
181 179 180 syl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( 𝑗 + 1 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑗 + 1 ) · ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) )
182 119 127 177 181 129 131 dvmptdivc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( 𝑗 + 1 ) · ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) )
183 124 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ℂ )
184 183 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → 𝑗 ∈ ℂ )
185 pncan ⊢ ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
186 184 96 185 sylancl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
187 186 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) = ( 𝑦 ↑ 𝑗 ) )
188 187 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝑗 + 1 ) · ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) = ( ( 𝑗 + 1 ) · ( 𝑦 ↑ 𝑗 ) ) )
189 facp1 ⊢ ( 𝑗 ∈ ℕ0 → ( ! ‘ ( 𝑗 + 1 ) ) = ( ( ! ‘ 𝑗 ) · ( 𝑗 + 1 ) ) )
190 139 189 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ! ‘ ( 𝑗 + 1 ) ) = ( ( ! ‘ 𝑗 ) · ( 𝑗 + 1 ) ) )
191 peano2cn ⊢ ( 𝑗 ∈ ℂ → ( 𝑗 + 1 ) ∈ ℂ )
192 184 191 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑗 + 1 ) ∈ ℂ )
193 138 192 mulcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( ! ‘ 𝑗 ) · ( 𝑗 + 1 ) ) = ( ( 𝑗 + 1 ) · ( ! ‘ 𝑗 ) ) )
194 190 193 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ! ‘ ( 𝑗 + 1 ) ) = ( ( 𝑗 + 1 ) · ( ! ‘ 𝑗 ) ) )
195 188 194 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝑗 + 1 ) · ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) = ( ( ( 𝑗 + 1 ) · ( 𝑦 ↑ 𝑗 ) ) / ( ( 𝑗 + 1 ) · ( ! ‘ 𝑗 ) ) ) )
196 179 nnne0d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ≠ 0 )
197 196 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑗 + 1 ) ≠ 0 )
198 135 138 192 141 197 divcan5d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝑗 + 1 ) · ( 𝑦 ↑ 𝑗 ) ) / ( ( 𝑗 + 1 ) · ( ! ‘ 𝑗 ) ) ) = ( ( 𝑦 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
199 195 198 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝑗 + 1 ) · ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑦 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
200 199 mpteq2dva ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℂ ↦ ( ( ( 𝑗 + 1 ) · ( 𝑦 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
201 182 200 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
202 oveq1 ⊢ ( 𝑦 = ( log ‘ ( 𝐴 / 𝑥 ) ) → ( 𝑦 ↑ ( 𝑗 + 1 ) ) = ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) )
203 202 oveq1d ⊢ ( 𝑦 = ( log ‘ ( 𝐴 / 𝑥 ) ) → ( ( 𝑦 ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) )
204 oveq1 ⊢ ( 𝑦 = ( log ‘ ( 𝐴 / 𝑥 ) ) → ( 𝑦 ↑ 𝑗 ) = ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) )
205 204 oveq1d ⊢ ( 𝑦 = ( log ‘ ( 𝐴 / 𝑥 ) ) → ( ( 𝑦 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
206 111 119 120 122 133 142 176 201 203 205 dvmptco ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · - ( 1 / 𝑥 ) ) ) )
207 107 an32s ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ∈ ℂ )
208 161 rpcnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℂ )
209 207 208 mulneg2d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · - ( 1 / 𝑥 ) ) = - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 1 / 𝑥 ) ) )
210 rpne0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
211 210 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
212 207 112 211 divrecd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) = ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 1 / 𝑥 ) ) )
213 212 negeqd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) = - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 1 / 𝑥 ) ) )
214 209 213 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · - ( 1 / 𝑥 ) ) = - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) )
215 214 mpteq2dva ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · - ( 1 / 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) ) )
216 206 215 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) ) )
217 111 112 113 114 115 117 216 dvmptmul ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 1 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) + ( - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) ) ) )
218 88 mullidd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 1 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) )
219 simplr ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑥 ∈ ℝ+ )
220 106 219 rerpdivcld ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) ∈ ℝ )
221 220 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) ∈ ℂ )
222 221 79 mulneg1d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) = - ( ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) )
223 211 an32s ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑥 ≠ 0 )
224 107 79 223 divcan1d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
225 224 negeqd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → - ( ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) = - ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
226 222 225 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) = - ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
227 218 226 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 1 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) + ( - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) ) = ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) + - ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
228 88 107 negsubd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) + - ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) = ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
229 227 228 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 1 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) + ( - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) ) = ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
230 229 an32s ⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) + ( - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) ) = ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
231 230 mpteq2dva ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( 1 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) + ( - ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) / 𝑥 ) · 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) ) )
232 217 231 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) ) )
233 70 71 62 75 99 101 110 232 dvmptfsum ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) ) )
234 oveq2 ⊢ ( 𝑘 = 𝑗 → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) = ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) )
235 fveq2 ⊢ ( 𝑘 = 𝑗 → ( ! ‘ 𝑘 ) = ( ! ‘ 𝑗 ) )
236 234 235 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
237 oveq2 ⊢ ( 𝑘 = 𝑁 → ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) = ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) )
238 fveq2 ⊢ ( 𝑘 = 𝑁 → ( ! ‘ 𝑘 ) = ( ! ‘ 𝑁 ) )
239 237 238 oveq12d ⊢ ( 𝑘 = 𝑁 → ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) )
240 236 43 24 239 17 13 telfsumo2 ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) = ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) ) )
241 31 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 0 ) / 1 ) ) = ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) )
242 240 241 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) = ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) )
243 242 mpteq2dva ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) − ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) ) )
244 233 243 eqtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) ) )
245 62 3 63 76 90 98 244 dvmptadd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 + Σ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( 𝑥 · ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ ( 𝑗 + 1 ) ) / ( ! ‘ ( 𝑗 + 1 ) ) ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 + ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) ) ) )
246 pncan3 ⊢ ( ( 1 ∈ ℂ ∧ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ∈ ℂ ) → ( 1 + ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) )
247 96 95 246 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 + ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) ) = ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) )
248 247 mpteq2dva ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ℝ+ ↦ ( 1 + ( ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) − 1 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) )
249 60 245 248 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0 ) → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( log ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) )