let a be Complex; :: thesis: for n being natural Number holds (1 / a) |^ n = 1 / (a |^ n)

let n be natural Number ; :: thesis: (1 / a) |^ n = 1 / (a |^ n)

A1: n is Nat by TARSKI:1;

defpred S_{1}[ Nat] means (1 / a) |^ $1 = 1 / (a |^ $1);

A2: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]

.= 1 / 1

.= 1 / (a |^ 0) by NEWTON:4 ;

then A3: S_{1}[ 0 ]
;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A3, A2);

hence (1 / a) |^ n = 1 / (a |^ n) by A1; :: thesis: verum

let n be natural Number ; :: thesis: (1 / a) |^ n = 1 / (a |^ n)

A1: n is Nat by TARSKI:1;

defpred S

A2: for m being Nat st S

S

proof

(1 / a) |^ 0 =
1
by NEWTON:4
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume (1 / a) |^ m = 1 / (a |^ m) ; :: thesis: S_{1}[m + 1]

hence (1 / a) |^ (m + 1) = (1 / (a |^ m)) * (1 / a) by NEWTON:6

.= (1 * 1) / ((a |^ m) * a) by XCMPLX_1:76

.= 1 / (a |^ (m + 1)) by NEWTON:6 ;

:: thesis: verum

end;assume (1 / a) |^ m = 1 / (a |^ m) ; :: thesis: S

hence (1 / a) |^ (m + 1) = (1 / (a |^ m)) * (1 / a) by NEWTON:6

.= (1 * 1) / ((a |^ m) * a) by XCMPLX_1:76

.= 1 / (a |^ (m + 1)) by NEWTON:6 ;

:: thesis: verum

.= 1 / 1

.= 1 / (a |^ 0) by NEWTON:4 ;

then A3: S

for m being Nat holds S

hence (1 / a) |^ n = 1 / (a |^ n) by A1; :: thesis: verum