Theorem dfrelog

Description: The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008)

	Ref	Expression
Assertion	dfrelog	⊢ ( log ↾ ℝ+ ) = ◡ ( exp ↾ ℝ )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( ( exp ↾ ran log ) “ ℝ ) = ran ( ( exp ↾ ran log ) ↾ ℝ )
2		relogrn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ran log )
3	2	ssriv	⊢ ℝ ⊆ ran log
4		resabs1	⊢ ( ℝ ⊆ ran log → ( ( exp ↾ ran log ) ↾ ℝ ) = ( exp ↾ ℝ ) )
5	3 4	ax-mp	⊢ ( ( exp ↾ ran log ) ↾ ℝ ) = ( exp ↾ ℝ )
6	5	rneqi	⊢ ran ( ( exp ↾ ran log ) ↾ ℝ ) = ran ( exp ↾ ℝ )
7		reeff1o	⊢ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+
8		dff1o2	⊢ ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ↔ ( ( exp ↾ ℝ ) Fn ℝ ∧ Fun ◡ ( exp ↾ ℝ ) ∧ ran ( exp ↾ ℝ ) = ℝ+ ) )
9	7 8	mpbi	⊢ ( ( exp ↾ ℝ ) Fn ℝ ∧ Fun ◡ ( exp ↾ ℝ ) ∧ ran ( exp ↾ ℝ ) = ℝ+ )
10	9	simp3i	⊢ ran ( exp ↾ ℝ ) = ℝ+
11	1 6 10	3eqtri	⊢ ( ( exp ↾ ran log ) “ ℝ ) = ℝ+
12	11	reseq2i	⊢ ( ◡ ( exp ↾ ran log ) ↾ ( ( exp ↾ ran log ) “ ℝ ) ) = ( ◡ ( exp ↾ ran log ) ↾ ℝ+ )
13	5	cnveqi	⊢ ◡ ( ( exp ↾ ran log ) ↾ ℝ ) = ◡ ( exp ↾ ℝ )
14		logf1o	⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
15		f1ofun	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → Fun log )
16	14 15	ax-mp	⊢ Fun log
17		dflog2	⊢ log = ◡ ( exp ↾ ran log )
18	17	funeqi	⊢ ( Fun log ↔ Fun ◡ ( exp ↾ ran log ) )
19	16 18	mpbi	⊢ Fun ◡ ( exp ↾ ran log )
20		funcnvres	⊢ ( Fun ◡ ( exp ↾ ran log ) → ◡ ( ( exp ↾ ran log ) ↾ ℝ ) = ( ◡ ( exp ↾ ran log ) ↾ ( ( exp ↾ ran log ) “ ℝ ) ) )
21	19 20	ax-mp	⊢ ◡ ( ( exp ↾ ran log ) ↾ ℝ ) = ( ◡ ( exp ↾ ran log ) ↾ ( ( exp ↾ ran log ) “ ℝ ) )
22	13 21	eqtr3i	⊢ ◡ ( exp ↾ ℝ ) = ( ◡ ( exp ↾ ran log ) ↾ ( ( exp ↾ ran log ) “ ℝ ) )
23	17	reseq1i	⊢ ( log ↾ ℝ+ ) = ( ◡ ( exp ↾ ran log ) ↾ ℝ+ )
24	12 22 23	3eqtr4ri	⊢ ( log ↾ ℝ+ ) = ◡ ( exp ↾ ℝ )