expdiv

Description: Nonnegative integer exponentiation of a quotient. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	expdiv	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to {(\frac{A}{B})}^{N} = \frac{A^{N}}{B^{N}}$

Proof

Step	Hyp	Ref	Expression
1		divrec	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} = A (\frac{1}{B})$
2	1	3expb	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{A}{B} = A (\frac{1}{B})$
3	2	3adant3	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to \frac{A}{B} = A (\frac{1}{B})$
4	3	oveq1d	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to {(\frac{A}{B})}^{N} = {A (\frac{1}{B})}^{N}$
5		reccl	$⊢ (B \in ℂ \land B \neq 0) \to \frac{1}{B} \in ℂ$
6		mulexp	$⊢ (A \in ℂ \land \frac{1}{B} \in ℂ \land N \in ℕ_{0}) \to {A (\frac{1}{B})}^{N} = A^{N} {(\frac{1}{B})}^{N}$
7	5 6	syl3an2	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to {A (\frac{1}{B})}^{N} = A^{N} {(\frac{1}{B})}^{N}$
8		simp2l	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to B \in ℂ$
9		simp2r	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to B \neq 0$
10		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
11	10	3ad2ant3	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to N \in ℤ$
12		exprec	$⊢ (B \in ℂ \land B \neq 0 \land N \in ℤ) \to {(\frac{1}{B})}^{N} = \frac{1}{B^{N}}$
13	8 9 11 12	syl3anc	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to {(\frac{1}{B})}^{N} = \frac{1}{B^{N}}$
14	13	oveq2d	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to A^{N} {(\frac{1}{B})}^{N} = A^{N} (\frac{1}{B^{N}})$
15		expcl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{N} \in ℂ$
16	15	3adant2	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to A^{N} \in ℂ$
17		expcl	$⊢ (B \in ℂ \land N \in ℕ_{0}) \to B^{N} \in ℂ$
18	17	adantlr	$⊢ ((B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to B^{N} \in ℂ$
19	18	3adant1	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to B^{N} \in ℂ$
20		expne0i	$⊢ (B \in ℂ \land B \neq 0 \land N \in ℤ) \to B^{N} \neq 0$
21	8 9 11 20	syl3anc	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to B^{N} \neq 0$
22	16 19 21	divrecd	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to \frac{A^{N}}{B^{N}} = A^{N} (\frac{1}{B^{N}})$
23	14 22	eqtr4d	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to A^{N} {(\frac{1}{B})}^{N} = \frac{A^{N}}{B^{N}}$
24	4 7 23	3eqtrd	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land N \in ℕ_{0}) \to {(\frac{A}{B})}^{N} = \frac{A^{N}}{B^{N}}$

Metamath Proof Explorer

Theorem expdiv

Proof