Metamath Proof Explorer

Theorem logeftb

Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion logeftb ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ran ⁡ log → log ⁡ A = B ↔ e B = A

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ A ∈ ℂ ∖ 0 ↔ A ∈ ℂ ∧ A ≠ 0
2 dflog2 ⊢ log = exp ↾ ran ⁡ log -1
3 2 fveq1i ⊢ log ⁡ A = exp ↾ ran ⁡ log -1 ⁡ A
4 3 eqeq1i ⊢ log ⁡ A = B ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
5 fvres ⊢ B ∈ ran ⁡ log → exp ↾ ran ⁡ log ⁡ B = e B
6 5 eqeq1d ⊢ B ∈ ran ⁡ log → exp ↾ ran ⁡ log ⁡ B = A ↔ e B = A
7 6 adantr ⊢ B ∈ ran ⁡ log ∧ A ∈ ℂ ∖ 0 → exp ↾ ran ⁡ log ⁡ B = A ↔ e B = A
8 eff1o2 ⊢ exp ↾ ran ⁡ log : ran ⁡ log ⟶ 1-1 onto ℂ ∖ 0
9 f1ocnvfvb ⊢ exp ↾ ran ⁡ log : ran ⁡ log ⟶ 1-1 onto ℂ ∖ 0 ∧ B ∈ ran ⁡ log ∧ A ∈ ℂ ∖ 0 → exp ↾ ran ⁡ log ⁡ B = A ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
10 8 9 mp3an1 ⊢ B ∈ ran ⁡ log ∧ A ∈ ℂ ∖ 0 → exp ↾ ran ⁡ log ⁡ B = A ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
11 7 10 bitr3d ⊢ B ∈ ran ⁡ log ∧ A ∈ ℂ ∖ 0 → e B = A ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
12 11 ancoms ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ran ⁡ log → e B = A ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
13 4 12 bitr4id ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ran ⁡ log → log ⁡ A = B ↔ e B = A
14 1 13 sylanbr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ran ⁡ log → log ⁡ A = B ↔ e B = A
15 14 3impa ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ran ⁡ log → log ⁡ A = B ↔ e B = A