let z be Element of F_Complex; :: thesis: ( 0 <= Re z & Im z = 0 implies |.z.| = Re z )

assume that

A1: 0 <= Re z and

A2: Im z = 0 ; :: thesis: |.z.| = Re z

reconsider a = z as Element of COMPLEX by COMPLFLD:def 1;

|.a.| = |.(Re a).| by A2, COMPLEX1:50;

hence |.z.| = Re z by A1, ABSVALUE:def 1; :: thesis: verum

assume that

A1: 0 <= Re z and

A2: Im z = 0 ; :: thesis: |.z.| = Re z

reconsider a = z as Element of COMPLEX by COMPLFLD:def 1;

|.a.| = |.(Re a).| by A2, COMPLEX1:50;

hence |.z.| = Re z by A1, ABSVALUE:def 1; :: thesis: verum