let a, b, c be Complex; for r being Real st a <> b & b <> c holds
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))
let r be Real; ( a <> b & b <> c implies angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) )
set cb = c - b;
set ab = a - b;
set rc = Rotate (c,r);
set rb = Rotate (b,r);
set ra = Rotate (a,r);
set rcb = (Rotate (c,r)) - (Rotate (b,r));
set rab = (Rotate (a,r)) - (Rotate (b,r));
assume that
A1:
a <> b
and
A2:
b <> c
; angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))
A3:
( 0 <= angle (a,b,c) & angle (a,b,c) < 2 * PI )
by Th68;
c - b <> 0
by A2;
then consider cbi being Integer such that
A4:
Arg (Rotate ((c - b),r)) = ((2 * PI) * cbi) + (r + (Arg (c - b)))
by Th52;
a - b <> 0
by A1;
then consider abi being Integer such that
A5:
Arg (Rotate ((a - b),r)) = ((2 * PI) * abi) + (r + (Arg (a - b)))
by Th52;
A6:
( 0 <= angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) & angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) < 2 * PI )
by Th68;
(Rotate (a,r)) - (Rotate (b,r)) = Rotate ((a - b),r)
by Th57;
then A7: (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) =
((((2 * PI) * cbi) + r) + (Arg (c - b))) - ((((2 * PI) * abi) + r) + (Arg (a - b)))
by A5, A4, Th57
.=
((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi))
;
per cases
( (Arg (c - b)) - (Arg (a - b)) >= 0 or (Arg (c - b)) - (Arg (a - b)) < 0 )
;
suppose
(Arg (c - b)) - (Arg (a - b)) >= 0
;
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))then A8:
angle (
a,
b,
c)
= (Arg (c - b)) - (Arg (a - b))
by Def4;
thus
angle (
a,
b,
c)
= angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r)))
verumproof
per cases
( (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 or (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 )
;
suppose
(Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0
;
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))then
angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r)))
= (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r))))
by Def4;
hence
angle (
a,
b,
c)
= angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r)))
by A3, A6, A7, A8, Th2;
verum end; suppose
(Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0
;
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))then angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r))) =
(((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi))) + (2 * PI)
by A7, Def4
.=
((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * ((cbi - abi) + 1))
;
hence
angle (
a,
b,
c)
= angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r)))
by A3, A6, A8, Th2;
verum end; end;
end; end; suppose
(Arg (c - b)) - (Arg (a - b)) < 0
;
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))then A9:
angle (
a,
b,
c)
= (2 * PI) + ((Arg (c - b)) - (Arg (a - b)))
by Def4;
thus
angle (
a,
b,
c)
= angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r)))
verumproof
per cases
( (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 or (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 )
;
suppose
(Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0
;
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))then
angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r)))
= ((2 * PI) + ((Arg (c - b)) - (Arg (a - b)))) + ((2 * PI) * ((cbi - abi) + (- 1)))
by A7, Def4;
hence
angle (
a,
b,
c)
= angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r)))
by A3, A6, A9, Th2;
verum end; suppose
(Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0
;
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))then angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r))) =
(((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi))) + (2 * PI)
by A7, Def4
.=
((2 * PI) + ((Arg (c - b)) - (Arg (a - b)))) + ((2 * PI) * (cbi - abi))
;
hence
angle (
a,
b,
c)
= angle (
(Rotate (a,r)),
(Rotate (b,r)),
(Rotate (c,r)))
by A3, A6, A9, Th2;
verum end; end;
end; end; end;