:: COMPLEX2 semantic presentation

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

theorem :: COMPLEX2:1

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

theorem Th2: :: COMPLEX2:2

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

proof end;

theorem Th3: :: COMPLEX2:3

for a, b, c being real number st a > 0 & b >= 0 & c >= 0 & b < a & c < a holds
for i being Integer st b = c + (a * i) holds
b = c

proof end;

theorem Th4: :: COMPLEX2:4

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

proof end;

theorem :: COMPLEX2:5

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

proof end;

theorem Th6: :: COMPLEX2:6

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

proof end;

theorem Th7: :: COMPLEX2:7

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

proof end;

theorem Th8: :: COMPLEX2:8

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

proof end;

theorem Th9: :: COMPLEX2:9

for a being real number
for i being Integer holds sin a = sin (((2 * PI ) * i) + a)

proof end;

theorem Th10: :: COMPLEX2:10

for a being real number
for i being Integer holds cos a = cos (((2 * PI ) * i) + a)

proof end;

theorem Th11: :: COMPLEX2:11

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

proof end;

theorem Th12: :: COMPLEX2:12

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

proof end;

definition

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

end;

:: deftheorem defines F_tize COMPLEX2:def 1 :

theorem :: COMPLEX2:13

canceled;

theorem :: COMPLEX2:14

for x, y being Element of COMPLEX holds F_tize (x + y) = (F_tize x) + (F_tize y) ;

theorem :: COMPLEX2:15

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

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

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

theorem :: COMPLEX2:16

canceled;

theorem :: COMPLEX2:17

canceled;

theorem :: COMPLEX2:18

canceled;

theorem Th19: :: COMPLEX2:19

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

proof end;

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

theorem Th20: :: COMPLEX2:20

Arg 0 = 0 by Lm4, COMPTRIG:53;

theorem Th21: :: COMPLEX2:21

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

proof end;

theorem Th22: :: COMPLEX2:22

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

proof end;

theorem Th23: :: COMPLEX2:23

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

proof end;

theorem Th24: :: COMPLEX2:24

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

proof end;

theorem Th25: :: COMPLEX2:25

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

proof end;

theorem Th26: :: COMPLEX2:26

for x, y being complex number st ( x <> y or x - y <> 0 ) holds
( Arg (x - y) < PI iff Arg (y - x) >= PI )

proof end;

theorem Th27: :: COMPLEX2:27

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

proof end;

theorem :: COMPLEX2:28

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

proof end;

theorem :: COMPLEX2:29

for x, y being complex number st Arg x < PI & Arg y < PI holds
Arg (x + y) < PI

proof end;

theorem Th30: :: COMPLEX2:30

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

proof end;

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

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

Lm7: for z being complex number st Im z > 0 holds
sin (Arg z) > 0
by COMPTRIG:63;

theorem :: COMPLEX2:31

canceled;

theorem :: COMPLEX2:32

canceled;

theorem :: COMPLEX2:33

canceled;

theorem Th34: :: COMPLEX2:34

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

proof end;

theorem Th35: :: COMPLEX2:35

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

proof end;

theorem Th36: :: COMPLEX2:36

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

proof end;

theorem Th37: :: COMPLEX2:37

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

proof end;

theorem Th38: :: COMPLEX2:38

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

proof end;

theorem Th39: :: COMPLEX2:39

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

proof end;

theorem Th40: :: COMPLEX2:40

for a being complex number
for r being Real st r > 0 holds
Arg (a * [*r,0*]) = Arg a

proof end;

theorem Th41: :: COMPLEX2:41

for a being complex number
for r being Real st r < 0 holds
Arg (a * [*r,0*]) = Arg (- a)

proof end;

definition

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

end;

:: deftheorem COMPLEX2:def 2 :

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

theorem Th42: :: COMPLEX2:42

for x, y being Element of COMPLEX holds x .|. y = [*(((Re x) * (Re y)) + ((Im x) * (Im y))),((- ((Re x) * (Im y))) + ((Im x) * (Re y)))*]

proof end;

theorem Th43: :: COMPLEX2:43

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

proof end;

theorem Th44: :: COMPLEX2:44

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

proof end;

theorem Th45: :: COMPLEX2:45

for x, y being Element of COMPLEX holds |.(x .|. y).| = |.x.| * |.y.|

proof end;

theorem :: COMPLEX2:46

for x being Element of COMPLEX st x .|. x = 0 holds
x = 0

proof end;

