let z1, z2 be complex number ; :: thesis: ( Arg z1 < PI & Arg z2 < PI implies Arg (z1 + z2) < PI )
assume A1: ( Arg z1 < PI & Arg z2 < PI ) ; :: thesis: Arg (z1 + z2) < PI
A2: |.z2.| = |.z2.| + (0 * <i> ) ;
A3: |.z1.| = |.z1.| + (0 * <i> ) ;

per cases ( Arg z1 = 0 or Arg z1 > 0 ) by COMPTRIG:52;

suppose B4: Arg z1 = 0 ; :: thesis: Arg (z1 + z2) < PI

then z1 = |.z1.| by Th24;
then A5: ( z1 = |.z1.| & Im z1 = 0 ) by A3, COMPLEX1:28;

per cases ( Arg z2 = 0 or Arg z2 > 0 ) by COMPTRIG:52;

suppose Arg z2 = 0 ; :: thesis: Arg (z1 + z2) < PI

then B7: z2 = |.z2.| by Th24;
A10: z1 + z2 = (|.z1.| + |.z2.|) + (0 * <i> ) by B4, B7, Th24;
A11: 0 <= |.z1.| by COMPLEX1:132;
0 <= |.z2.| by COMPLEX1:132;
hence Arg (z1 + z2) < PI by A10, COMPTRIG:21, COMPTRIG:53, A11; :: thesis: verum

end;

suppose Arg z2 > 0 ; :: thesis: Arg (z1 + z2) < PI

then Arg z2 in ].0 ,PI .[ by A1, XXREAL_1:4;
then A12: Im z2 > 0 by Th27;
Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:19;
then Arg (z1 + z2) in ].0 ,PI .[ by A5, A12, Th27;
hence Arg (z1 + z2) < PI by XXREAL_1:4; :: thesis: verum

end;

end;

end;

suppose Arg z1 > 0 ; :: thesis: Arg (z1 + z2) < PI

then Arg z1 in ].0 ,PI .[ by A1, XXREAL_1:4;
then A13: Im z1 > 0 by Th27;

per cases ( Arg z2 = 0 or Arg z2 > 0 ) by COMPTRIG:52;

suppose Arg z2 = 0 ; :: thesis: Arg (z1 + z2) < PI

then z2 = |.z2.| by Th24;
then A14: ( z2 = |.z2.| & Im z2 = 0 ) by A2, COMPLEX1:28;
Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:19;
then Arg (z1 + z2) in ].0 ,PI .[ by A13, A14, Th27;
hence Arg (z1 + z2) < PI by XXREAL_1:4; :: thesis: verum

end;

suppose Arg z2 > 0 ; :: thesis: Arg (z1 + z2) < PI

then Arg z2 in ].0 ,PI .[ by A1, XXREAL_1:4;
then A15: Im z2 > 0 by Th27;
Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:19;
then Arg (z1 + z2) in ].0 ,PI .[ by Th27, A13, A15;
hence Arg (z1 + z2) < PI by XXREAL_1:4; :: thesis: verum

end;

end;

end;

end;