dvrelog

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

		Ref	Expression
	Assertion	dvrelog	$⊢ ℝ D ({log ↾}_{ℝ^{+}}) = (x \in ℝ^{+} ⟼ \frac{1}{x})$

Proof

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

Metamath Proof Explorer

Theorem dvrelog

Proof