:: COMPLEX2 semantic presentation

Lemma1: 0. F_Complex = 0
by COMPLFLD:9;

theorem Th1: :: COMPLEX2:1

for b₁, b₂ being Real holds - (b₁ + (b₂ * <i> )) = (- b₁) + ((- b₂) * <i> ) ;

theorem Th2: :: COMPLEX2:2

for b₁, b₂ being real number st b₂ > 0 holds
ex b₃ being real number st
( b₃ = (b₂ * (- [\(b₁ / b₂)/])) + b₁ & 0 <= b₃ & b₃ < b₂ )

proof end;

theorem Th3: :: COMPLEX2:3

for b₁, b₂, b₃ being real number st b₁ > 0 & b₂ >= 0 & b₃ >= 0 & b₂ < b₁ & b₃ < b₁ holds
for b₄ being Integer st b₂ = b₃ + (b₁ * b₄) holds
b₂ = b₃

proof end;

theorem Th4: :: COMPLEX2:4

for b₁, b₂ being real number holds
( sin (b₁ - b₂) = ((sin b₁) * (cos b₂)) - ((cos b₁) * (sin b₂)) & cos (b₁ - b₂) = ((cos b₁) * (cos b₂)) + ((sin b₁) * (sin b₂)) )

proof end;

theorem Th5: :: COMPLEX2:5

for b₁ being real number holds
( sin . (b₁ - PI ) = - (sin . b₁) & cos . (b₁ - PI ) = - (cos . b₁) )

proof end;

theorem Th6: :: COMPLEX2:6

for b₁ being real number holds
( sin (b₁ - PI ) = - (sin b₁) & cos (b₁ - PI ) = - (cos b₁) )

proof end;

theorem Th7: :: COMPLEX2:7

