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

Proof

Step Hyp Ref Expression
1 df-ima ⊢ exp ↾ ran ⁡ log ℝ = ran ⁡ exp ↾ ran ⁡ log ↾ ℝ
2 relogrn ⊢ x ∈ ℝ → x ∈ 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 ↾ ℝ -1 ∧ ran ⁡ exp ↾ ℝ = ℝ +
9 7 8 mpbi ⊢ exp ↾ ℝ Fn ℝ ∧ Fun ⁡ exp ↾ ℝ -1 ∧ ran ⁡ exp ↾ ℝ = ℝ +
10 9 simp3i ⊢ ran ⁡ exp ↾ ℝ = ℝ +
11 1 6 10 3eqtri ⊢ exp ↾ ran ⁡ log ℝ = ℝ +
12 11 reseq2i ⊢ exp ↾ ran ⁡ log -1 ↾ exp ↾ ran ⁡ log ℝ = exp ↾ ran ⁡ log -1 ↾ ℝ +
13 5 cnveqi ⊢ exp ↾ ran ⁡ log ↾ ℝ -1 = exp ↾ ℝ -1
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 -1
18 17 funeqi ⊢ Fun ⁡ log ↔ Fun ⁡ exp ↾ ran ⁡ log -1
19 16 18 mpbi ⊢ Fun ⁡ exp ↾ ran ⁡ log -1
20 funcnvres ⊢ Fun ⁡ exp ↾ ran ⁡ log -1 → exp ↾ ran ⁡ log ↾ ℝ -1 = exp ↾ ran ⁡ log -1 ↾ exp ↾ ran ⁡ log ℝ
21 19 20 ax-mp ⊢ exp ↾ ran ⁡ log ↾ ℝ -1 = exp ↾ ran ⁡ log -1 ↾ exp ↾ ran ⁡ log ℝ
22 13 21 eqtr3i ⊢ exp ↾ ℝ -1 = exp ↾ ran ⁡ log -1 ↾ exp ↾ ran ⁡ log ℝ
23 17 reseq1i ⊢ log ↾ ℝ + = exp ↾ ran ⁡ log -1 ↾ ℝ +
24 12 22 23 3eqtr4ri ⊢ log ↾ ℝ + = exp ↾ ℝ -1