Theorem cxpmul2z

Description: Generalize cxpmul2 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Assertion	cxpmul2z	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elznn0	⊢ ( 𝐶 ∈ ℤ ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐶 ∈ ℕ0 ∨ - 𝐶 ∈ ℕ0 ) ) )
2		cxpmul2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )
3	2	3expia	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 ∈ ℕ0 → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
4	3	ad4ant13	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ℕ0 → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
5		simplll	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐴 ∈ ℂ )
6		simplr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐵 ∈ ℂ )
7		simprr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - 𝐶 ∈ ℕ0 )
8		cxpmul2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ - 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) )
9	5 6 7 8	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) )
10	9	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 1 / ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) ) = ( 1 / ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) ) )
11		simprl	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐶 ∈ ℝ )
12	11	recnd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐶 ∈ ℂ )
13	6 12	mulneg2d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐵 · - 𝐶 ) = - ( 𝐵 · 𝐶 ) )
14	13	negeqd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - ( 𝐵 · - 𝐶 ) = - - ( 𝐵 · 𝐶 ) )
15	6 12	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
16	15	negnegd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - - ( 𝐵 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
17	14 16	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - ( 𝐵 · - 𝐶 ) = ( 𝐵 · 𝐶 ) )
18	17	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 - ( 𝐵 · - 𝐶 ) ) = ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) )
19		simpllr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐴 ≠ 0 )
20	12	negcld	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - 𝐶 ∈ ℂ )
21	6 20	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐵 · - 𝐶 ) ∈ ℂ )
22		cxpneg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( 𝐵 · - 𝐶 ) ∈ ℂ ) → ( 𝐴 ↑𝑐 - ( 𝐵 · - 𝐶 ) ) = ( 1 / ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) ) )
23	5 19 21 22	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 - ( 𝐵 · - 𝐶 ) ) = ( 1 / ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) ) )
24	18 23	eqtr3d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( 1 / ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) ) )
25		cxpcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )
26	25	ad4ant13	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )
27		expneg2	⊢ ( ( ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ - 𝐶 ∈ ℕ0 ) → ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) = ( 1 / ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) ) )
28	26 12 7 27	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) = ( 1 / ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) ) )
29	10 24 28	3eqtr4d	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )
30	29	expr	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℝ ) → ( - 𝐶 ∈ ℕ0 → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
31	4 30	jaod	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 ∈ ℕ0 ∨ - 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
32	31	expimpd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 ∈ ℝ ∧ ( 𝐶 ∈ ℕ0 ∨ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
33	1 32	biimtrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( 𝐶 ∈ ℤ → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
34	33	impr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )