let z1, z2 be Complex; :: thesis: ( Arg z1 < PI & Arg z2 < PI implies Arg (z1 + z2) < PI )
assume that
A1: Arg z1 < PI and
A2: Arg z2 < PI ; :: thesis: Arg (z1 + z2) < PI
A3: |.z2.| = |.z2.| + (0 * <i>) ;
A4: |.z1.| = |.z1.| + (0 * <i>) ;
per cases ( Arg z1 = 0 or Arg z1 > 0 ) by COMPTRIG:34;
suppose A5: Arg z1 = 0 ; :: thesis: Arg (z1 + z2) < PI
then z1 = |.z1.| by Th13;
then A6: Im z1 = 0 by A4, COMPLEX1:12;
per cases ( Arg z2 = 0 or Arg z2 > 0 ) by COMPTRIG:34;
suppose Arg z2 = 0 ; :: thesis: Arg (z1 + z2) < PI
then z2 = |.z2.| by Th13;
then A7: z1 + z2 = (|.z1.| + |.z2.|) + (0 * <i>) by A5, Th13;
( 0 <= |.z1.| & 0 <= |.z2.| ) by COMPLEX1:46;
hence Arg (z1 + z2) < PI by A7, COMPTRIG:5, COMPTRIG:35; :: thesis: verum
end;
suppose Arg z2 > 0 ; :: thesis: Arg (z1 + z2) < PI
then Arg z2 in ].0,PI.[ by A2, XXREAL_1:4;
then A8: Im z2 > 0 by Th16;
Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:8;
then Arg (z1 + z2) in ].0,PI.[ by A6, A8, Th16;
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 A9: Im z1 > 0 by Th16;
per cases ( Arg z2 = 0 or Arg z2 > 0 ) by COMPTRIG:34;
suppose Arg z2 = 0 ; :: thesis: Arg (z1 + z2) < PI
then z2 = |.z2.| by Th13;
then A10: Im z2 = 0 by A3, COMPLEX1:12;
Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:8;
then Arg (z1 + z2) in ].0,PI.[ by A9, A10, Th16;
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 A2, XXREAL_1:4;
then A11: Im z2 > 0 by Th16;
Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:8;
then Arg (z1 + z2) in ].0,PI.[ by A9, A11, Th16;
hence Arg (z1 + z2) < PI by XXREAL_1:4; :: thesis: verum
end;
end;
end;
end;