Theorem dvrelog3

Description: The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		dvrelog3.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		dvrelog3.2	$$⊢\phi \to B\in {ℝ}^{*}$$
3		dvrelog3.3	$$⊢\phi \to 0\le A$$
4		dvrelog3.4	$$⊢\phi \to A\le B$$
5		dvrelog3.5	$$⊢F=\left(x\in \left(A,B\right)⟼\log x\right)$$
6		dvrelog3.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		rpcn	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
12	11	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to x\in ℂ$$
13		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
14	13	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to x\ne 0$$
15	12 14	logcld	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \log x\in ℂ$$
16		1red	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to 1\in ℝ$$
17		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
18	17	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to x\in ℝ$$
19	16 18 14	redivcld	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \frac{1}{x}\in ℝ$$
20		logf1o	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log$$
21		f1of	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log\to log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
22	20 21	ax-mp	$$⊢log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
23	22	a1i	$$⊢\phi \to log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
24		0nrp	$$⊢\neg 0\in {ℝ}^{+}$$
25		disjsn	$$⊢{ℝ}^{+}\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in {ℝ}^{+}$$
26	24 25	mpbir	$$⊢{ℝ}^{+}\cap \left\{0\right\}=\varnothing$$
27		disjdif2	$$⊢{ℝ}^{+}\cap \left\{0\right\}=\varnothing \to {ℝ}^{+}\setminus \left\{0\right\}={ℝ}^{+}$$
28	26 27	ax-mp	$$⊢{ℝ}^{+}\setminus \left\{0\right\}={ℝ}^{+}$$
29		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
30		ax-resscn	$$⊢ℝ\subseteq ℂ$$
31	29 30	sstri	$$⊢{ℝ}^{+}\subseteq ℂ$$
32		ssdif	$$⊢{ℝ}^{+}\subseteq ℂ\to {ℝ}^{+}\setminus \left\{0\right\}\subseteq ℂ\setminus \left\{0\right\}$$
33	31 32	ax-mp	$$⊢{ℝ}^{+}\setminus \left\{0\right\}\subseteq ℂ\setminus \left\{0\right\}$$
34	28 33	eqsstrri	$$⊢{ℝ}^{+}\subseteq ℂ\setminus \left\{0\right\}$$
35	34	a1i	$$⊢\phi \to {ℝ}^{+}\subseteq ℂ\setminus \left\{0\right\}$$
36	23 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		elioo2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(y\in \left(A,B\right)\leftrightarrow \left(y\in ℝ\wedge A<y\wedge y<B\right)\right)$$
43	1 2 42	syl2anc	$$⊢\phi \to \left(y\in \left(A,B\right)\leftrightarrow \left(y\in ℝ\wedge A<y\wedge y<B\right)\right)$$
44	43	biimpa	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to \left(y\in ℝ\wedge A<y\wedge y<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	46	rexrd	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to 0\in {ℝ}^{*}$$
48	1	adantr	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to A\in {ℝ}^{*}$$
49	45	rexrd	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to y\in {ℝ}^{*}$$
50	3	adantr	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to 0\le A$$
51	44	simp2d	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to A<y$$
52	47 48 49 50 51	xrlelttrd	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to 0<y$$
53	45 52	jca	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to \left(y\in ℝ\wedge 0<y\right)$$
54		elrp	$$⊢y\in {ℝ}^{+}\leftrightarrow \left(y\in ℝ\wedge 0<y\right)$$
55	53 54	sylibr	$$⊢\left(\phi \wedge y\in \left(A,B\right)\right)\to y\in {ℝ}^{+}$$
56	55	ex	$$⊢\phi \to \left(y\in \left(A,B\right)\to y\in {ℝ}^{+}\right)$$
57	56	ssrdv	$$⊢\phi \to \left(A,B\right)\subseteq {ℝ}^{+}$$
58		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
59	58	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
60		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
61	60	a1i	$$⊢\phi \to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
62		iooretop	$$⊢\left(A,B\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
63	62	a1i	$$⊢\phi \to \left(A,B\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
64		isopn3i	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge \left(A,B\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left(A,B\right)\right)=\left(A,B\right)$$
65	61 63 64	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)$$
66	10 15 19 41 57 59 58 65	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)$$
67	8 66	eqtrd	$$⊢\phi \to ℝ\mathrm{D}F=\left(x\in \left(A,B\right)⟼\frac{1}{x}\right)$$
68	6	a1i	$$⊢\phi \to G=\left(x\in \left(A,B\right)⟼\frac{1}{x}\right)$$
69	68	eqcomd	$$⊢\phi \to \left(x\in \left(A,B\right)⟼\frac{1}{x}\right)=G$$
70	67 69	eqtrd	$$⊢\phi \to ℝ\mathrm{D}F=G$$