Theorem cxpneg

Description: Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Assertion	cxpneg	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^{-B}=\frac{1}{A^B}$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A\in ℂ$$
2		simp3	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to B\in ℂ$$
3		cxpcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^B\in ℂ$$
4	1 2 3	syl2anc	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B\in ℂ$$
5	2	negcld	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to -B\in ℂ$$
6		cxpcl	$$⊢\left(A\in ℂ\wedge -B\in ℂ\right)\to A^{-B}\in ℂ$$
7	1 5 6	syl2anc	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^{-B}\in ℂ$$
8		cxpne0	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B\ne 0$$
9	2	negidd	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to B+\left(-B\right)=0$$
10	9	oveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^{B+\left(-B\right)}=A^0$$
11		simp2	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A\ne 0$$
12		cxpadd	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge B\in ℂ\wedge -B\in ℂ\right)\to A^{B+\left(-B\right)}=A^B{A}^{-B}$$
13	1 11 2 5 12	syl211anc	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^{B+\left(-B\right)}=A^B{A}^{-B}$$
14		cxp0	$$⊢A\in ℂ\to A^0=1$$
15	1 14	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^0=1$$
16	10 13 15	3eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B{A}^{-B}=1$$
17	4 7 8 16	mvllmuld	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^{-B}=\frac{1}{A^B}$$