Theorem 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	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elznn0nn	⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
2		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
3		simpl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
4	2 3	anim12i	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
5		mulexp	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )
6	5	3expa	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )
7	4 6	sylan	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )
8		simplll	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ∈ ℂ )
9		simplrl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐵 ∈ ℂ )
10	8 9	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
11		recn	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
12	11	ad2antrl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
13		nnnn0	⊢ ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℕ0 )
14	13	ad2antll	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ0 )
15		expneg2	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) )
16	10 12 14 15	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) )
17		expneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
18	8 12 14 17	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
19		expneg2	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) = ( 1 / ( 𝐵 ↑ - 𝑁 ) ) )
20	9 12 14 19	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐵 ↑ 𝑁 ) = ( 1 / ( 𝐵 ↑ - 𝑁 ) ) )
21	18 20	oveq12d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) = ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) )
22		mulexp	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) = ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) )
23	8 9 14 22	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) = ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) )
24	23	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) = ( 1 / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
25		1t1e1	⊢ ( 1 · 1 ) = 1
26	25	oveq1i	⊢ ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) = ( 1 / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) )
27	24 26	eqtr4di	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) = ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
28		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) ∈ ℂ )
29	8 14 28	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝑁 ) ∈ ℂ )
30		simpllr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ≠ 0 )
31		nnz	⊢ ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℤ )
32	31	ad2antll	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℤ )
33		expne0i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) ≠ 0 )
34	8 30 32 33	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝑁 ) ≠ 0 )
35		expcl	⊢ ( ( 𝐵 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝑁 ) ∈ ℂ )
36	9 14 35	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐵 ↑ - 𝑁 ) ∈ ℂ )
37		simplrr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐵 ≠ 0 )
38		expne0i	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( 𝐵 ↑ - 𝑁 ) ≠ 0 )
39	9 37 32 38	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐵 ↑ - 𝑁 ) ≠ 0 )
40		ax-1cn	⊢ 1 ∈ ℂ
41		divmuldiv	⊢ ( ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( ( ( 𝐴 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐴 ↑ - 𝑁 ) ≠ 0 ) ∧ ( ( 𝐵 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐵 ↑ - 𝑁 ) ≠ 0 ) ) ) → ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) = ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
42	40 40 41	mpanl12	⊢ ( ( ( ( 𝐴 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐴 ↑ - 𝑁 ) ≠ 0 ) ∧ ( ( 𝐵 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐵 ↑ - 𝑁 ) ≠ 0 ) ) → ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) = ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
43	29 34 36 39 42	syl22anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) = ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
44	27 43	eqtr4d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) = ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) )
45	21 44	eqtr4d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) = ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) )
46	16 45	eqtr4d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )
47	7 46	jaodan	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )
48	1 47	sylan2b	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )
49	48	3impa	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )