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

Metamath Proof Explorer

Theorem cxpmul2d

Description: Product of exponents law for complex exponentiation. Variation on cxpmul with more general conditions on A and B when C is a nonnegative integer. (Contributed by Mario Carneiro, 30-May-2016)

	Ref	Expression
Hypotheses	cxp0d.1	$⊢ φ \to A \in ℂ$
	cxpcld.2	$⊢ φ \to B \in ℂ$
	cxpmul2d.4	$⊢ φ \to C \in ℕ_{0}$
Assertion	cxpmul2d	$⊢ φ \to A^{B C} = {(A^{B})}^{C}$

Proof

Step	Hyp	Ref	Expression
1		cxp0d.1	$⊢ φ \to A \in ℂ$
2		cxpcld.2	$⊢ φ \to B \in ℂ$
3		cxpmul2d.4	$⊢ φ \to C \in ℕ_{0}$
4		cxpmul2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℕ_{0}) \to A^{B C} = {(A^{B})}^{C}$
5	1 2 3 4	syl3anc	$⊢ φ \to A^{B C} = {(A^{B})}^{C}$