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	$⊢ (A \in ℝ^{+} \land N \in ℕ_{0}) \to \frac{d (x \in ℝ^{+}⟼ x \sum_{k = 0}^{N} (\frac{{\log (\frac{A}{x})}^{k}}{k!}))}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ \frac{{\log (\frac{A}{x})}^{N}}{N!})$

Proof

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

Metamath Proof Explorer

Theorem advlogexp

Proof