mulexpz

Description: Integer exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135. (Contributed by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	mulexpz	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land N \in ℤ) \to {A B}^{N} = A^{N} B^{N}$

Proof

Step	Hyp	Ref	Expression
1		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
2		simpl	$⊢ (A \in ℂ \land A \neq 0) \to A \in ℂ$
3		simpl	$⊢ (B \in ℂ \land B \neq 0) \to B \in ℂ$
4	2 3	anim12i	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (A \in ℂ \land B \in ℂ)$
5		mulexp	$⊢ (A \in ℂ \land B \in ℂ \land N \in ℕ_{0}) \to {A B}^{N} = A^{N} B^{N}$
6	5	3expa	$⊢ ((A \in ℂ \land B \in ℂ) \land N \in ℕ_{0}) \to {A B}^{N} = A^{N} B^{N}$
7	4 6	sylan	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land N \in ℕ_{0}) \to {A B}^{N} = A^{N} B^{N}$
8		simplll	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to A \in ℂ$
9		simplrl	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to B \in ℂ$
10	8 9	mulcld	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to A B \in ℂ$
11		recn	$⊢ N \in ℝ \to N \in ℂ$
12	11	ad2antrl	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℂ$
13		nnnn0	$⊢ - N \in ℕ \to - N \in ℕ_{0}$
14	13	ad2antll	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ_{0}$
15		expneg2	$⊢ (A B \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to {A B}^{N} = \frac{1}{{A B}^{- N}}$
16	10 12 14 15	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to {A B}^{N} = \frac{1}{{A B}^{- N}}$
17		expneg2	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to A^{N} = \frac{1}{A^{- N}}$
18	8 12 14 17	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to A^{N} = \frac{1}{A^{- N}}$
19		expneg2	$⊢ (B \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to B^{N} = \frac{1}{B^{- N}}$
20	9 12 14 19	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to B^{N} = \frac{1}{B^{- N}}$
21	18 20	oveq12d	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to A^{N} B^{N} = (\frac{1}{A^{- N}}) (\frac{1}{B^{- N}})$
22		mulexp	$⊢ (A \in ℂ \land B \in ℂ \land - N \in ℕ_{0}) \to {A B}^{- N} = A^{- N} B^{- N}$
23	8 9 14 22	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to {A B}^{- N} = A^{- N} B^{- N}$
24	23	oveq2d	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{{A B}^{- N}} = \frac{1}{A^{- N} B^{- N}}$
25		1t1e1	$⊢ 1 \cdot 1 = 1$
26	25	oveq1i	$⊢ \frac{1 \cdot 1}{A^{- N} B^{- N}} = \frac{1}{A^{- N} B^{- N}}$
27	24 26	eqtr4di	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{{A B}^{- N}} = \frac{1 \cdot 1}{A^{- N} B^{- N}}$
28		expcl	$⊢ (A \in ℂ \land - N \in ℕ_{0}) \to A^{- N} \in ℂ$
29	8 14 28	syl2anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to A^{- N} \in ℂ$
30		simpllr	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to A \neq 0$
31		nnz	$⊢ - N \in ℕ \to - N \in ℤ$
32	31	ad2antll	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℤ$
33		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land - N \in ℤ) \to A^{- N} \neq 0$
34	8 30 32 33	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to A^{- N} \neq 0$
35		expcl	$⊢ (B \in ℂ \land - N \in ℕ_{0}) \to B^{- N} \in ℂ$
36	9 14 35	syl2anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to B^{- N} \in ℂ$
37		simplrr	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to B \neq 0$
38		expne0i	$⊢ (B \in ℂ \land B \neq 0 \land - N \in ℤ) \to B^{- N} \neq 0$
39	9 37 32 38	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to B^{- N} \neq 0$
40		ax-1cn	$⊢ 1 \in ℂ$
41		divmuldiv	$⊢ ((1 \in ℂ \land 1 \in ℂ) \land ((A^{- N} \in ℂ \land A^{- N} \neq 0) \land (B^{- N} \in ℂ \land B^{- N} \neq 0))) \to (\frac{1}{A^{- N}}) (\frac{1}{B^{- N}}) = \frac{1 \cdot 1}{A^{- N} B^{- N}}$
42	40 40 41	mpanl12	$⊢ ((A^{- N} \in ℂ \land A^{- N} \neq 0) \land (B^{- N} \in ℂ \land B^{- N} \neq 0)) \to (\frac{1}{A^{- N}}) (\frac{1}{B^{- N}}) = \frac{1 \cdot 1}{A^{- N} B^{- N}}$
43	29 34 36 39 42	syl22anc	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to (\frac{1}{A^{- N}}) (\frac{1}{B^{- N}}) = \frac{1 \cdot 1}{A^{- N} B^{- N}}$
44	27 43	eqtr4d	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{{A B}^{- N}} = (\frac{1}{A^{- N}}) (\frac{1}{B^{- N}})$
45	21 44	eqtr4d	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to A^{N} B^{N} = \frac{1}{{A B}^{- N}}$
46	16 45	eqtr4d	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℝ \land - N \in ℕ)) \to {A B}^{N} = A^{N} B^{N}$
47	7 46	jaodan	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))) \to {A B}^{N} = A^{N} B^{N}$
48	1 47	sylan2b	$⊢ (((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \land N \in ℤ) \to {A B}^{N} = A^{N} B^{N}$
49	48	3impa	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land N \in ℤ) \to {A B}^{N} = A^{N} B^{N}$

Metamath Proof Explorer

Theorem mulexpz

Proof