let a be Real; :: thesis: for m, n being Nat st a <> 0 holds

a #Z (m - n) = (a |^ m) / (a |^ n)

let m, n be Nat; :: thesis: ( a <> 0 implies a #Z (m - n) = (a |^ m) / (a |^ n) )

assume A1: a <> 0 ; :: thesis: a #Z (m - n) = (a |^ m) / (a |^ n)

a #Z (m - n) = (a |^ m) / (a |^ n)

let m, n be Nat; :: thesis: ( a <> 0 implies a #Z (m - n) = (a |^ m) / (a |^ n) )

assume A1: a <> 0 ; :: thesis: a #Z (m - n) = (a |^ m) / (a |^ n)

per cases
( m - n >= 0 or m - n < 0 )
;

end;

suppose
m - n >= 0
; :: thesis: a #Z (m - n) = (a |^ m) / (a |^ n)

then reconsider m1 = m - n as Element of NAT by INT_1:3;

A2: (a #Z (m - n)) * (a |^ n) = (a |^ m1) * (a |^ n) by Th36

.= a |^ (m1 + n) by NEWTON:8

.= a |^ m ;

a |^ n <> 0 by A1, Th5;

hence a #Z (m - n) = (a |^ m) / (a |^ n) by A2, XCMPLX_1:89; :: thesis: verum

end;A2: (a #Z (m - n)) * (a |^ n) = (a |^ m1) * (a |^ n) by Th36

.= a |^ (m1 + n) by NEWTON:8

.= a |^ m ;

a |^ n <> 0 by A1, Th5;

hence a #Z (m - n) = (a |^ m) / (a |^ n) by A2, XCMPLX_1:89; :: thesis: verum

suppose
m - n < 0
; :: thesis: a #Z (m - n) = (a |^ m) / (a |^ n)

then
- (m - n) > 0
;

then reconsider m1 = n - m as Element of NAT by INT_1:3;

A3: a #Z (n - m) = a #Z (- (m - n))

.= 1 / (a #Z (m - n)) by Th41 ;

(a #Z (n - m)) * (a |^ m) = (a |^ m1) * (a |^ m) by Th36

.= a |^ (m1 + m) by NEWTON:8

.= a |^ n ;

then A4: (a |^ m) / (a #Z (m - n)) = a |^ n by A3;

a |^ n <> 0 by A1, Th5;

hence a #Z (m - n) = (a |^ m) / (a |^ n) by A4, XCMPLX_1:54; :: thesis: verum

end;then reconsider m1 = n - m as Element of NAT by INT_1:3;

A3: a #Z (n - m) = a #Z (- (m - n))

.= 1 / (a #Z (m - n)) by Th41 ;

(a #Z (n - m)) * (a |^ m) = (a |^ m1) * (a |^ m) by Th36

.= a |^ (m1 + m) by NEWTON:8

.= a |^ n ;

then A4: (a |^ m) / (a #Z (m - n)) = a |^ n by A3;

a |^ n <> 0 by A1, Th5;

hence a #Z (m - n) = (a |^ m) / (a |^ n) by A4, XCMPLX_1:54; :: thesis: verum