begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th19:
Lm1:
Arg 0 = 0
by COMPTRIG:53;
theorem
canceled;
theorem
canceled;
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
begin
:: deftheorem COMPLEX2:def 1 :
canceled;
:: deftheorem COMPLEX2:def 2 :
canceled;
:: deftheorem defines .|. COMPLEX2:def 3 :
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem
theorem Th47:
theorem
theorem Th49:
theorem
theorem Th51:
theorem
theorem
theorem
theorem Th55:
theorem
theorem Th57:
theorem
theorem
theorem Th60:
theorem
canceled;
theorem
theorem Th63:
Lm2:
for z being Element of COMPLEX holds |.z.| ^2 = ((Re z) ^2 ) + ((Im z) ^2 )
theorem Th64:
begin
:: deftheorem defines Rotate COMPLEX2:def 4 :
theorem
theorem Th66:
theorem Th67:
theorem Th68:
theorem
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
begin
:: deftheorem Def5 defines angle COMPLEX2:def 5 :
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem
theorem
theorem
theorem Th83:
:: deftheorem Def6 defines angle COMPLEX2:def 6 :
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem
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 ) )
theorem
theorem Th92:
theorem Th93:
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)
theorem Th94:
theorem
theorem
theorem Th97:
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 Th98:
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 Th99:
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 Th100:
theorem Th101:
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 ) )