This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↾ ℝ )