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

Metamath Proof Explorer

Theorem cxpmul

Description: Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpmul ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑𝑐 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
2 simp2 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℝ )
3 2 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
4 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
5 4 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( log ‘ 𝐴 ) ∈ ℝ )
6 5 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( log ‘ 𝐴 ) ∈ ℂ )
7 1 3 6 mulassd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 · 𝐵 ) · ( log ‘ 𝐴 ) ) = ( 𝐶 · ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
8 3 1 mulcomd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
9 8 oveq1d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 · 𝐶 ) · ( log ‘ 𝐴 ) ) = ( ( 𝐶 · 𝐵 ) · ( log ‘ 𝐴 ) ) )
10 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
11 10 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
12 rpne0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
13 12 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → 𝐴 ≠ 0 )
14 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
15 11 13 3 14 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
16 15 fveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
17 2 5 remulcld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
18 17 relogefd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )
19 16 18 eqtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )
20 19 oveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 · ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ) = ( 𝐶 · ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
21 7 9 20 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 · 𝐶 ) · ( log ‘ 𝐴 ) ) = ( 𝐶 · ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ) )
22 21 fveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( exp ‘ ( ( 𝐵 · 𝐶 ) · ( log ‘ 𝐴 ) ) ) = ( exp ‘ ( 𝐶 · ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ) ) )
23 3 1 mulcld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
24 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( exp ‘ ( ( 𝐵 · 𝐶 ) · ( log ‘ 𝐴 ) ) ) )
25 11 13 23 24 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( exp ‘ ( ( 𝐵 · 𝐶 ) · ( log ‘ 𝐴 ) ) ) )
26 cxpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )
27 11 3 26 syl2anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )
28 cxpne0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ≠ 0 )
29 11 13 3 28 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ≠ 0 )
30 cxpef ⊢ ( ( ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ ∧ ( 𝐴 ↑𝑐 𝐵 ) ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐵 ) ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ) ) )
31 27 29 1 30 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐵 ) ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) ) ) )
32 22 25 31 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑𝑐 𝐶 ) )