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)
per cases ( ( k >= 0 & l >= 0 ) or ( k >= 0 & l < 0 ) or ( k < 0 & l >= 0 ) or ( k < 0 & l < 0 ) ) ;
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
.= a |^ () by
.= (a |^ |.k.|) * (a |^ |.l.|) by NEWTON:8
.= (a #Z k) * (a |^ |.l.|) by
.= (a #Z k) * (a #Z l) by ; :: thesis: verum
end;
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 ;
k + l = m - n ;
hence a #Z (k + l) = (a |^ m) / (a |^ n) by
.= (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
.= (a #Z k) * (a #Z l) by ;
:: thesis: verum
end;
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 ;
k + l = m - n ;
hence a #Z (k + l) = (a |^ m) / (a |^ n) by
.= (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
.= (a #Z k) * (a #Z l) by ;
:: thesis: verum
end;
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
.= (a |^ ()) " by
.= ((a |^ |.k.|) * (a |^ |.l.|)) " by NEWTON:8
.= ((a |^ |.k.|) ") * ((a |^ |.l.|) ") by XCMPLX_1:204
.= (a #Z k) * ((a |^ |.l.|) ") by
.= (a #Z k) * (a #Z l) by ; :: thesis: verum
end;
end;