let a be Real; :: thesis: for k, l being Integer st a <> 0 holds

a #Z (k + l) = (a #Z k) * (a #Z l)

let k, l be Integer; :: thesis: ( a <> 0 implies a #Z (k + l) = (a #Z k) * (a #Z l) )

assume A1: a <> 0 ; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

a #Z (k + l) = (a #Z k) * (a #Z l)

let k, l be Integer; :: thesis: ( a <> 0 implies a #Z (k + l) = (a #Z k) * (a #Z l) )

assume A1: a <> 0 ; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

per cases
( ( k >= 0 & l >= 0 ) or ( k >= 0 & l < 0 ) or ( k < 0 & l >= 0 ) or ( k < 0 & l < 0 ) )
;

end;

suppose A2:
( k >= 0 & l >= 0 )
; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

then A3:
k * l >= 0
;

thus a #Z (k + l) = a |^ |.(k + l).| by A2, Def3

.= a |^ (|.k.| + |.l.|) by A3, ABSVALUE:11

.= (a |^ |.k.|) * (a |^ |.l.|) by NEWTON:8

.= (a #Z k) * (a |^ |.l.|) by A2, Def3

.= (a #Z k) * (a #Z l) by A2, Def3 ; :: thesis: verum

end;thus a #Z (k + l) = a |^ |.(k + l).| by A2, Def3

.= a |^ (|.k.| + |.l.|) by A3, ABSVALUE:11

.= (a |^ |.k.|) * (a |^ |.l.|) by NEWTON:8

.= (a #Z k) * (a |^ |.l.|) by A2, Def3

.= (a #Z k) * (a #Z l) by A2, Def3 ; :: thesis: verum

suppose A4:
( k >= 0 & l < 0 )
; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

then reconsider m = k as Element of NAT by INT_1:3;

reconsider n = - l as Element of NAT by A4, INT_1:3;

k + l = m - n ;

hence a #Z (k + l) = (a |^ m) / (a |^ n) by A1, Th43

.= (a |^ m) * ((a |^ n) ")

.= (a |^ |.k.|) * ((a |^ n) ") by ABSVALUE:def 1

.= (a |^ |.k.|) * ((a |^ |.(- l).|) ") by ABSVALUE:def 1

.= (a |^ |.k.|) * ((a |^ |.l.|) ") by COMPLEX1:52

.= (a #Z k) * ((a |^ |.l.|) ") by A4, Def3

.= (a #Z k) * (a #Z l) by A4, Def3 ;

:: thesis: verum

end;reconsider n = - l as Element of NAT by A4, INT_1:3;

k + l = m - n ;

hence a #Z (k + l) = (a |^ m) / (a |^ n) by A1, Th43

.= (a |^ m) * ((a |^ n) ")

.= (a |^ |.k.|) * ((a |^ n) ") by ABSVALUE:def 1

.= (a |^ |.k.|) * ((a |^ |.(- l).|) ") by ABSVALUE:def 1

.= (a |^ |.k.|) * ((a |^ |.l.|) ") by COMPLEX1:52

.= (a #Z k) * ((a |^ |.l.|) ") by A4, Def3

.= (a #Z k) * (a #Z l) by A4, Def3 ;

:: thesis: verum

suppose A5:
( k < 0 & l >= 0 )
; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

then reconsider m = l as Element of NAT by INT_1:3;

reconsider n = - k as Element of NAT by A5, INT_1:3;

k + l = m - n ;

hence a #Z (k + l) = (a |^ m) / (a |^ n) by A1, Th43

.= (a |^ m) * ((a |^ n) ")

.= (a |^ |.l.|) * ((a |^ n) ") by ABSVALUE:def 1

.= (a |^ |.l.|) * ((a |^ |.(- k).|) ") by ABSVALUE:def 1

.= (a |^ |.l.|) * ((a |^ |.k.|) ") by COMPLEX1:52

.= (a #Z l) * ((a |^ |.k.|) ") by A5, Def3

.= (a #Z k) * (a #Z l) by A5, Def3 ;

:: thesis: verum

end;reconsider n = - k as Element of NAT by A5, INT_1:3;

k + l = m - n ;

hence a #Z (k + l) = (a |^ m) / (a |^ n) by A1, Th43

.= (a |^ m) * ((a |^ n) ")

.= (a |^ |.l.|) * ((a |^ n) ") by ABSVALUE:def 1

.= (a |^ |.l.|) * ((a |^ |.(- k).|) ") by ABSVALUE:def 1

.= (a |^ |.l.|) * ((a |^ |.k.|) ") by COMPLEX1:52

.= (a #Z l) * ((a |^ |.k.|) ") by A5, Def3

.= (a #Z k) * (a #Z l) by A5, Def3 ;

:: thesis: verum

suppose A6:
( k < 0 & l < 0 )
; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

then A7:
k * l >= 0
;

thus a #Z (k + l) = (a |^ |.(k + l).|) " by A6, Def3

.= (a |^ (|.k.| + |.l.|)) " by A7, ABSVALUE:11

.= ((a |^ |.k.|) * (a |^ |.l.|)) " by NEWTON:8

.= ((a |^ |.k.|) ") * ((a |^ |.l.|) ") by XCMPLX_1:204

.= (a #Z k) * ((a |^ |.l.|) ") by A6, Def3

.= (a #Z k) * (a #Z l) by A6, Def3 ; :: thesis: verum

end;thus a #Z (k + l) = (a |^ |.(k + l).|) " by A6, Def3

.= (a |^ (|.k.| + |.l.|)) " by A7, ABSVALUE:11

.= ((a |^ |.k.|) * (a |^ |.l.|)) " by NEWTON:8

.= ((a |^ |.k.|) ") * ((a |^ |.l.|) ") by XCMPLX_1:204

.= (a #Z k) * ((a |^ |.l.|) ") by A6, Def3

.= (a #Z k) * (a #Z l) by A6, Def3 ; :: thesis: verum