Metamath Proof Explorer

Theorem logcxp0

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

Ref Expression
Assertion logcxp0 ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → 𝐴 ∈ ℂ )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log ) → 𝐴 ∈ ℂ )
3 eldifsni ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → 𝐴 ≠ 0 )
4 3 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log ) → 𝐴 ≠ 0 )
5 simp2 ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log ) → 𝐵 ∈ ℂ )
6 2 4 5 cxpefd ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
7 6 fveq2d ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
8 logef ⊢ ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log → ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )
9 8 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log ) → ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )
10 7 9 eqtrd ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ran log ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )