let a be Real; :: thesis: for k, l being Integer holds (a #Z k) #Z l = a #Z (k * l)
let k, l be Integer; :: thesis: (a #Z k) #Z l = a #Z (k * l)
per cases ( k * l > 0 or k * l < 0 or k * l = 0 ) ;
suppose A1: k * l > 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
per cases ( ( k > 0 & l > 0 ) or ( k < 0 & l < 0 ) ) by ;
suppose A2: ( k > 0 & l > 0 ) ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = (a #Z k) |^ |.l.| by Def3
.= (a |^ |.k.|) |^ |.l.| by
.= a |^ () by NEWTON:9
.= a |^ |.(k * l).| by COMPLEX1:65
.= a #Z (k * l) by ;
:: thesis: verum
end;
suppose A3: ( k < 0 & l < 0 ) ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = ((a #Z k) |^ |.l.|) " by Def3
.= (((a |^ |.k.|) ") |^ |.l.|) " by
.= ((1 / (a |^ |.k.|)) |^ |.l.|) "
.= (1 / ((a |^ |.k.|) |^ |.l.|)) " by Th7
.= (((a |^ |.k.|) |^ |.l.|) ") "
.= a |^ () by NEWTON:9
.= a |^ |.(k * l).| by COMPLEX1:65
.= a #Z (k * l) by ;
:: thesis: verum
end;
end;
end;
suppose A4: k * l < 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
per cases ( ( k < 0 & l > 0 ) or ( k > 0 & l < 0 ) ) by ;
suppose A5: ( k < 0 & l > 0 ) ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = (a #Z k) |^ |.l.| by Def3
.= ((a |^ |.k.|) ") |^ |.l.| by
.= (1 / (a |^ |.k.|)) |^ |.l.|
.= 1 / ((a |^ |.k.|) |^ |.l.|) by Th7
.= 1 / (a |^ ()) by NEWTON:9
.= 1 / (a |^ |.(k * l).|) by COMPLEX1:65
.= (a |^ |.(k * l).|) "
.= a #Z (k * l) by ;
:: thesis: verum
end;
suppose A6: ( k > 0 & l < 0 ) ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = ((a #Z k) |^ |.l.|) " by Def3
.= ((a |^ |.k.|) |^ |.l.|) " by
.= (a |^ ()) " by NEWTON:9
.= (a |^ |.(k * l).|) " by COMPLEX1:65
.= a #Z (k * l) by ;
:: thesis: verum
end;
end;
end;
suppose A7: k * l = 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
per cases ( k = 0 or l = 0 ) by A7;
suppose k = 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = 1 #Z l by Th34
.= 1 by Th37
.= a #Z (k * l) by ;
:: thesis: verum
end;
suppose l = 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)
hence (a #Z k) #Z l = 1 by Th34
.= a #Z (k * l) by ;
:: thesis: verum
end;
end;
end;
end;