dvrelog3

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

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

Proof

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

Metamath Proof Explorer

Theorem dvrelog3

Proof