Theorem dvrelog3

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

	Ref	Expression
Hypotheses	dvrelog3.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	dvrelog3.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	dvrelog3.3	⊢ ( 𝜑 → 0 ≤ 𝐴 )
	dvrelog3.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	dvrelog3.5	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) )
	dvrelog3.6	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) )
Assertion	dvrelog3	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		dvrelog3.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		dvrelog3.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		dvrelog3.3	⊢ ( 𝜑 → 0 ≤ 𝐴 )
4		dvrelog3.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5		dvrelog3.5	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) )
6		dvrelog3.6	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) )
7	5	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) )
8	7	oveq2d	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) )
9		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
10	9	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
11		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
13		rpne0	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
15	12 14	logcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
16		1red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℝ )
17		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
19	16 18 14	redivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ )
20		logf1o	⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
21		f1of	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
22	20 21	ax-mp	⊢ log : ( ℂ ∖ { 0 } ) ⟶ ran log
23	22	a1i	⊢ ( 𝜑 → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
24		0nrp	⊢ ¬ 0 ∈ ℝ+
25		disjsn	⊢ ( ( ℝ+ ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ℝ+ )
26	24 25	mpbir	⊢ ( ℝ+ ∩ { 0 } ) = ∅
27		disjdif2	⊢ ( ( ℝ+ ∩ { 0 } ) = ∅ → ( ℝ+ ∖ { 0 } ) = ℝ+ )
28	26 27	ax-mp	⊢ ( ℝ+ ∖ { 0 } ) = ℝ+
29		rpssre	⊢ ℝ+ ⊆ ℝ
30		ax-resscn	⊢ ℝ ⊆ ℂ
31	29 30	sstri	⊢ ℝ+ ⊆ ℂ
32		ssdif	⊢ ( ℝ+ ⊆ ℂ → ( ℝ+ ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } ) )
33	31 32	ax-mp	⊢ ( ℝ+ ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } )
34	28 33	eqsstrri	⊢ ℝ+ ⊆ ( ℂ ∖ { 0 } )
35	34	a1i	⊢ ( 𝜑 → ℝ+ ⊆ ( ℂ ∖ { 0 } ) )
36	23 35	feqresmpt	⊢ ( 𝜑 → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
37	36	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) = ( log ↾ ℝ+ ) )
38	37	oveq2d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( ℝ D ( log ↾ ℝ+ ) ) )
39		dvrelog	⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
40	39	a1i	⊢ ( 𝜑 → ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
41	38 40	eqtrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
42		elioo2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵 ) ) )
43	1 2 42	syl2anc	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵 ) ) )
44	43	biimpa	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵 ) )
45	44	simp1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ )
46		0red	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
47	46	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ* )
48	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
49	45	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ* )
50	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ 𝐴 )
51	44	simp2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑦 )
52	47 48 49 50 51	xrlelttrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < 𝑦 )
53	45 52	jca	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) )
54		elrp	⊢ ( 𝑦 ∈ ℝ+ ↔ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) )
55	53 54	sylibr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ+ )
56	55	ex	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → 𝑦 ∈ ℝ+ ) )
57	56	ssrdv	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ+ )
58		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
59		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
60		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
61	60	a1i	⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
62		iooretop	⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
63	62	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
64		isopn3i	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
65	61 63 64	syl2anc	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
66	10 15 19 41 57 58 59 65	dvmptres2	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) )
67	8 66	eqtrd	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) )
68	6	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) )
69	68	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) = 𝐺 )
70	67 69	eqtrd	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )