Metamath Proof Explorer

Theorem logcxp0

Description: Logarithm of a complex power. Generalization of logcxp . (Contributed by AV, 22-May-2020)

Ref Expression
Assertion logcxp0 ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ℂ ∧ B ⁢ log ⁡ A ∈ ran ⁡ log → log ⁡ A B = B ⁢ log ⁡ A

Proof

Step Hyp Ref Expression
1 eldifi ⊢ A ∈ ℂ ∖ 0 → A ∈ ℂ
2 1 3ad2ant1 ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ℂ ∧ B ⁢ log ⁡ A ∈ ran ⁡ log → A ∈ ℂ
3 eldifsni ⊢ A ∈ ℂ ∖ 0 → A ≠ 0
4 3 3ad2ant1 ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ℂ ∧ B ⁢ log ⁡ A ∈ ran ⁡ log → A ≠ 0
5 simp2 ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ℂ ∧ B ⁢ log ⁡ A ∈ ran ⁡ log → B ∈ ℂ
6 2 4 5 cxpefd ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ℂ ∧ B ⁢ log ⁡ A ∈ ran ⁡ log → A B = e B ⁢ log ⁡ A
7 6 fveq2d ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ℂ ∧ B ⁢ log ⁡ A ∈ ran ⁡ log → log ⁡ A B = log ⁡ e B ⁢ log ⁡ A
8 logef ⊢ B ⁢ log ⁡ A ∈ ran ⁡ log → log ⁡ e B ⁢ log ⁡ A = B ⁢ log ⁡ A
9 8 3ad2ant3 ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ℂ ∧ B ⁢ log ⁡ A ∈ ran ⁡ log → log ⁡ e B ⁢ log ⁡ A = B ⁢ log ⁡ A
10 7 9 eqtrd ⊢ A ∈ ℂ ∖ 0 ∧ B ∈ ℂ ∧ B ⁢ log ⁡ A ∈ ran ⁡ log → log ⁡ A B = B ⁢ log ⁡ A