let x be Complex; :: thesis: for r being natural Number st x <> 0 holds

(x |^ r) " = (x ") |^ r

let r be natural Number ; :: thesis: ( x <> 0 implies (x |^ r) " = (x ") |^ r )

assume A1: x <> 0 ; :: thesis: (x |^ r) " = (x ") |^ r

reconsider y = x * (x ") as Complex ;

A2: y = x / x by XCMPLX_0:def 9

.= 1 by A1, XCMPLX_1:60 ;

(x |^ r) * ((x ") |^ r) = y |^ r by NEWTON:7

.= 1 by A2, NEWTON:10 ;

hence (x |^ r) " = (x ") |^ r by XCMPLX_1:210; :: thesis: verum

(x |^ r) " = (x ") |^ r

let r be natural Number ; :: thesis: ( x <> 0 implies (x |^ r) " = (x ") |^ r )

assume A1: x <> 0 ; :: thesis: (x |^ r) " = (x ") |^ r

reconsider y = x * (x ") as Complex ;

A2: y = x / x by XCMPLX_0:def 9

.= 1 by A1, XCMPLX_1:60 ;

(x |^ r) * ((x ") |^ r) = y |^ r by NEWTON:7

.= 1 by A2, NEWTON:10 ;

hence (x |^ r) " = (x ") |^ r by XCMPLX_1:210; :: thesis: verum