This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )