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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑𝑐 𝐶 ) )