let p be Real; for z being Complex st p > 0 holds
( Re (z / (p * <i>)) = (Im z) / p & Im (z / (p * <i>)) = - ((Re z) / p) & |.(z / p).| = |.z.| / p )
let z be Complex; ( p > 0 implies ( Re (z / (p * <i>)) = (Im z) / p & Im (z / (p * <i>)) = - ((Re z) / p) & |.(z / p).| = |.z.| / p ) )
assume A1:
p > 0
; ( Re (z / (p * <i>)) = (Im z) / p & Im (z / (p * <i>)) = - ((Re z) / p) & |.(z / p).| = |.z.| / p )
A2:
( Re (0 + (p * <i>)) = 0 & Im (0 + (p * <i>)) = p )
by COMPLEX1:12;
A3:
Im (p + (0 * <i>)) = 0
by COMPLEX1:12;
A4: z / (p * <i>) =
((((Re z) * 0) + ((Im z) * p)) / ((0 ^2) + (p ^2))) + ((((0 * (Im z)) - ((Re z) * p)) / ((0 ^2) + (p ^2))) * <i>)
by A2, COMPLEX1:86
.=
(((Im z) * p) / (p * p)) + ((((- (Re z)) * p) / (p * p)) * <i>)
.=
(((Im z) * p) / (p * p)) + (((- (Re z)) / p) * <i>)
by A1, XCMPLX_1:91
.=
((Im z) / p) + ((- ((Re z) / p)) * <i>)
by A1, XCMPLX_1:91
;
|.(z / p).| =
|.z.| / |.p.|
by COMPLEX1:67
.=
|.z.| / (sqrt (p ^2))
by A3, COMPLEX1:12
;
hence
( Re (z / (p * <i>)) = (Im z) / p & Im (z / (p * <i>)) = - ((Re z) / p) & |.(z / p).| = |.z.| / p )
by A1, A4, COMPLEX1:12, SQUARE_1:22; verum