begin
begin
Lm1:
Arg 0 = 0
by COMPTRIG:35;
begin
Lm2:
for z being Element of COMPLEX holds |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2)
begin
begin
Lm3:
for a, b, c being Element of COMPLEX st a <> b & c <> b holds
( Re ((a - b) .|. (c - b)) = 0 iff ( angle (a,b,c) = PI / 2 or angle (a,b,c) = (3 / 2) * PI ) )
Lm4:
for x, y, z being Element of COMPLEX st angle (x,y,z) <> 0 holds
angle (z,y,x) = (2 * PI) - (angle (x,y,z))
Lm5:
for a, b being Element of COMPLEX st Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI holds
( ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = PI & 0 < angle (0c,b,a) & 0 < angle (b,a,0c) )
theorem Th84:
for
a,
b,
c being
Element of
COMPLEX st
a <> b &
b <> c &
0 < angle (
a,
b,
c) &
angle (
a,
b,
c)
< PI holds
(
((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI &
0 < angle (
b,
c,
a) &
0 < angle (
c,
a,
b) )
theorem Th85:
for
a,
b,
c being
Element of
COMPLEX st
a <> b &
b <> c &
angle (
a,
b,
c)
> PI holds
(
((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5
* PI &
angle (
b,
c,
a)
> PI &
angle (
c,
a,
b)
> PI )
Lm6:
for a, b being Element of COMPLEX st Im a = 0 & Re a > 0 & Arg b = PI holds
( ((angle (a,0,b)) + (angle (0,b,a))) + (angle (b,a,0)) = PI & 0 = angle (0,b,a) & 0 = angle (b,a,0) )
theorem Th87:
for
a,
b,
c being
Element of
COMPLEX st
a <> b &
a <> c &
b <> c &
angle (
a,
b,
c)
= 0 & not (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) holds
(
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 )
theorem
for
a,
b,
c being
Element of
COMPLEX holds
( (
((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or
((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5
* PI ) iff (
a <> b &
a <> c &
b <> c ) )