Theorem expm1

Description: Value of a complex number raised to an integer power minus one. (Contributed by NM, 25-Dec-2008) (Revised by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expm1	|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / A ) )

Proof

Step	Hyp	Ref	Expression
1		1z	|- 1 e. ZZ
2		expsub	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. ZZ /\ 1 e. ZZ ) ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / ( A ^ 1 ) ) )
3	1 2	mpanr2	|- ( ( ( A e. CC /\ A =/= 0 ) /\ N e. ZZ ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / ( A ^ 1 ) ) )
4	3	3impa	|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / ( A ^ 1 ) ) )
5		exp1	|- ( A e. CC -> ( A ^ 1 ) = A )
6	5	3ad2ant1	|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ 1 ) = A )
7	6	oveq2d	|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( A ^ N ) / ( A ^ 1 ) ) = ( ( A ^ N ) / A ) )
8	4 7	eqtrd	|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / A ) )