let r be Real; :: thesis: ( r >= 0 implies Arg r = 0 )
assume A1: r >= 0 ; :: thesis: Arg r = 0
A2: |.r.| = r by A1, ABSVALUE:def 1;
A3: ( r = r + (0 * <i> ) & r = (|.r.| * (cos (Arg r))) + ((|.r.| * (sin (Arg r))) * <i> ) ) by Th19;
then A4: r = |.r.| * (cos (Arg r)) by COMPLEX1:163;

per cases ( r = 0 or r > 0 ) by A1;

suppose r = 0 ; :: thesis: Arg r = 0

hence Arg r = 0 by COMPTRIG:53; :: thesis: verum

end;

suppose A5: r > 0 ; :: thesis: Arg r = 0

A6: ( 0 <= Arg r & Arg r < 2 * PI ) by COMPTRIG:52;
( cos (Arg r) = 1 & sin (Arg r) = 0 ) by A2, A3, A4, A5, XCMPLX_1:7;
hence Arg r = 0 by A6, Th12, SIN_COS:34; :: thesis: verum

end;

end;