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	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A^{B C} = {(A^{B})}^{C}$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to C \in ℂ$
2		simp2	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to B \in ℝ$
3	2	recnd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to B \in ℂ$
4		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
5	4	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to \log A \in ℝ$
6	5	recnd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to \log A \in ℂ$
7	1 3 6	mulassd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to C B \log A = C B \log A$
8	3 1	mulcomd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to B C = C B$
9	8	oveq1d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to B C \log A = C B \log A$
10		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
11	10	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A \in ℂ$
12		rpne0	$⊢ A \in ℝ^{+} \to A \neq 0$
13	12	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A \neq 0$
14		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} = e^{B \log A}$
15	11 13 3 14	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A^{B} = e^{B \log A}$
16	15	fveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to \log A^{B} = \log e^{B \log A}$
17	2 5	remulcld	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to B \log A \in ℝ$
18	17	relogefd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to \log e^{B \log A} = B \log A$
19	16 18	eqtrd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to \log A^{B} = B \log A$
20	19	oveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to C \log A^{B} = C B \log A$
21	7 9 20	3eqtr4d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to B C \log A = C \log A^{B}$
22	21	fveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to e^{B C \log A} = e^{C \log A^{B}}$
23	3 1	mulcld	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to B C \in ℂ$
24		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land B C \in ℂ) \to A^{B C} = e^{B C \log A}$
25	11 13 23 24	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A^{B C} = e^{B C \log A}$
26		cxpcl	$⊢ (A \in ℂ \land B \in ℂ) \to A^{B} \in ℂ$
27	11 3 26	syl2anc	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A^{B} \in ℂ$
28		cxpne0	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} \neq 0$
29	11 13 3 28	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A^{B} \neq 0$
30		cxpef	$⊢ (A^{B} \in ℂ \land A^{B} \neq 0 \land C \in ℂ) \to {(A^{B})}^{C} = e^{C \log A^{B}}$
31	27 29 1 30	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to {(A^{B})}^{C} = e^{C \log A^{B}}$
32	22 25 31	3eqtr4d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A^{B C} = {(A^{B})}^{C}$

Metamath Proof Explorer

Theorem cxpmul

Proof