let c1, c2, c3 be Element of COMPLEX ; ( (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 )
;
( (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
;
( (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;
verum end; suppose A3:
Arg c1 <> 0
;
( (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;
verum end; end; end; suppose A4:
(
c2 <> 0 &
c3 = 0 )
;
( (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 )
;
( (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
;
( (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;
verum end; end; end; suppose A6:
(
Arg c1 <> 0 &
Arg c2 = 0 )
;
( (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
;
( (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;
verum end; end; end; suppose A7:
(
Arg c1 = 0 &
Arg c2 <> 0 )
;
( (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 A8:
(Arg c2) - (Arg c1) >= 0
;
( (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;
verum end; end; end; suppose A10:
(
Arg c1 <> 0 &
Arg c2 <> 0 )
;
( (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
;
( (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;
verum end; suppose A13:
(Arg c2) - (Arg c1) >= 0
;
( (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;
verum end; end; end; end; end; suppose A15:
(
c2 = 0 &
c3 <> 0 )
;
( (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 A16:
(
(Arg c3) - (Arg c2) >= 0 &
(Arg c3) - (Arg c1) < 0 )
;
( (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
;
( (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;
verum end; end; end; suppose A17:
(
(Arg c3) - (Arg c2) >= 0 &
(Arg c3) - (Arg c1) >= 0 )
;
( (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
;
( (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;
verum end; suppose A19:
Arg c1 <> 0
;
( (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;
verum end; end; end; end; end; suppose A21:
(
c2 <> 0 &
c3 <> 0 )
;
( (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 )
;
( (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
;
( (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;
verum end; suppose
(Arg c2) - (Arg c1) >= 0
;
( (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;
verum end; end; end; suppose A25:
(
(Arg c3) - (Arg c2) >= 0 &
(Arg c3) - (Arg c1) < 0 )
;
( (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
;
( (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;
verum end; end; end; suppose A26:
(
(Arg c3) - (Arg c2) < 0 &
(Arg c3) - (Arg c1) >= 0 )
;
( (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 A27:
(Arg c2) - (Arg c1) >= 0
;
( (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;
verum end; end; end; suppose A29:
(
(Arg c3) - (Arg c2) >= 0 &
(Arg c3) - (Arg c1) >= 0 )
;
( (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
;
( (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;
verum end; suppose
(Arg c2) - (Arg c1) >= 0
;
( (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;
verum end; end; end; end; end; end;