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

Metamath Proof Explorer

Theorem expmuld

Description: Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of Gleason p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	expcld.1	$⊢ φ \to A \in ℂ$
	expcld.2	$⊢ φ \to N \in ℕ_{0}$
	expaddd.2	$⊢ φ \to M \in ℕ_{0}$
Assertion	expmuld	$⊢ φ \to A^{M \cdot N} = {(A^{M})}^{N}$

Proof

Step	Hyp	Ref	Expression
1		expcld.1	$⊢ φ \to A \in ℂ$
2		expcld.2	$⊢ φ \to N \in ℕ_{0}$
3		expaddd.2	$⊢ φ \to M \in ℕ_{0}$
4		expmul	$⊢ (A \in ℂ \land M \in ℕ_{0} \land N \in ℕ_{0}) \to A^{M \cdot N} = {(A^{M})}^{N}$
5	1 3 2 4	syl3anc	$⊢ φ \to A^{M \cdot N} = {(A^{M})}^{N}$