let c1, c2, c3 be Element of COMPLEX ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( ( c2 = 0 & c3 = 0 ) or ( c2 <> 0 & c3 = 0 ) or ( c2 = 0 & c3 <> 0 ) or ( c2 <> 0 & c3 <> 0 ) ) ;

suppose A1: ( c2 = 0 & c3 = 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then A2: Arg c2 = 0 by COMPTRIG:def 1;

per cases ( Arg c1 = 0 or Arg c1 <> 0 ) ;

suppose Arg c1 = 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = 0 + (angle c2,c3) by A1, Lm9;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A1, A2, Lm9; :: thesis: verum

end;

suppose A3: Arg c1 <> 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = ((2 * PI ) - (Arg c1)) + (angle c2,c3) by A1, COMPLEX2:def 5
.= ((2 * PI ) - (Arg c1)) + 0 by A1, A2, Lm9 ;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A1, A3, COMPLEX2:def 5; :: thesis: verum

end;

end;

end;

suppose A4: ( c2 <> 0 & c3 = 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( ( Arg c1 = 0 & Arg c2 = 0 ) or ( Arg c1 <> 0 & Arg c2 = 0 ) or ( Arg c1 = 0 & Arg c2 <> 0 ) or ( Arg c1 <> 0 & Arg c2 <> 0 ) ) ;

suppose A5: ( Arg c1 = 0 & Arg c2 = 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A5; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = ((Arg c2) - (Arg c1)) + (angle c2,c3) by A4, Lm11
.= 0 by A4, A5, Lm9 ;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A4, A5, Lm9; :: thesis: verum

end;

end;

end;

suppose A6: ( Arg c1 <> 0 & Arg c2 = 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = (((2 * PI ) - (Arg c1)) + (Arg c2)) + (angle c2,c3) by A4, Lm13
.= (2 * PI ) - (Arg c1) by A4, A6, Lm9 ;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A4, A6, COMPLEX2:def 5; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then - (- (Arg c1)) <= - 0 by A6;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A6, COMPTRIG:52; :: thesis: verum

end;

end;

end;

suppose A7: ( Arg c1 = 0 & Arg c2 <> 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A7, COMPTRIG:52; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then A8: (angle c1,c2) + (angle c2,c3) = ((Arg c2) - (Arg c1)) + (angle c2,c3) by A4, Lm11
.= (Arg c2) + ((2 * PI ) - (Arg c2)) by A4, A7, COMPLEX2:def 5 ;
angle c1,c3 = 0 by A4, A7, Lm9;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A8; :: thesis: verum

end;

end;

end;

suppose A9: ( Arg c1 <> 0 & Arg c2 <> 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then A10: (angle c1,c2) + (angle c2,c3) = (((2 * PI ) - (Arg c1)) + (Arg c2)) + (angle c2,c3) by A4, Lm13
.= (((2 * PI ) - (Arg c1)) + (Arg c2)) + ((2 * PI ) - (Arg c2)) by A4, A9, COMPLEX2:def 5
.= ((2 * PI ) + (2 * PI )) - (Arg c1) ;
angle c1,c3 = (2 * PI ) - (Arg c1) by A4, A9, COMPLEX2:def 5;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A10; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then A11: (angle c1,c2) + (angle c2,c3) = ((Arg c2) - (Arg c1)) + (angle c2,c3) by A4, Lm11
.= ((Arg c2) - (Arg c1)) + ((2 * PI ) - (Arg c2)) by A4, A9, COMPLEX2:def 5 ;
angle c1,c3 = (2 * PI ) - (Arg c1) by A4, A9, COMPLEX2:def 5;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A11; :: thesis: verum

end;

end;

end;

end;

end;

suppose A12: ( c2 = 0 & c3 <> 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) < 0 ) or ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) < 0 ) or ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) >= 0 ) or ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) >= 0 ) ) ;

suppose ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) < 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (Arg c3) - 0 < 0 by A12, COMPTRIG:def 1;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by COMPTRIG:52; :: thesis: verum

end;

suppose A13: ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) < 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( Arg c1 = 0 or Arg c1 <> 0 ) ;

suppose Arg c1 = 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A13, COMPTRIG:52; :: thesis: verum

end;

suppose Arg c1 <> 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = ((2 * PI ) - (Arg c1)) + (angle c2,c3) by A12, COMPLEX2:def 5
.= ((2 * PI ) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A12, A13, Lm11
.= ((2 * PI ) - (Arg c1)) + ((Arg c3) - 0 ) by A12, COMPTRIG:def 1
.= ((2 * PI ) - (Arg c1)) + (Arg c3) ;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A12, A13, Lm13; :: thesis: verum

end;

end;

end;

suppose ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) >= 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (Arg c3) - 0 < 0 by A12, COMPTRIG:def 1;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by COMPTRIG:52; :: thesis: verum

end;

suppose A14: ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) >= 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( Arg c1 = 0 or Arg c1 <> 0 ) ;

suppose A15: Arg c1 = 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = 0 + (angle c2,c3) by A12, Lm9
.= 0 + ((Arg c3) - (Arg c2)) by A12, A14, Lm11
.= 0 + ((Arg c3) - 0 ) by A12, COMPTRIG:def 1 ;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A12, A14, A15, Lm11; :: thesis: verum

end;

suppose Arg c1 <> 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then A16: (angle c1,c2) + (angle c2,c3) = ((2 * PI ) - (Arg c1)) + (angle c2,c3) by A12, COMPLEX2:def 5
.= ((2 * PI ) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A12, A14, Lm11
.= ((2 * PI ) - (Arg c1)) + ((Arg c3) - 0 ) by A12, COMPTRIG:def 1 ;
angle c1,c3 = (Arg c3) - (Arg c1) by A12, A14, Lm11;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A16; :: thesis: verum

end;

end;

end;

end;

end;

suppose A17: ( c2 <> 0 & c3 <> 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) < 0 ) or ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) < 0 ) or ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) >= 0 ) or ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) >= 0 ) ) ;

suppose A18: ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) < 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then A19: (angle c1,c2) + (angle c2,c3) = (((2 * PI ) - (Arg c1)) + (Arg c2)) + (angle c2,c3) by A17, Lm13
.= (((2 * PI ) - (Arg c1)) + (Arg c2)) + (((2 * PI ) - (Arg c2)) + (Arg c3)) by A17, A18, Lm13
.= (((2 * PI ) + (2 * PI )) - (Arg c1)) + (Arg c3) ;
angle c1,c3 = ((2 * PI ) - (Arg c1)) + (Arg c3) by A17, A18, Lm13;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A19; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = ((Arg c2) - (Arg c1)) + (angle c2,c3) by A17, Lm11
.= ((Arg c2) - (Arg c1)) + (((2 * PI ) - (Arg c2)) + (Arg c3)) by A17, A18, Lm13
.= ((2 * PI ) - (Arg c1)) + (Arg c3) ;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A17, A18, Lm13; :: thesis: verum

end;

end;

end;

suppose A20: ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) < 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = (((2 * PI ) - (Arg c1)) + (Arg c2)) + (angle c2,c3) by A17, Lm13
.= (((2 * PI ) - (Arg c1)) + (Arg c2)) + ((Arg c3) - (Arg c2)) by A17, A20, Lm11
.= ((2 * PI ) - (Arg c1)) + (Arg c3) ;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A17, A20, Lm13; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then ((Arg c2) - (Arg c1)) + ((Arg c3) - (Arg c2)) >= 0 + 0 by A20;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A20; :: thesis: verum

end;

end;

end;

suppose A21: ( (Arg c3) - (Arg c2) < 0 & (Arg c3) - (Arg c1) >= 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then ((Arg c2) - (Arg c1)) + ((Arg c3) - (Arg c2)) < 0 + 0 by A21;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A21; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then A22: (angle c1,c2) + (angle c2,c3) = ((Arg c2) - (Arg c1)) + (angle c2,c3) by A17, Lm11
.= ((Arg c2) - (Arg c1)) + (((2 * PI ) - (Arg c2)) + (Arg c3)) by A17, A21, Lm13
.= ((2 * PI ) - (Arg c1)) + (Arg c3) ;
angle c1,c3 = (Arg c3) - (Arg c1) by A17, A21, Lm11;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A22; :: thesis: verum

end;

end;

end;

suppose A23: ( (Arg c3) - (Arg c2) >= 0 & (Arg c3) - (Arg c1) >= 0 ) ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

per cases ( (Arg c2) - (Arg c1) < 0 or (Arg c2) - (Arg c1) >= 0 ) ;

suppose (Arg c2) - (Arg c1) < 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then A24: (angle c1,c2) + (angle c2,c3) = (((2 * PI ) - (Arg c1)) + (Arg c2)) + (angle c2,c3) by A17, Lm13
.= (((2 * PI ) + (Arg c2)) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A17, A23, Lm11
.= ((2 * PI ) - (Arg c1)) + (Arg c3) ;
angle c1,c3 = (Arg c3) - (Arg c1) by A17, A23, Lm11;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A24; :: thesis: verum

end;

suppose (Arg c2) - (Arg c1) >= 0 ; :: thesis: ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )

then (angle c1,c2) + (angle c2,c3) = ((Arg c2) - (Arg c1)) + (angle c2,c3) by A17, Lm11
.= ((Arg c2) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A17, A23, Lm11
.= (- (Arg c1)) + (Arg c3) ;
hence ( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) ) by A17, A23, Lm11; :: thesis: verum

end;

end;

end;

end;

end;

end;