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)

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

end;

suppose A1:
k * l > 0
; :: thesis: (a #Z k) #Z l = a #Z (k * l)

end;

per cases
( ( k > 0 & l > 0 ) or ( k < 0 & l < 0 ) )
by A1, XREAL_1:134;

end;

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 A2, Def3

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

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

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

:: thesis: verum

end;.= (a |^ |.k.|) |^ |.l.| by A2, Def3

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

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

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

:: thesis: verum

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 A3, Def3

.= ((1 / (a |^ |.k.|)) |^ |.l.|) "

.= (1 / ((a |^ |.k.|) |^ |.l.|)) " by Th7

.= (((a |^ |.k.|) |^ |.l.|) ") "

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

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

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

:: thesis: verum

end;.= (((a |^ |.k.|) ") |^ |.l.|) " by A3, Def3

.= ((1 / (a |^ |.k.|)) |^ |.l.|) "

.= (1 / ((a |^ |.k.|) |^ |.l.|)) " by Th7

.= (((a |^ |.k.|) |^ |.l.|) ") "

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

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

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

:: thesis: verum

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

end;

per cases
( ( k < 0 & l > 0 ) or ( k > 0 & l < 0 ) )
by A4, XREAL_1:133;

end;

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 A5, Def3

.= (1 / (a |^ |.k.|)) |^ |.l.|

.= 1 / ((a |^ |.k.|) |^ |.l.|) by Th7

.= 1 / (a |^ (|.k.| * |.l.|)) by NEWTON:9

.= 1 / (a |^ |.(k * l).|) by COMPLEX1:65

.= (a |^ |.(k * l).|) "

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

:: thesis: verum

end;.= ((a |^ |.k.|) ") |^ |.l.| by A5, Def3

.= (1 / (a |^ |.k.|)) |^ |.l.|

.= 1 / ((a |^ |.k.|) |^ |.l.|) by Th7

.= 1 / (a |^ (|.k.| * |.l.|)) by NEWTON:9

.= 1 / (a |^ |.(k * l).|) by COMPLEX1:65

.= (a |^ |.(k * l).|) "

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

:: thesis: verum