Metamath Proof Explorer


Theorem expsub

Description: Exponent subtraction law for integer exponentiation. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 znegcl
 |-  ( N e. ZZ -> -u N e. ZZ )
2 expaddz
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ -u N e. ZZ ) ) -> ( A ^ ( M + -u N ) ) = ( ( A ^ M ) x. ( A ^ -u N ) ) )
3 1 2 sylanr2
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M + -u N ) ) = ( ( A ^ M ) x. ( A ^ -u N ) ) )
4 zcn
 |-  ( M e. ZZ -> M e. CC )
5 zcn
 |-  ( N e. ZZ -> N e. CC )
6 negsub
 |-  ( ( M e. CC /\ N e. CC ) -> ( M + -u N ) = ( M - N ) )
7 4 5 6 syl2an
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + -u N ) = ( M - N ) )
8 7 adantl
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M + -u N ) = ( M - N ) )
9 8 oveq2d
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M + -u N ) ) = ( A ^ ( M - N ) ) )
10 expnegz
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
11 10 3expa
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ N e. ZZ ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
12 11 adantrl
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
13 12 oveq2d
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A ^ M ) x. ( A ^ -u N ) ) = ( ( A ^ M ) x. ( 1 / ( A ^ N ) ) ) )
14 expclz
 |-  ( ( A e. CC /\ A =/= 0 /\ M e. ZZ ) -> ( A ^ M ) e. CC )
15 14 3expa
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. ZZ ) -> ( A ^ M ) e. CC )
16 15 adantrr
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ M ) e. CC )
17 expclz
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. CC )
18 17 3expa
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ N e. ZZ ) -> ( A ^ N ) e. CC )
19 18 adantrl
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ N ) e. CC )
20 expne0i
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) =/= 0 )
21 20 3expa
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ N e. ZZ ) -> ( A ^ N ) =/= 0 )
22 21 adantrl
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ N ) =/= 0 )
23 16 19 22 divrecd
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A ^ M ) / ( A ^ N ) ) = ( ( A ^ M ) x. ( 1 / ( A ^ N ) ) ) )
24 13 23 eqtr4d
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A ^ M ) x. ( A ^ -u N ) ) = ( ( A ^ M ) / ( A ^ N ) ) )
25 3 9 24 3eqtr3d
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M - N ) ) = ( ( A ^ M ) / ( A ^ N ) ) )