theorem Th47: :: COMPLEX2:47

for y, x being Element of COMPLEX holds y .|. x = (x .|. y) *'

proof end;

theorem :: COMPLEX2:48

for x, y, z being Element of COMPLEX holds (x + y) .|. z = (x .|. z) + (y .|. z) ;

theorem Th49: :: COMPLEX2:49

for x, y, z being Element of COMPLEX holds x .|. (y + z) = (x .|. y) + (x .|. z)

proof end;

theorem :: COMPLEX2:50

for a, x, y being Element of COMPLEX holds (a * x) .|. y = a * (x .|. y) ;

theorem Th51: :: COMPLEX2:51

for x, a, y being Element of COMPLEX holds x .|. (a * y) = (a *' ) * (x .|. y)

proof end;

theorem :: COMPLEX2:52

for a, x, y being Element of COMPLEX holds (a * x) .|. y = x .|. ((a *' ) * y)

proof end;

theorem :: COMPLEX2:53

for a, x, b, y, z being Element of COMPLEX holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) ;

theorem :: COMPLEX2:54

for x, a, y, b, z being Element of COMPLEX holds x .|. ((a * y) + (b * z)) = ((a *' ) * (x .|. y)) + ((b *' ) * (x .|. z))

proof end;

theorem Th55: :: COMPLEX2:55

for x, y being Element of COMPLEX holds (- x) .|. y = x .|. (- y)

proof end;

theorem :: COMPLEX2:56

for x, y being Element of COMPLEX holds (- x) .|. y = - (x .|. y) ;

theorem Th57: :: COMPLEX2:57

for x, y being Element of COMPLEX holds - (x .|. y) = x .|. (- y)

proof end;

theorem :: COMPLEX2:58

for x, y being Element of COMPLEX holds (- x) .|. (- y) = x .|. y

proof end;

theorem :: COMPLEX2:59

for x, y, z being Element of COMPLEX holds (x - y) .|. z = (x .|. z) - (y .|. z) ;

theorem Th60: :: COMPLEX2:60

for x, y, z being Element of COMPLEX holds x .|. (y - z) = (x .|. y) - (x .|. z)

proof end;

theorem :: COMPLEX2:61

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

theorem :: COMPLEX2:62

for x, y being Element of COMPLEX holds (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)

proof end;

theorem Th63: :: COMPLEX2:63

for x, y being Element of COMPLEX holds (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y)

proof end;

Lm8: for z being Element of COMPLEX holds |.z.| ^2 = ((Re z) ^2 ) + ((Im z) ^2 )

proof end;

theorem Th64: :: COMPLEX2:64

for x, y being Element of COMPLEX holds
( Re (x .|. y) = 0 iff ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) )

proof end;

definition

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

end;

:: deftheorem defines Rotate COMPLEX2:def 4 :

theorem Th65: :: COMPLEX2:65

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

theorem Th66: :: COMPLEX2:66

for a being Element of COMPLEX
for r being Real holds
( Rotate a,r = 0 iff a = 0 )

proof end;

theorem Th67: :: COMPLEX2:67

for a being Element of COMPLEX
for r being Real holds |.(Rotate a,r).| = |.a.|

proof end;

theorem Th68: :: COMPLEX2:68

for a being Element of COMPLEX
for r being Real st a <> 0 holds
ex i being Integer st Arg (Rotate a,r) = ((2 * PI ) * i) + (r + (Arg a))

proof end;

theorem Th69: :: COMPLEX2:69

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

theorem Th70: :: COMPLEX2:70

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

proof end;

theorem Th71: :: COMPLEX2:71

for a, b being Element of COMPLEX
for r being Real holds Rotate (a + b),r = (Rotate a,r) + (Rotate b,r)

proof end;

theorem Th72: :: COMPLEX2:72

for a being Element of COMPLEX
for r being Real holds Rotate (- a),r = - (Rotate a,r)

proof end;

theorem Th73: :: COMPLEX2:73

for a, b being Element of COMPLEX
for r being Real holds Rotate (a - b),r = (Rotate a,r) - (Rotate b,r)

proof end;

theorem Th74: :: COMPLEX2:74

for a being Element of COMPLEX holds Rotate a,PI = - a

proof end;

definition

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

end;

:: deftheorem Def5 defines angle COMPLEX2:def 5 :

theorem Th75: :: COMPLEX2:75

for a being Element of COMPLEX
for r being Real st r >= 0 holds
angle [*r,0*],a = Arg a

proof end;

theorem Th76: :: COMPLEX2:76

for a, b being Element of COMPLEX
for r being Real st Arg a = Arg b & a <> 0 & b <> 0 holds
Arg (Rotate a,r) = Arg (Rotate b,r)

proof end;

theorem Th77: :: COMPLEX2:77

for a, b being Element of COMPLEX
for r being Real st r > 0 holds
angle a,b = angle (a * [*r,0*]),(b * [*r,0*])

proof end;

theorem Th78: :: COMPLEX2:78

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

proof end;

theorem Th79: :: COMPLEX2:79

for a, b being Element of COMPLEX
for r being Real st a <> 0 & b <> 0 holds
angle a,b = angle (Rotate a,r),(Rotate b,r)

proof end;

theorem :: COMPLEX2:80

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

proof end;

theorem :: COMPLEX2:81

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

proof end;

theorem :: COMPLEX2:82

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

proof end;

theorem Th83: :: COMPLEX2:83

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

proof end;

definition

let x, y, z be complex number ;
func angle x,y,z -> real number equals :Def6: :: COMPLEX2:def 6
(Arg (z - y)) - (Arg (x - y)) if (Arg (z - y)) - (Arg (x - y)) >= 0
otherwise (2 * PI ) + ((Arg (z - y)) - (Arg (x - y)));
correctness ;

end;

:: deftheorem Def6 defines angle COMPLEX2:def 6 :

theorem Th84: :: COMPLEX2:84

for x, y, z being Element of COMPLEX holds
( 0 <= angle x,y,z & angle x,y,z < 2 * PI )

proof end;

theorem Th85: :: COMPLEX2:85

for x, y, z being Element of COMPLEX holds angle x,y,z = angle (x - y),0,(z - y)

proof end;

theorem Th86: :: COMPLEX2:86

for a, b, c, d being Element of COMPLEX holds angle a,b,c = angle (a + d),(b + d),(c + d)

proof end;

theorem Th87: :: COMPLEX2:87

for a, b being Element of COMPLEX holds angle a,b = angle a,0,b

proof end;

theorem Th88: :: COMPLEX2:88

for x, y, z being Element of COMPLEX st angle x,y,z = 0 holds
( Arg (x - y) = Arg (z - y) & angle z,y,x = 0 )

proof end;

theorem Th89: :: COMPLEX2:89

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

proof end;

theorem :: COMPLEX2:90

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

proof end;

Lm9: 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 ) )

