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		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
71	70	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
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 71 70 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 71 70 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	71 70 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 ‘ ( 𝐴 / 𝑥 ) ) ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ) )