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 fvres ⊢ B ∈ ran ⁡ log → exp ↾ ran ⁡ log ⁡ B = e B
3 2 eqeq1d ⊢ B ∈ ran ⁡ log → exp ↾ ran ⁡ log ⁡ B = A ↔ e B = A
4 3 adantr ⊢ B ∈ ran ⁡ log ∧ A ∈ ℂ ∖ 0 → exp ↾ ran ⁡ log ⁡ B = A ↔ e B = A
5 eff1o2 ⊢ exp ↾ ran ⁡ log : ran ⁡ log ⟶ 1-1 onto ℂ ∖ 0
6 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
7 5 6 mp3an1 ⊢ B ∈ ran ⁡ log ∧ A ∈ ℂ ∖ 0 → exp ↾ ran ⁡ log ⁡ B = A ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
8 4 7 bitr3d ⊢ B ∈ ran ⁡ log ∧ A ∈ ℂ ∖ 0 → e B = A ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
9 8 ancoms ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ran ⁡ log → e B = A ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
10 dflog2 ⊢ log = exp ↾ ran ⁡ log -1
11 10 fveq1i ⊢ log ⁡ A = exp ↾ ran ⁡ log -1 ⁡ A
12 11 eqeq1i ⊢ log ⁡ A = B ↔ exp ↾ ran ⁡ log -1 ⁡ A = B
13 9 12 syl6rbbr ⊢ 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