let x be real number ; :: thesis: for m, n being natural number holds x #Z (n + m) = (x #Z n) * (x #Z m)
let m, n be natural number ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

per cases ( x <> 0 or x = 0 ) ;

suppose x <> 0 ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

hence x #Z (n + m) = (x #Z n) * (x #Z m) by PREPOWER:54; :: thesis: verum

end;

suppose A1: x = 0 ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

thus x #Z (n + m) = (x #Z n) * (x #Z m) :: thesis: verum

proof

A2: 0 #Z (n + m) = 0 |^ (abs (n + m)) by PREPOWER:def 4
.= 0 |^ (n + m) by ABSVALUE:def 1
.= (0 |^ n) * (0 |^ m) by NEWTON:13 ;

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

suppose A3: ( n = 0 & m = 0 ) ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

x #Z (0 + 0 ) = 1 * (x #Z 0 )
.= (x #Z 0 ) * (x #Z 0 ) by PREPOWER:44 ;
hence x #Z (n + m) = (x #Z n) * (x #Z m) by A3; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

then 0 < n ;
then A4: 0 + 1 <= n by NAT_1:13;
then A5: 0 #Z (n + m) = 0 * (0 |^ m) by A2, NEWTON:16;
(0 #Z n) * (0 #Z m) = (0 |^ (abs n)) * (0 #Z m) by PREPOWER:def 4
.= (0 |^ n) * (0 #Z m) by ABSVALUE:def 1
.= 0 * (0 #Z m) by A4, NEWTON:16 ;
hence x #Z (n + m) = (x #Z n) * (x #Z m) by A1, A5; :: thesis: verum

end;

suppose m <> 0 ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

then 0 < m ;
then A6: 0 + 1 <= m by NAT_1:13;
then A7: 0 #Z (n + m) = 0 * (0 |^ n) by A2, NEWTON:16;
(0 #Z n) * (0 #Z m) = (0 |^ (abs m)) * (0 #Z n) by PREPOWER:def 4
.= (0 |^ m) * (0 #Z n) by ABSVALUE:def 1
.= 0 * (0 #Z n) by A6, NEWTON:16 ;
hence x #Z (n + m) = (x #Z n) * (x #Z m) by A1, A7; :: thesis: verum

end;

end;

end;

end;

end;