Theorem dvrelog

Description: The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Assertion	dvrelog	⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		dfrelog	⊢ ( log ↾ ℝ+ ) = ◡ ( exp ↾ ℝ )
2	1	oveq2i	⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( ℝ D ◡ ( exp ↾ ℝ ) )
3		reeff1o	⊢ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+
4		f1of	⊢ ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ → ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ )
5	3 4	ax-mp	⊢ ( exp ↾ ℝ ) : ℝ ⟶ ℝ+
6		rpssre	⊢ ℝ+ ⊆ ℝ
7		fss	⊢ ( ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ ∧ ℝ+ ⊆ ℝ ) → ( exp ↾ ℝ ) : ℝ ⟶ ℝ )
8	5 6 7	mp2an	⊢ ( exp ↾ ℝ ) : ℝ ⟶ ℝ
9		ax-resscn	⊢ ℝ ⊆ ℂ
10		efcn	⊢ exp ∈ ( ℂ –cn→ ℂ )
11		rescncf	⊢ ( ℝ ⊆ ℂ → ( exp ∈ ( ℂ –cn→ ℂ ) → ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) )
12	9 10 11	mp2	⊢ ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℂ )
13		cncffvrn	⊢ ( ( ℝ ⊆ ℂ ∧ ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) → ( ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) ↔ ( exp ↾ ℝ ) : ℝ ⟶ ℝ ) )
14	9 12 13	mp2an	⊢ ( ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) ↔ ( exp ↾ ℝ ) : ℝ ⟶ ℝ )
15	8 14	mpbir	⊢ ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )
16	15	a1i	⊢ ( ⊤ → ( exp ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) )
17		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
18		eff	⊢ exp : ℂ ⟶ ℂ
19		ssid	⊢ ℂ ⊆ ℂ
20		dvef	⊢ ( ℂ D exp ) = exp
21	20	dmeqi	⊢ dom ( ℂ D exp ) = dom exp
22	18	fdmi	⊢ dom exp = ℂ
23	21 22	eqtri	⊢ dom ( ℂ D exp ) = ℂ
24	9 23	sseqtrri	⊢ ℝ ⊆ dom ( ℂ D exp )
25		dvres3	⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ exp : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D exp ) ) ) → ( ℝ D ( exp ↾ ℝ ) ) = ( ( ℂ D exp ) ↾ ℝ ) )
26	17 18 19 24 25	mp4an	⊢ ( ℝ D ( exp ↾ ℝ ) ) = ( ( ℂ D exp ) ↾ ℝ )
27	20	reseq1i	⊢ ( ( ℂ D exp ) ↾ ℝ ) = ( exp ↾ ℝ )
28	26 27	eqtri	⊢ ( ℝ D ( exp ↾ ℝ ) ) = ( exp ↾ ℝ )
29	28	dmeqi	⊢ dom ( ℝ D ( exp ↾ ℝ ) ) = dom ( exp ↾ ℝ )
30	5	fdmi	⊢ dom ( exp ↾ ℝ ) = ℝ
31	29 30	eqtri	⊢ dom ( ℝ D ( exp ↾ ℝ ) ) = ℝ
32	31	a1i	⊢ ( ⊤ → dom ( ℝ D ( exp ↾ ℝ ) ) = ℝ )
33		0nrp	⊢ ¬ 0 ∈ ℝ+
34	28	rneqi	⊢ ran ( ℝ D ( exp ↾ ℝ ) ) = ran ( exp ↾ ℝ )
35		f1ofo	⊢ ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ → ( exp ↾ ℝ ) : ℝ –onto→ ℝ+ )
36		forn	⊢ ( ( exp ↾ ℝ ) : ℝ –onto→ ℝ+ → ran ( exp ↾ ℝ ) = ℝ+ )
37	3 35 36	mp2b	⊢ ran ( exp ↾ ℝ ) = ℝ+
38	34 37	eqtri	⊢ ran ( ℝ D ( exp ↾ ℝ ) ) = ℝ+
39	38	eleq2i	⊢ ( 0 ∈ ran ( ℝ D ( exp ↾ ℝ ) ) ↔ 0 ∈ ℝ+ )
40	33 39	mtbir	⊢ ¬ 0 ∈ ran ( ℝ D ( exp ↾ ℝ ) )
41	40	a1i	⊢ ( ⊤ → ¬ 0 ∈ ran ( ℝ D ( exp ↾ ℝ ) ) )
42	3	a1i	⊢ ( ⊤ → ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ )
43	16 32 41 42	dvcnvre	⊢ ( ⊤ → ( ℝ D ◡ ( exp ↾ ℝ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) ) ) )
44	43	mptru	⊢ ( ℝ D ◡ ( exp ↾ ℝ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) ) )
45	28	fveq1i	⊢ ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) = ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) )
46		f1ocnvfv2	⊢ ( ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) = 𝑥 )
47	3 46	mpan	⊢ ( 𝑥 ∈ ℝ+ → ( ( exp ↾ ℝ ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) = 𝑥 )
48	45 47	syl5eq	⊢ ( 𝑥 ∈ ℝ+ → ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) = 𝑥 )
49	48	oveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) ) = ( 1 / 𝑥 ) )
50	49	mpteq2ia	⊢ ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( ( ℝ D ( exp ↾ ℝ ) ) ‘ ( ◡ ( exp ↾ ℝ ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
51	44 50	eqtri	⊢ ( ℝ D ◡ ( exp ↾ ℝ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
52	2 51	eqtri	⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )