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