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

Metamath Proof Explorer

Theorem relogf1o

Description: The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion relogf1o ⊢ log ↾ ℝ + : ℝ + ⟶ 1-1 onto ℝ

Proof

Step Hyp Ref Expression
1 eff1o2 ⊢ exp ↾ ran ⁡ log : ran ⁡ log ⟶ 1-1 onto ℂ ∖ 0
2 dff1o3 ⊢ exp ↾ ran ⁡ log : ran ⁡ log ⟶ 1-1 onto ℂ ∖ 0 ↔ exp ↾ ran ⁡ log : ran ⁡ log ⟶ onto ℂ ∖ 0 ∧ Fun ⁡ exp ↾ ran ⁡ log -1
3 2 simprbi ⊢ exp ↾ ran ⁡ log : ran ⁡ log ⟶ 1-1 onto ℂ ∖ 0 → Fun ⁡ exp ↾ ran ⁡ log -1
4 1 3 ax-mp ⊢ Fun ⁡ exp ↾ ran ⁡ log -1
5 reeff1o ⊢ exp ↾ ℝ : ℝ ⟶ 1-1 onto ℝ +
6 relogrn ⊢ x ∈ ℝ → x ∈ ran ⁡ log
7 6 ssriv ⊢ ℝ ⊆ ran ⁡ log
8 resabs1 ⊢ ℝ ⊆ ran ⁡ log → exp ↾ ran ⁡ log ↾ ℝ = exp ↾ ℝ
9 f1oeq1 ⊢ exp ↾ ran ⁡ log ↾ ℝ = exp ↾ ℝ → exp ↾ ran ⁡ log ↾ ℝ : ℝ ⟶ 1-1 onto ℝ + ↔ exp ↾ ℝ : ℝ ⟶ 1-1 onto ℝ +
10 7 8 9 mp2b ⊢ exp ↾ ran ⁡ log ↾ ℝ : ℝ ⟶ 1-1 onto ℝ + ↔ exp ↾ ℝ : ℝ ⟶ 1-1 onto ℝ +
11 5 10 mpbir ⊢ exp ↾ ran ⁡ log ↾ ℝ : ℝ ⟶ 1-1 onto ℝ +
12 f1orescnv ⊢ Fun ⁡ exp ↾ ran ⁡ log -1 ∧ exp ↾ ran ⁡ log ↾ ℝ : ℝ ⟶ 1-1 onto ℝ + → exp ↾ ran ⁡ log -1 ↾ ℝ + : ℝ + ⟶ 1-1 onto ℝ
13 4 11 12 mp2an ⊢ exp ↾ ran ⁡ log -1 ↾ ℝ + : ℝ + ⟶ 1-1 onto ℝ
14 dflog2 ⊢ log = exp ↾ ran ⁡ log -1
15 reseq1 ⊢ log = exp ↾ ran ⁡ log -1 → log ↾ ℝ + = exp ↾ ran ⁡ log -1 ↾ ℝ +
16 f1oeq1 ⊢ log ↾ ℝ + = exp ↾ ran ⁡ log -1 ↾ ℝ + → log ↾ ℝ + : ℝ + ⟶ 1-1 onto ℝ ↔ exp ↾ ran ⁡ log -1 ↾ ℝ + : ℝ + ⟶ 1-1 onto ℝ
17 14 15 16 mp2b ⊢ log ↾ ℝ + : ℝ + ⟶ 1-1 onto ℝ ↔ exp ↾ ran ⁡ log -1 ↾ ℝ + : ℝ + ⟶ 1-1 onto ℝ
18 13 17 mpbir ⊢ log ↾ ℝ + : ℝ + ⟶ 1-1 onto ℝ