Theorem dvrelog2

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

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

Proof

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