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	$$⊢\phi \to A\in ℂ$$
	expcld.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	expaddd.2	$$⊢\phi \to M\in {\mathbb{N}}_0$$
Assertion	expmuld	$$⊢\phi \to A^{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={\left(A^M\right)}^N$$

Proof

Step	Hyp	Ref	Expression
1		expcld.1	$$⊢\phi \to A\in ℂ$$
2		expcld.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		expaddd.2	$$⊢\phi \to M\in {\mathbb{N}}_0$$
4		expmul	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to A^{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={\left(A^M\right)}^N$$
5	1 3 2 4	syl3anc	$$⊢\phi \to A^{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={\left(A^M\right)}^N$$