let r be Real; :: thesis: ( r >= 0 implies Arg r = 0 )
assume A1: r >= 0 ; :: thesis: Arg r = 0
B2: r = r + (0 * <i> ) ;
A2: |.r.| = r by A1, ABSVALUE:def 1;
B3: r = (|.r.| * (cos (Arg r))) + ((|.r.| * (sin (Arg r))) * <i> ) by Th19;
then A3: ( r = |.r.| * (cos (Arg r)) & 0 = |.r.| * (sin (Arg r)) ) by B2, 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 A4: r > 0 ; :: thesis: Arg r = 0

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

end;

end;