let z1, z2 be Complex; ( Re z1 >= 0 & Re z2 >= 0 & Im z1 >= 0 & Im z2 >= 0 & z1 ^2 = z2 ^2 & z1 ^2 is Real implies z1 = z2 )
assume A1:
( Re z1 >= 0 & Re z2 >= 0 & Im z1 >= 0 & Im z2 >= 0 & z1 ^2 = z2 ^2 & z1 ^2 is Real & z1 <> z2 )
; contradiction
A2:
( z1 ^2 = z1 * z1 & z2 ^2 = z2 * z2 )
by SQUARE_1:def 1;
A3:
Re (z1 * z1) = ((Re z1) * (Re z1)) - ((Im z1) * (Im z1))
by COMPLEX1:9;
A4:
Re (z2 * z2) = ((Re z2) * (Re z2)) - ((Im z2) * (Im z2))
by COMPLEX1:9;
A5:
Re (z1 * z1) = Re (z2 * z2)
by A2, A1;
A6: 0 =
Im (z2 ^2)
by A1, COMPLEX1:def 2
.=
Im (z2 * z2)
by SQUARE_1:def 1
.=
((Im z2) * (Re z2)) + ((Im z2) * (Re z2))
by COMPLEX1:9
;
0 =
Im (z1 ^2)
by A1, COMPLEX1:def 2
.=
((Im z1) * (Re z1)) + ((Im z1) * (Re z1))
by A2, COMPLEX1:9
;
per cases then
( ( Im z1 = 0 & Im z2 = 0 ) or ( Im z1 = 0 & Re z2 = 0 ) or ( Im z2 = 0 & Re z1 = 0 ) or ( Re z1 = 0 & Re z2 = 0 ) )
by A6;
suppose A9:
(
Im z1 = 0 &
Re z2 = 0 )
;
contradictionthen A10:
Im z2 = 0
by A2, A1, A3, A4;
Re z1 = 0
by A2, A9, A1, A3, A4;
hence
contradiction
by A10, A9, COMPLEX1:def 3, A1;
verum end; suppose A11:
(
Im z2 = 0 &
Re z1 = 0 )
;
contradictionthen A12:
Im z1 = 0
by A2, A1, A3, A4;
Re z2 = 0
by A2, A11, A1, A3, A4;
hence
contradiction
by A12, A11, COMPLEX1:def 3, A1;
verum end;