Theorem dvrelog2

Description: The derivative of the logarithm, ftc2 version. (Contributed by metakunt, 11-Aug-2024)

	Ref	Expression
Hypotheses	dvrelog2.1	$$⊢\phi \to A\in ℝ$$
	dvrelog2.2	$$⊢\phi \to B\in ℝ$$
	dvrelog2.3	$$⊢\phi \to 0<A$$
	dvrelog2.4	$$⊢\phi \to A\le B$$
	dvrelog2.5	$$⊢F=\left(x\in \left[A,B\right]⟼\log x\right)$$
	dvrelog2.6	$$⊢G=\left(x\in \left(A,B\right)⟼\frac{1}{x}\right)$$
Assertion	dvrelog2	$$⊢\phi \to ℝ\mathrm{D}F=G$$

Proof

Step	Hyp	Ref	Expression
1		dvrelog2.1	$$⊢\phi \to A\in ℝ$$
2		dvrelog2.2	$$⊢\phi \to B\in ℝ$$
3		dvrelog2.3	$$⊢\phi \to 0<A$$
4		dvrelog2.4	$$⊢\phi \to A\le B$$
5		dvrelog2.5	$$⊢F=\left(x\in \left[A,B\right]⟼\log x\right)$$
6		dvrelog2.6	$$⊢G=\left(x\in \left(A,B\right)⟼\frac{1}{x}\right)$$
7	5	a1i	$$⊢\phi \to F=\left(x\in \left[A,B\right]⟼\log x\right)$$
8	7	oveq2d	$$⊢\phi \to ℝ\mathrm{D}F=\frac{d\left(x\in \left[A,B\right]⟼\log x\right)}{d_{ℝ}x}$$
9		reelprrecn	$$⊢ℝ\in \left\{ℝ,ℂ\right\}$$
10	9	a1i	$$⊢\phi \to ℝ\in \left\{ℝ,ℂ\right\}$$
11		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
12		ax-resscn	$$⊢ℝ\subseteq ℂ$$
13	11 12	sstri	$$⊢{ℝ}^{+}\subseteq ℂ$$
14	13	sseli	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
15	14	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to x\in ℂ$$
16		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
17	16	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to x\ne 0$$
18	15 17	logcld	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \log x\in ℂ$$
19		1red	$$⊢x\in {ℝ}^{+}\to 1\in ℝ$$
20	11	sseli	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
21	19 20 16	redivcld	$$⊢x\in {ℝ}^{+}\to \frac{1}{x}\in ℝ$$
22	21	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \frac{1}{x}\in ℝ$$
23		logf1o	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log$$
24		f1of	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log\to log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
25	23 24	ax-mp	$$⊢log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
26	25	a1i	$$⊢\phi \to log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
27		0nrp	$$⊢\neg 0\in {ℝ}^{+}$$
28		disjsn	$$⊢{ℝ}^{+}\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in {ℝ}^{+}$$
29	27 28	mpbir	$$⊢{ℝ}^{+}\cap \left\{0\right\}=\varnothing$$
30		disjdif2	$$⊢{ℝ}^{+}\cap \left\{0\right\}=\varnothing \to {ℝ}^{+}\setminus \left\{0\right\}={ℝ}^{+}$$
31	29 30	ax-mp	$$⊢{ℝ}^{+}\setminus \left\{0\right\}={ℝ}^{+}$$
32		ssdif	$$⊢{ℝ}^{+}\subseteq ℂ\to {ℝ}^{+}\setminus \left\{0\right\}\subseteq ℂ\setminus \left\{0\right\}$$
33	13 32	ax-mp	$$⊢{ℝ}^{+}\setminus \left\{0\right\}\subseteq ℂ\setminus \left\{0\right\}$$
34	31 33	eqsstrri	$$⊢{ℝ}^{+}\subseteq ℂ\setminus \left\{0\right\}$$
35	34	a1i	$$⊢\phi \to {ℝ}^{+}\subseteq ℂ\setminus \left\{0\right\}$$
36	26 35	feqresmpt	$$⊢\phi \to {log\upharpoonright }_{{ℝ}^{+}}=\left(x\in {ℝ}^{+}⟼\log x\right)$$
37	36	eqcomd	$$⊢\phi \to \left(x\in {ℝ}^{+}⟼\log x\right)={log\upharpoonright }_{{ℝ}^{+}}$$
38	37	oveq2d	$$⊢\phi \to \frac{d\left(x\in {ℝ}^{+}⟼\log x\right)}{d_{ℝ}x}=ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)$$
39		dvrelog	$$⊢ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
40	39	a1i	$$⊢\phi \to ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
41	38 40	eqtrd	$$⊢\phi \to \frac{d\left(x\in {ℝ}^{+}⟼\log x\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
42		elicc2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(y\in \left[A,B\right]\leftrightarrow \left(y\in ℝ\wedge A\le y\wedge y\le B\right)\right)$$
43	1 2 42	syl2anc	$$⊢\phi \to \left(y\in \left[A,B\right]\leftrightarrow \left(y\in ℝ\wedge A\le y\wedge y\le B\right)\right)$$
44	43	biimpa	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to \left(y\in ℝ\wedge A\le y\wedge y\le B\right)$$
45	44	simp1d	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to y\in ℝ$$
46		0red	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to 0\in ℝ$$
47	1	adantr	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to A\in ℝ$$
48	3	adantr	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to 0<A$$
49	44	simp2d	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to A\le y$$
50	46 47 45 48 49	ltletrd	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to 0<y$$
51	45 50	jca	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to \left(y\in ℝ\wedge 0<y\right)$$
52		elrp	$$⊢y\in {ℝ}^{+}\leftrightarrow \left(y\in ℝ\wedge 0<y\right)$$
53	51 52	sylibr	$$⊢\left(\phi \wedge y\in \left[A,B\right]\right)\to y\in {ℝ}^{+}$$
54	53	ex	$$⊢\phi \to \left(y\in \left[A,B\right]\to y\in {ℝ}^{+}\right)$$
55	54	ssrdv	$$⊢\phi \to \left[A,B\right]\subseteq {ℝ}^{+}$$
56		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
57	56	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
58		iccntr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[A,B\right]\right)=\left(A,B\right)$$
59	1 2 58	syl2anc	$$⊢\phi \to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[A,B\right]\right)=\left(A,B\right)$$
60	10 18 22 41 55 57 56 59	dvmptres2	$$⊢\phi \to \frac{d\left(x\in \left[A,B\right]⟼\log x\right)}{d_{ℝ}x}=\left(x\in \left(A,B\right)⟼\frac{1}{x}\right)$$
61	8 60	eqtrd	$$⊢\phi \to ℝ\mathrm{D}F=\left(x\in \left(A,B\right)⟼\frac{1}{x}\right)$$
62	6	a1i	$$⊢\phi \to G=\left(x\in \left(A,B\right)⟼\frac{1}{x}\right)$$
63	62	eqcomd	$$⊢\phi \to \left(x\in \left(A,B\right)⟼\frac{1}{x}\right)=G$$
64	61 63	eqtrd	$$⊢\phi \to ℝ\mathrm{D}F=G$$