Theorem advlog

Description: The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016)

	Ref	Expression
Assertion	advlog	$$⊢\frac{d\left(x\in {ℝ}^{+}⟼x\left(\log x-1\right)\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\log x\right)$$

Proof

Step	Hyp	Ref	Expression
1		reelprrecn	$$⊢ℝ\in \left\{ℝ,ℂ\right\}$$
2	1	a1i	$$⊢\top \to ℝ\in \left\{ℝ,ℂ\right\}$$
3		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
4	3	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to x\in ℝ$$
5	4	recnd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to x\in ℂ$$
6		1cnd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to 1\in ℂ$$
7		recn	$$⊢x\in ℝ\to x\in ℂ$$
8	7	adantl	$$⊢\left(\top \wedge x\in ℝ\right)\to x\in ℂ$$
9		1red	$$⊢\left(\top \wedge x\in ℝ\right)\to 1\in ℝ$$
10	2	dvmptid	$$⊢\top \to \frac{d\left(x\in ℝ⟼x\right)}{d_{ℝ}x}=\left(x\in ℝ⟼1\right)$$
11		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
12	11	a1i	$$⊢\top \to {ℝ}^{+}\subseteq ℝ$$
13		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
14	13	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
15		ioorp	$$⊢\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$$
16		iooretop	$$⊢\left(0,\mathrm{+\infty }\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
17	15 16	eqeltrri	$$⊢{ℝ}^{+}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
18	17	a1i	$$⊢\top \to {ℝ}^{+}\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
19	2 8 9 10 12 14 13 18	dvmptres	$$⊢\top \to \frac{d\left(x\in {ℝ}^{+}⟼x\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼1\right)$$
20		relogcl	$$⊢x\in {ℝ}^{+}\to \log x\in ℝ$$
21	20	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \log x\in ℝ$$
22		peano2rem	$$⊢\log x\in ℝ\to \log x-1\in ℝ$$
23	21 22	syl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \log x-1\in ℝ$$
24	23	recnd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \log x-1\in ℂ$$
25		rpreccl	$$⊢x\in {ℝ}^{+}\to \frac{1}{x}\in {ℝ}^{+}$$
26	25	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \frac{1}{x}\in {ℝ}^{+}$$
27	26	rpcnd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \frac{1}{x}\in ℂ$$
28	21	recnd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \log x\in ℂ$$
29		relogf1o	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$
30		f1of	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
31	29 30	mp1i	$$⊢\top \to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
32	31	feqmptd	$$⊢\top \to {log\upharpoonright }_{{ℝ}^{+}}=\left(x\in {ℝ}^{+}⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)\right)$$
33		fvres	$$⊢x\in {ℝ}^{+}\to \left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)=\log x$$
34	33	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)\right)=\left(x\in {ℝ}^{+}⟼\log x\right)$$
35	32 34	eqtrdi	$$⊢\top \to {log\upharpoonright }_{{ℝ}^{+}}=\left(x\in {ℝ}^{+}⟼\log x\right)$$
36	35	oveq2d	$$⊢\top \to ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\frac{d\left(x\in {ℝ}^{+}⟼\log x\right)}{d_{ℝ}x}$$
37		dvrelog	$$⊢ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
38	36 37	eqtr3di	$$⊢\top \to \frac{d\left(x\in {ℝ}^{+}⟼\log x\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
39		0cnd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to 0\in ℂ$$
40		1cnd	$$⊢\left(\top \wedge x\in ℝ\right)\to 1\in ℂ$$
41		0cnd	$$⊢\left(\top \wedge x\in ℝ\right)\to 0\in ℂ$$
42		1cnd	$$⊢\top \to 1\in ℂ$$
43	2 42	dvmptc	$$⊢\top \to \frac{d\left(x\in ℝ⟼1\right)}{d_{ℝ}x}=\left(x\in ℝ⟼0\right)$$
44	2 40 41 43 12 14 13 18	dvmptres	$$⊢\top \to \frac{d\left(x\in {ℝ}^{+}⟼1\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼0\right)$$
45	2 28 27 38 6 39 44	dvmptsub	$$⊢\top \to \frac{d\left(x\in {ℝ}^{+}⟼\log x-1\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\left(\frac{1}{x}\right)-0\right)$$
46	27	subid1d	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \left(\frac{1}{x}\right)-0=\frac{1}{x}$$
47	46	mpteq2dva	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\left(\frac{1}{x}\right)-0\right)=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
48	45 47	eqtrd	$$⊢\top \to \frac{d\left(x\in {ℝ}^{+}⟼\log x-1\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
49	2 5 6 19 24 27 48	dvmptmul	$$⊢\top \to \frac{d\left(x\in {ℝ}^{+}⟼x\left(\log x-1\right)\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼1\left(\log x-1\right)+\left(\frac{1}{x}\right)x\right)$$
50	24	mullidd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to 1\left(\log x-1\right)=\log x-1$$
51		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
52	51	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to x\ne 0$$
53	5 52	recid2d	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \left(\frac{1}{x}\right)x=1$$
54	50 53	oveq12d	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to 1\left(\log x-1\right)+\left(\frac{1}{x}\right)x=\log x-1+1$$
55		ax-1cn	$$⊢1\in ℂ$$
56		npcan	$$⊢\left(\log x\in ℂ\wedge 1\in ℂ\right)\to \log x-1+1=\log x$$
57	28 55 56	sylancl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \log x-1+1=\log x$$
58	54 57	eqtrd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to 1\left(\log x-1\right)+\left(\frac{1}{x}\right)x=\log x$$
59	58	mpteq2dva	$$⊢\top \to \left(x\in {ℝ}^{+}⟼1\left(\log x-1\right)+\left(\frac{1}{x}\right)x\right)=\left(x\in {ℝ}^{+}⟼\log x\right)$$
60	49 59	eqtrd	$$⊢\top \to \frac{d\left(x\in {ℝ}^{+}⟼x\left(\log x-1\right)\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\log x\right)$$
61	60	mptru	$$⊢\frac{d\left(x\in {ℝ}^{+}⟼x\left(\log x-1\right)\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\log x\right)$$