for b₁, b₂ being real number st b₁ in ].0,(PI / 2).[ & b₂ in ].0,(PI / 2).[ holds
( b₁ < b₂ iff sin b₁ < sin b₂ )

proof end;

theorem Th8: :: COMPLEX2:8

for b₁, b₂ being real number st b₁ in ].(PI / 2),PI .[ & b₂ in ].(PI / 2),PI .[ holds
( b₁ < b₂ iff sin b₁ > sin b₂ )

proof end;

theorem Th9: :: COMPLEX2:9

for b₁ being real number
for b₂ being Integer holds sin b₁ = sin (((2 * PI ) * b₂) + b₁)

proof end;

theorem Th10: :: COMPLEX2:10

for b₁ being real number
for b₂ being Integer holds cos b₁ = cos (((2 * PI ) * b₂) + b₁)

proof end;

theorem Th11: :: COMPLEX2:11

for b₁ being real number st sin b₁ = 0 holds
cos b₁ <> 0

proof end;

theorem Th12: :: COMPLEX2:12

for b₁, b₂ being real number st 0 <= b₁ & b₁ < 2 * PI & 0 <= b₂ & b₂ < 2 * PI & sin b₁ = sin b₂ & cos b₁ = cos b₂ holds
b₁ = b₂

proof end;

definition

let c₁ be Element of COMPLEX ;
func F_tize c₁ -> Element of F_Complex equals :: COMPLEX2:def 1
a₁;
correctness by COMPLFLD:def 1;

end;

:: deftheorem Def1 defines F_tize COMPLEX2:def 1 :

theorem Th13: :: COMPLEX2:13

canceled;

theorem Th14: :: COMPLEX2:14

for b₁, b₂ being Element of COMPLEX holds F_tize (b₁ + b₂) = (F_tize b₁) + (F_tize b₂) ;

theorem Th15: :: COMPLEX2:15

for b₁ being Element of COMPLEX holds
( b₁ = 0 iff F_tize b₁ = 0. F_Complex ) by COMPLFLD:9;

Lemma12: for b₁ being complex number holds
( 0 <= Arg b₁ & Arg b₁ < 2 * PI )
by COMPTRIG:52;

Lemma13: 0c = [*0,0*]
by ARYTM_0:def 7;

theorem Th16: :: COMPLEX2:16

canceled;

theorem Th17: :: COMPLEX2:17

canceled;

theorem Th18: :: COMPLEX2:18

canceled;

theorem Th19: :: COMPLEX2:19

for b₁ being complex number holds b₁ = [*(|.b₁.| * (cos (Arg b₁))),(|.b₁.| * (sin (Arg b₁)))*]

proof end;

Lemma15: [**0,0**] = 0 + (0 * <i> )
by HAHNBAN1:def 1;

theorem Th20: :: COMPLEX2:20

Arg 0 = 0 by Lemma15, COMPTRIG:53;

theorem Th21: :: COMPLEX2:21

for b₁ being complex number
for b₂ being Real st b₁ <> 0 & b₁ = [*(|.b₁.| * (cos b₂)),(|.b₁.| * (sin b₂))*] & 0 <= b₂ & b₂ < 2 * PI holds
b₂ = Arg b₁

proof end;

theorem Th22: :: COMPLEX2:22

for b₁ being complex number st b₁ <> 0 holds
( ( Arg b₁ < PI implies Arg (- b₁) = (Arg b₁) + PI ) & ( Arg b₁ >= PI implies Arg (- b₁) = (Arg b₁) - PI ) )

proof end;

theorem Th23: :: COMPLEX2:23

for b₁ being Real st b₁ >= 0 holds
Arg [*b₁,0*] = 0

proof end;

theorem Th24: :: COMPLEX2:24

for b₁ being complex number holds
( Arg b₁ = 0 iff b₁ = [*|.b₁.|,0*] )

proof end;

theorem Th25: :: COMPLEX2:25

for b₁ being complex number st b₁ <> 0 holds
( Arg b₁ < PI iff Arg (- b₁) >= PI )

proof end;

theorem Th26: :: COMPLEX2:26

for b₁, b₂ being complex number st ( b₁ <> b₂ or b₁ - b₂ <> 0 ) holds
( Arg (b₁ - b₂) < PI iff Arg (b₂ - b₁) >= PI )

proof end;

theorem Th27: :: COMPLEX2:27

for b₁ being complex number holds
( Arg b₁ in ].0,PI .[ iff Im b₁ > 0 )

proof end;

theorem Th28: :: COMPLEX2:28

for b₁ being complex number st Arg b₁ <> 0 holds
( Arg b₁ < PI iff sin (Arg b₁) > 0 )

proof end;

theorem Th29: :: COMPLEX2:29

for b₁, b₂ being complex number st Arg b₁ < PI & Arg b₂ < PI holds
Arg (b₁ + b₂) < PI

proof end;

theorem Th30: :: COMPLEX2:30

for b₁ being Real st b₁ > 0 holds
Arg [*0,b₁*] = PI / 2

proof end;

Lemma25: for b₁ being complex number holds
( Arg b₁ in ].0,(PI / 2).[ iff ( Re b₁ > 0 & Im b₁ > 0 ) )
by COMPTRIG:59;

Lemma26: for b₁ being complex number holds
( Arg b₁ in ].(PI / 2),PI .[ iff ( Re b₁ < 0 & Im b₁ > 0 ) )
by COMPTRIG:60;

Lemma27: for b₁ being complex number st Im b₁ > 0 holds
sin (Arg b₁) > 0
by COMPTRIG:63;

theorem Th31: :: COMPLEX2:31

canceled;

theorem Th32: :: COMPLEX2:32

canceled;

theorem Th33: :: COMPLEX2:33

canceled;

theorem Th34: :: COMPLEX2:34

for b₁ being complex number holds
( Arg b₁ = 0 iff ( Re b₁ >= 0 & Im b₁ = 0 ) )

proof end;

theorem Th35: :: COMPLEX2:35

for b₁ being complex number holds
( Arg b₁ = PI iff ( Re b₁ < 0 & Im b₁ = 0 ) )

proof end;

theorem Th36: :: COMPLEX2:36

for b₁ being complex number holds
( Im b₁ = 0 iff ( Arg b₁ = 0 or Arg b₁ = PI ) )

proof end;

theorem Th37: :: COMPLEX2:37

for b₁ being complex number st Arg b₁ <= PI holds
Im b₁ >= 0

proof end;

theorem Th38: :: COMPLEX2:38

for b₁ being Element of COMPLEX st b₁ <> 0 holds
( cos (Arg (- b₁)) = - (cos (Arg b₁)) & sin (Arg (- b₁)) = - (sin (Arg b₁)) )

proof end;

theorem Th39: :: COMPLEX2:39

for b₁ being complex number st b₁ <> 0 holds
( cos (Arg b₁) = (Re b₁) / |.b₁.| & sin (Arg b₁) = (Im b₁) / |.b₁.| )

proof end;

theorem Th40: :: COMPLEX2:40

for b₁ being complex number
for b₂ being Real st b₂ > 0 holds
Arg (b₁ * [*b₂,0*]) = Arg b₁

proof end;

theorem Th41: :: COMPLEX2:41

for b₁ being complex number
for b₂ being Real st b₂ < 0 holds
Arg (b₁ * [*b₂,0*]) = Arg (- b₁)

proof end;

definition

let c₁, c₂ be complex number ;
canceled;
func c₁ .|. c₂ -> Element of COMPLEX equals :: COMPLEX2:def 3
a₁ * (a₂ *' );
correctness by XCMPLX_0:def 2;

end;

:: deftheorem Def2 COMPLEX2:def 2 :

:: deftheorem Def3 defines .|. COMPLEX2:def 3 :

theorem Th42: :: COMPLEX2:42

for b₁, b₂ being Element of COMPLEX holds b₁ .|. b₂ = [*(((Re b₁) * (Re b₂)) + ((Im b₁) * (Im b₂))),((- ((Re b₁) * (Im b₂))) + ((Im b₁) * (Re b₂)))*]

proof end;

theorem Th43: :: COMPLEX2:43

for b₁ being Element of COMPLEX holds
( b₁ .|. b₁ = [*(((Re b₁) * (Re b₁)) + ((Im b₁) * (Im b₁))),0*] & b₁ .|. b₁ = [*(((Re b₁) ^2 ) + ((Im b₁) ^2 )),0*] )

proof end;

theorem Th44: :: COMPLEX2:44

for b₁ being Element of COMPLEX holds
( b₁ .|. b₁ = [*(|.b₁.| ^2 ),0*] & |.b₁.| ^2 = Re (b₁ .|. b₁) )

proof end;

theorem Th45: :: COMPLEX2:45

for b₁, b₂ being Element of COMPLEX holds |.(b₁ .|. b₂).| = |.b₁.| * |.b₂.|

proof end;

theorem Th46: :: COMPLEX2:46

for b₁ being Element of COMPLEX st b₁ .|. b₁ = 0 holds
b₁ = 0

proof end;

theorem Th47: :: COMPLEX2:47

for b₁, b₂ being Element of COMPLEX holds b₁ .|. b₂ = (b₂ .|. b₁) *'

proof end;

theorem Th48: :: COMPLEX2:48

for b₁, b₂, b₃ being Element of COMPLEX holds (b₁ + b₂) .|. b₃ = (b₁ .|. b₃) + (b₂ .|. b₃) ;

theorem Th49: :: COMPLEX2:49

for b₁, b₂, b₃ being Element of COMPLEX holds b₁ .|. (b₂ + b₃) = (b₁ .|. b₂) + (b₁ .|. b₃)

proof end;

theorem Th50: :: COMPLEX2:50

for b₁, b₂, b₃ being Element of COMPLEX holds (b₁ * b₂) .|. b₃ = b₁ * (b₂ .|. b₃) ;

theorem Th51: :: COMPLEX2:51

for b₁, b₂, b₃ being Element of COMPLEX holds b₁ .|. (b₂ * b₃) = (b₂ *' ) * (b₁ .|. b₃)

proof end;

theorem Th52: :: COMPLEX2:52

for b₁, b₂, b₃ being Element of COMPLEX holds (b₁ * b₂) .|. b₃ = b₂ .|. ((b₁ *' ) * b₃)

proof end;

theorem Th53: :: COMPLEX2:53

for b₁, b₂, b₃, b₄, b₅ being Element of COMPLEX holds ((b₁ * b₂) + (b₃ * b₄)) .|. b₅ = (b₁ * (b₂ .|. b₅)) + (b₃ * (b₄ .|. b₅)) ;

theorem Th54: :: COMPLEX2:54

for b₁, b₂, b₃, b₄, b₅ being Element of COMPLEX holds b₁ .|. ((b₂ * b₃) + (b₄ * b₅)) = ((b₂ *' ) * (b₁ .|. b₃)) + ((b₄ *' ) * (b₁ .|. b₅))

proof end;

theorem Th55: :: COMPLEX2:55

for b₁, b₂ being Element of COMPLEX holds (- b₁) .|. b₂ = b₁ .|. (- b₂)

proof end;

theorem Th56: :: COMPLEX2:56

for b₁, b₂ being Element of COMPLEX holds (- b₁) .|. b₂ = - (b₁ .|. b₂) ;

theorem Th57: :: COMPLEX2:57

for b₁, b₂ being Element of COMPLEX holds - (b₁ .|. b₂) = b₁ .|. (- b₂)

proof end;

theorem Th58: :: COMPLEX2:58

for b₁, b₂ being Element of COMPLEX holds (- b₁) .|. (- b₂) = b₁ .|. b₂

proof end;

theorem Th59: :: COMPLEX2:59

for b₁, b₂, b₃ being Element of COMPLEX holds (b₁ - b₂) .|. b₃ = (b₁ .|. b₃) - (b₂ .|. b₃) ;

theorem Th60: :: COMPLEX2:60

for b₁, b₂, b₃ being Element of COMPLEX holds b₁ .|. (b₂ - b₃) = (b₁ .|. b₂) - (b₁ .|. b₃)

proof end;

theorem Th61: :: COMPLEX2:61

for b₁ being Element of COMPLEX holds
( 0 .|. b₁ = 0c & b₁ .|. 0 = 0 ) by COMPLEX1:113;

theorem Th62: :: COMPLEX2:62

for b₁, b₂ being Element of COMPLEX holds (b₁ + b₂) .|. (b₁ + b₂) = (((b₁ .|. b₁) + (b₁ .|. b₂)) + (b₂ .|. b₁)) + (b₂ .|. b₂)

proof end;

theorem Th63: :: COMPLEX2:63

for b₁, b₂ being Element of COMPLEX holds (b₁ - b₂) .|. (b₁ - b₂) = (((b₁ .|. b₁) - (b₁ .|. b₂)) - (b₂ .|. b₁)) + (b₂ .|. b₂)

proof end;

Lemma47: for b₁ being Element of COMPLEX holds |.b₁.| ^2 = ((Re b₁) ^2 ) + ((Im b₁) ^2 )

proof end;

theorem Th64: :: COMPLEX2:64

for b₁, b₂ being Element of COMPLEX holds
( Re (b₁ .|. b₂) = 0 iff ( Im (b₁ .|. b₂) = |.b₁.| * |.b₂.| or Im (b₁ .|. b₂) = - (|.b₁.| * |.b₂.|) ) )

proof end;

definition

let c₁ be complex number ;
let c₂ be Real;
func Rotate c₁,c₂ -> Element of COMPLEX equals :: COMPLEX2:def 4
[*(|.a₁.| * (cos (a₂ + (Arg a₁)))),(|.a₁.| * (sin (a₂ + (Arg a₁))))*];
correctness ;

end;

:: deftheorem Def4 defines Rotate COMPLEX2:def 4 :

theorem Th65: :: COMPLEX2:65

for b₁ being Element of COMPLEX holds Rotate b₁,0 = b₁ by Th19;

theorem Th66: :: COMPLEX2:66

for b₁ being Element of COMPLEX
for b₂ being Real holds
( Rotate b₁,b₂ = 0 iff b₁ = 0 )

proof end;

theorem Th67: :: COMPLEX2:67

for b₁ being Element of COMPLEX
for b₂ being Real holds |.(Rotate b₁,b₂).| = |.b₁.|

proof end;

theorem Th68: :: COMPLEX2:68

for b₁ being Element of COMPLEX
for b₂ being Real st b₁ <> 0 holds
ex b₃ being Integer st Arg (Rotate b₁,b₂) = ((2 * PI ) * b₃) + (b₂ + (Arg b₁))

proof end;

theorem Th69: :: COMPLEX2:69

for b₁ being Element of COMPLEX holds Rotate b₁,(- (Arg b₁)) = [*|.b₁.|,0*] by SIN_COS:34;

theorem Th70: :: COMPLEX2:70

for b₁ being Element of COMPLEX
for b₂ being Real holds
( Re (Rotate b₁,b₂) = ((Re b₁) * (cos b₂)) - ((Im b₁) * (sin b₂)) & Im (Rotate b₁,b₂) = ((Re b₁) * (sin b₂)) + ((Im b₁) * (cos b₂)) )

proof end;

theorem Th71: :: COMPLEX2:71

for b₁, b₂ being Element of COMPLEX
for b₃ being Real holds Rotate (b₁ + b₂),b₃ = (Rotate b₁,b₃) + (Rotate b₂,b₃)

proof end;

theorem Th72: :: COMPLEX2:72

for b₁ being Element of COMPLEX
for b₂ being Real holds Rotate (- b₁),b₂ = - (Rotate b₁,b₂)

proof end;

theorem Th73: :: COMPLEX2:73

for b₁, b₂ being Element of COMPLEX
for b₃ being Real holds Rotate (b₁ - b₂),b₃ = (Rotate b₁,b₃) - (Rotate b₂,b₃)

proof end;

theorem Th74: :: COMPLEX2:74

for b₁ being Element of COMPLEX holds Rotate b₁,PI = - b₁

proof end;

definition

let c₁, c₂ be Element of COMPLEX ;
func angle c₁,c₂ -> Real equals :Def5: :: COMPLEX2:def 5
Arg (Rotate a₂,(- (Arg a₁))) if ( Arg a₁ = 0 or a₂ <> 0 )
otherwise (2 * PI ) - (Arg a₁);
correctness ;

end;

:: deftheorem Def5 defines angle COMPLEX2:def 5 :

theorem Th75: :: COMPLEX2:75

for b₁ being Element of COMPLEX
for b₂ being Real st b₂ >= 0 holds
angle [*b₂,0*],b₁ = Arg b₁

proof end;

theorem Th76: :: COMPLEX2:76

for b₁, b₂ being Element of COMPLEX
for b₃ being Real st Arg b₁ = Arg b₂ & b₁ <> 0 & b₂ <> 0 holds
Arg (Rotate b₁,b₃) = Arg (Rotate b₂,b₃)

proof end;

theorem Th77: :: COMPLEX2:77

for b₁, b₂ being Element of COMPLEX
for b₃ being Real st b₃ > 0 holds
angle b₁,b₂ = angle (b₁ * [*b₃,0*]),(b₂ * [*b₃,0*])

proof end;

theorem Th78: :: COMPLEX2:78

for b₁, b₂ being Element of COMPLEX st b₁ <> 0 & b₂ <> 0 & Arg b₁ = Arg b₂ holds
Arg (- b₁) = Arg (- b₂)

proof end;

theorem Th79: :: COMPLEX2:79

for b₁, b₂ being Element of COMPLEX
for b₃ being Real st b₁ <> 0 & b₂ <> 0 holds
angle b₁,b₂ = angle (Rotate b₁,b₃),(Rotate b₂,b₃)

proof end;

theorem Th80: :: COMPLEX2:80

for b₁, b₂ being Element of COMPLEX
for b₃ being Real st b₃ < 0 & b₁ <> 0 & b₂ <> 0 holds
angle b₁,b₂ = angle (b₁ * [*b₃,0*]),(b₂ * [*b₃,0*])

proof end;

theorem Th81: :: COMPLEX2:81

for b₁, b₂ being Element of COMPLEX st b₁ <> 0 & b₂ <> 0 holds
angle b₁,b₂ = angle (- b₁),(- b₂)

proof end;

theorem Th82: :: COMPLEX2:82

for b₁, b₂ being Element of COMPLEX st b₁ <> 0 & angle b₂,b₁ = 0 holds
angle b₂,(- b₁) = PI

proof end;

theorem Th83: :: COMPLEX2:83

for b₁, b₂ being Element of COMPLEX st b₁ <> 0 & b₂ <> 0 holds
( cos (angle b₁,b₂) = (Re (b₁ .|. b₂)) / (|.b₁.| * |.b₂.|) & sin (angle b₁,b₂) = - ((Im (b₁ .|. b₂)) / (|.b₁.| * |.b₂.|)) )

proof end;

definition

let c₁, c₂, c₃ be complex number ;
func angle c₁,c₂,c₃ -> real number equals :Def6: :: COMPLEX2:def 6
(Arg (a₃ - a₂)) - (Arg (a₁ - a₂)) if (Arg (a₃ - a₂)) - (Arg (a₁ - a₂)) >= 0
otherwise (2 * PI ) + ((Arg (a₃ - a₂)) - (Arg (a₁ - a₂)));
correctness ;

end;

:: deftheorem Def6 defines angle COMPLEX2:def 6 :

theorem Th84: :: COMPLEX2:84

for b₁, b₂, b₃ being Element of COMPLEX holds
( 0 <= angle b₁,b₂,b₃ & angle b₁,b₂,b₃ < 2 * PI )

proof end;

theorem Th85: :: COMPLEX2:85

for b₁, b₂, b₃ being Element of COMPLEX holds angle b₁,b₂,b₃ = angle (b₁ - b₂),0,(b₃ - b₂)

proof end;

theorem Th86: :: COMPLEX2:86

for b₁, b₂, b₃, b₄ being Element of COMPLEX holds angle b₁,b₂,b₃ = angle (b₁ + b₄),(b₂ + b₄),(b₃ + b₄)

proof end;

theorem Th87: :: COMPLEX2:87

for b₁, b₂ being Element of COMPLEX holds angle b₁,b₂ = angle b₁,0,b₂

proof end;

theorem Th88: :: COMPLEX2:88

for b₁, b₂, b₃ being Element of COMPLEX st angle b₁,b₂,b₃ = 0 holds
( Arg (b₁ - b₂) = Arg (b₃ - b₂) & angle b₃,b₂,b₁ = 0 )

proof end;

theorem Th89: :: COMPLEX2:89

for b₁, b₂ being Element of COMPLEX st b₁ <> 0 & b₂ <> 0 holds
( Re (b₁ .|. b₂) = 0 iff ( angle b₁,0,b₂ = PI / 2 or angle b₁,0,b₂ = (3 / 2) * PI ) )

proof end;

theorem Th90: :: COMPLEX2:90

for b₁, b₂ being Element of COMPLEX st b₁ <> 0 & b₂ <> 0 holds
( ( ( not Im (b₁ .|. b₂) = |.b₁.| * |.b₂.| & not Im (b₁ .|. b₂) = - (|.b₁.| * |.b₂.|) ) or angle b₁,0,b₂ = PI / 2 or angle b₁,0,b₂ = (3 / 2) * PI ) & ( ( not angle b₁,0,b₂ = PI / 2 & not angle b₁,0,b₂ = (3 / 2) * PI ) or Im (b₁ .|. b₂) = |.b₁.| * |.b₂.| or Im (b₁ .|. b₂) = - (|.b₁.| * |.b₂.|) ) )

proof end;

Lemma73: for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> b₂ & b₃ <> b₂ holds
( Re ((b₁ - b₂) .|. (b₃ - b₂)) = 0 iff ( angle b₁,b₂,b₃ = PI / 2 or angle b₁,b₂,b₃ = (3 / 2) * PI ) )

proof end;

theorem Th91: :: COMPLEX2:91

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> b₂ & b₃ <> b₂ & ( angle b₁,b₂,b₃ = PI / 2 or angle b₁,b₂,b₃ = (3 / 2) * PI ) holds
(|.(b₁ - b₂).| ^2 ) + (|.(b₃ - b₂).| ^2 ) = |.(b₁ - b₃).| ^2

proof end;

theorem Th92: :: COMPLEX2:92

for b₁, b₂, b₃ being Element of COMPLEX
for b₄ being Real st b₁ <> b₂ & b₂ <> b₃ holds
angle b₁,b₂,b₃ = angle (Rotate b₁,b₄),(Rotate b₂,b₄),(Rotate b₃,b₄)

proof end;

theorem Th93: :: COMPLEX2:93

for b₁, b₂ being Element of COMPLEX holds angle b₁,b₂,b₁ = 0

proof end;

Lemma76: for b₁, b₂, b₃ being Element of COMPLEX st angle b₁,b₂,b₃ <> 0 holds
angle b₃,b₂,b₁ = (2 * PI ) - (angle b₁,b₂,b₃)

proof end;

theorem Th94: :: COMPLEX2:94

for b₁, b₂, b₃ being Element of COMPLEX holds
( angle b₁,b₂,b₃ <> 0 iff (angle b₁,b₂,b₃) + (angle b₃,b₂,b₁) = 2 * PI )

proof end;

theorem Th95: :: COMPLEX2:95

for b₁, b₂, b₃ being Element of COMPLEX st angle b₁,b₂,b₃ <> 0 holds
angle b₃,b₂,b₁ <> 0

proof end;

theorem Th96: :: COMPLEX2:96

for b₁, b₂, b₃ being Element of COMPLEX st angle b₁,b₂,b₃ = PI holds
angle b₃,b₂,b₁ = PI

proof end;

theorem Th97: :: COMPLEX2:97

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> b₂ & b₁ <> b₃ & b₂ <> b₃ & not angle b₁,b₂,b₃ <> 0 & not angle b₂,b₃,b₁ <> 0 holds
angle b₃,b₁,b₂ <> 0

proof end;

Lemma79: for b₁, b₂ being Element of COMPLEX st Im b₁ = 0 & Re b₁ > 0 & 0 < Arg b₂ & Arg b₂ < PI holds
( ((angle b₁,0c ,b₂) + (angle 0c ,b₂,b₁)) + (angle b₂,b₁,0c ) = PI & 0 < angle 0c ,b₂,b₁ & 0 < angle b₂,b₁,0c )

proof end;

theorem Th98: :: COMPLEX2:98

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> b₂ & b₂ <> b₃ & 0 < angle b₁,b₂,b₃ & angle b₁,b₂,b₃ < PI holds
( ((angle b₁,b₂,b₃) + (angle b₂,b₃,b₁)) + (angle b₃,b₁,b₂) = PI & 0 < angle b₂,b₃,b₁ & 0 < angle b₃,b₁,b₂ )

proof end;

theorem Th99: :: COMPLEX2:99

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> b₂ & b₂ <> b₃ & angle b₁,b₂,b₃ > PI holds
( ((angle b₁,b₂,b₃) + (angle b₂,b₃,b₁)) + (angle b₃,b₁,b₂) = 5 * PI & angle b₂,b₃,b₁ > PI & angle b₃,b₁,b₂ > PI )

proof end;

Lemma82: for b₁, b₂ being Element of COMPLEX st Im b₁ = 0 & Re b₁ > 0 & Arg b₂ = PI holds
( ((angle b₁,0,b₂) + (angle 0,b₂,b₁)) + (angle b₂,b₁,0) = PI & 0 = angle 0,b₂,b₁ & 0 = angle b₂,b₁,0 )

proof end;

theorem Th100: :: COMPLEX2:100

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> b₂ & b₂ <> b₃ & angle b₁,b₂,b₃ = PI holds
( angle b₂,b₃,b₁ = 0 & angle b₃,b₁,b₂ = 0 )

proof end;

theorem Th101: :: COMPLEX2:101

for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> b₂ & b₁ <> b₃ & b₂ <> b₃ & angle b₁,b₂,b₃ = 0 & not ( angle b₂,b₃,b₁ = 0 & angle b₃,b₁,b₂ = PI ) holds
( angle b₂,b₃,b₁ = PI & angle b₃,b₁,b₂ = 0 )

proof end;

Lemma85: for b₁, b₂, b₃ being Element of COMPLEX st b₁ <> b₂ & b₁ <> b₃ & b₂ <> b₃ & angle b₁,b₂,b₃ = 0 holds
(angle b₂,b₃,b₁) + (angle b₃,b₁,b₂) = PI

proof end;

theorem Th102: :: COMPLEX2:102

for b₁, b₂, b₃ being Element of COMPLEX holds
( ( ((angle b₁,b₂,b₃) + (angle b₂,b₃,b₁)) + (angle b₃,b₁,b₂) = PI or ((angle b₁,b₂,b₃) + (angle b₂,b₃,b₁)) + (angle b₃,b₁,b₂) = 5 * PI ) iff ( b₁ <> b₂ & b₁ <> b₃ & b₂ <> b₃ ) )

proof end;