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

Metamath Proof Explorer

Theorem logcxp

Description: Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion logcxp ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
3 rpne0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐴 ≠ 0 )
5 simpr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
6 5 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℂ )
7 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
8 2 4 6 7 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
9 8 fveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
10 id ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ )
11 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
12 remulcl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
13 10 11 12 syl2anr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
14 13 relogefd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )
15 9 14 eqtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )