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 3
.= ((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 3; :: 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 3; :: 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:34; :: 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:34; :: thesis: verum
end;
suppose A8: (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) )
A9: angle (c1,c3) = 0 by A4, A7, Lm9;
(angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A4, A8, Lm11
.= (Arg c2) + ((2 * PI) - (Arg c2)) by A4, A7, COMPLEX2:def 3 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A9; :: thesis: verum
end;
end;
end;
suppose A10: ( 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 A11: (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) )
A12: angle (c1,c3) = (2 * PI) - (Arg c1) by A4, A10, COMPLEX2:def 3;
(angle (c1,c2)) + (angle (c2,c3)) = (((2 * PI) - (Arg c1)) + (Arg c2)) + (angle (c2,c3)) by A4, A11, Lm13
.= (((2 * PI) - (Arg c1)) + (Arg c2)) + ((2 * PI) - (Arg c2)) by A4, A10, COMPLEX2:def 3
.= ((2 * PI) + (2 * PI)) - (Arg c1) ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A12; :: thesis: verum
end;
suppose A13: (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) )
A14: angle (c1,c3) = (2 * PI) - (Arg c1) by A4, A10, COMPLEX2:def 3;
(angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A4, A13, Lm11
.= ((Arg c2) - (Arg c1)) + ((2 * PI) - (Arg c2)) by A4, A10, COMPLEX2:def 3 ;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A14; :: thesis: verum
end;
end;
end;
end;
end;
suppose A15: ( 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 A15, 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:34; :: thesis: verum
end;
suppose A16: ( (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 A16, COMPTRIG:34; :: 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 A15, COMPLEX2:def 3
.= ((2 * PI) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A15, A16, Lm11
.= ((2 * PI) - (Arg c1)) + ((Arg c3) - 0) by A15, 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 A15, A16, 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 A15, 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:34; :: thesis: verum
end;
suppose A17: ( (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 A18: 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 A15, Lm9
.= 0 + ((Arg c3) - (Arg c2)) by A15, A17, Lm11
.= 0 + ((Arg c3) - 0) by A15, 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 A15, A17, A18, Lm11; :: thesis: verum
end;
suppose A19: 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) )
A20: angle (c1,c3) = (Arg c3) - (Arg c1) by A15, A17, Lm11;
(angle (c1,c2)) + (angle (c2,c3)) = ((2 * PI) - (Arg c1)) + (angle (c2,c3)) by A15, A19, COMPLEX2:def 3
.= ((2 * PI) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A15, A17, Lm11
.= ((2 * PI) - (Arg c1)) + ((Arg c3) - 0) by A15, 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 A20; :: thesis: verum
end;
end;
end;
end;
end;
suppose A21: ( 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 A22: ( (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 A23: (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) )
A24: angle (c1,c3) = ((2 * PI) - (Arg c1)) + (Arg c3) by A21, A22, Lm13;
(angle (c1,c2)) + (angle (c2,c3)) = (((2 * PI) - (Arg c1)) + (Arg c2)) + (angle (c2,c3)) by A21, A23, Lm13
.= (((2 * PI) - (Arg c1)) + (Arg c2)) + (((2 * PI) - (Arg c2)) + (Arg c3)) by A21, A22, Lm13
.= (((2 * PI) + (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 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 A21, Lm11
.= ((Arg c2) - (Arg c1)) + (((2 * PI) - (Arg c2)) + (Arg c3)) by A21, A22, 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 A21, A22, Lm13; :: thesis: verum
end;
end;
end;
suppose A25: ( (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 A21, Lm13
.= (((2 * PI) - (Arg c1)) + (Arg c2)) + ((Arg c3) - (Arg c2)) by A21, A25, 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 A21, A25, 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 A25;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A25; :: thesis: verum
end;
end;
end;
suppose A26: ( (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 A26;
hence ( (angle (c1,c2)) + (angle (c2,c3)) = angle (c1,c3) or (angle (c1,c2)) + (angle (c2,c3)) = (angle (c1,c3)) + (2 * PI) ) by A26; :: thesis: verum
end;
suppose A27: (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) )
A28: angle (c1,c3) = (Arg c3) - (Arg c1) by A21, A26, Lm11;
(angle (c1,c2)) + (angle (c2,c3)) = ((Arg c2) - (Arg c1)) + (angle (c2,c3)) by A21, A27, Lm11
.= ((Arg c2) - (Arg c1)) + (((2 * PI) - (Arg c2)) + (Arg c3)) by A21, A26, 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 A28; :: thesis: verum
end;
end;
end;
suppose A29: ( (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 A30: (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) )
A31: angle (c1,c3) = (Arg c3) - (Arg c1) by A21, A29, Lm11;
(angle (c1,c2)) + (angle (c2,c3)) = (((2 * PI) - (Arg c1)) + (Arg c2)) + (angle (c2,c3)) by A21, A30, Lm13
.= (((2 * PI) + (Arg c2)) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A21, A29, 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 A31; :: 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 A21, Lm11
.= ((Arg c2) - (Arg c1)) + ((Arg c3) - (Arg c2)) by A21, A29, 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 A21, A29, Lm11; :: thesis: verum
end;
end;
end;
end;
end;
end;