proof end;

theorem :: COMPLEX2:91

for x, y, z being Element of COMPLEX st x <> y & z <> y & ( angle x,y,z = PI / 2 or angle x,y,z = (3 / 2) * PI ) holds
(|.(x - y).| ^2 ) + (|.(z - y).| ^2 ) = |.(x - z).| ^2

proof end;

theorem Th92: :: COMPLEX2:92

for a, b, c being Element of 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)

proof end;

theorem Th93: :: COMPLEX2:93

for a, b being Element of COMPLEX holds angle a,b,a = 0

proof end;

Lm10: 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)

proof end;

theorem Th94: :: COMPLEX2:94

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

proof end;

theorem :: COMPLEX2:95

for a, b, c being Element of COMPLEX st angle a,b,c <> 0 holds
angle c,b,a <> 0

proof end;

theorem :: COMPLEX2:96

for a, b, c being Element of COMPLEX st angle a,b,c = PI holds
angle c,b,a = PI

proof end;

theorem Th97: :: COMPLEX2:97

for a, b, c being Element of COMPLEX st a <> b & a <> c & b <> c & not angle a,b,c <> 0 & not angle b,c,a <> 0 holds
angle c,a,b <> 0

proof end;

Lm11: 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 )

proof end;

theorem Th98: :: COMPLEX2:98

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 )

proof end;

theorem Th99: :: COMPLEX2:99

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 )

proof end;

Lm12: 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 )

proof end;

theorem Th100: :: COMPLEX2:100

for a, b, c being Element of COMPLEX st a <> b & b <> c & angle a,b,c = PI holds
( angle b,c,a = 0 & angle c,a,b = 0 )

proof end;

theorem Th101: :: COMPLEX2:101

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 )

proof end;

Lm13: for a, b, c being Element of COMPLEX st a <> b & a <> c & b <> c & angle a,b,c = 0 holds
(angle b,c,a) + (angle c,a,b) = PI

proof end;

theorem :: COMPLEX2:102

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 ) )

proof end;