:: Inner Products and Angles of Complex Numbers
:: by Wenpai Chang, Yatsuka Nakamura and Piotr Rudnicki
::
:: Received May 29, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem Th1: :: COMPLEX2:1
for a, b being real number st b > 0 holds
ex r being real number st
( r = (b * (- [\(a / b)/])) + a &amp; 0 <= r &amp; r < b )
proofend;

theorem Th2: :: COMPLEX2:2
for a, b, c being real number st a > 0 &amp; b >= 0 &amp; c >= 0 &amp; b < a &amp; c < a holds
for i being Integer st b = c + (a * i) holds
b = c
proofend;

theorem Th3: :: COMPLEX2:3
for a, b being real number holds
( sin (a - b) = ((sin a) * (cos b)) - ((cos a) * (sin b)) &amp; cos (a - b) = ((cos a) * (cos b)) + ((sin a) * (sin b)) )
proofend;

theorem :: COMPLEX2:4
for a being real number holds
( sin . (a - PI) = - (sin . a) &amp; cos . (a - PI) = - (cos . a) )
proofend;

theorem Th5: :: COMPLEX2:5
for a being real number holds
( sin (a - PI) = - (sin a) &amp; cos (a - PI) = - (cos a) )
proofend;

theorem Th6: :: COMPLEX2:6
for a, b being real number st a in ].0,(PI / 2).[ &amp; b in ].0,(PI / 2).[ holds
( a < b iff sin a < sin b )
proofend;

theorem Th7: :: COMPLEX2:7
for a, b being real number st a in ].(PI / 2),PI.[ &amp; b in ].(PI / 2),PI.[ holds
( a < b iff sin a > sin b )
proofend;

theorem Th8: :: COMPLEX2:8
for a being real number
for i being Integer holds sin a = sin (((2 * PI) * i) + a)
proofend;

theorem Th9: :: COMPLEX2:9
for a being real number
for i being Integer holds cos a = cos (((2 * PI) * i) + a)
proofend;

theorem Th10: :: COMPLEX2:10
for a being real number st sin a = 0 holds
cos a <> 0
proofend;

theorem Th11: :: COMPLEX2:11
for a, b being real number st 0 <= a &amp; a < 2 * PI &amp; 0 <= b &amp; b < 2 * PI &amp; sin a = sin b &amp; cos a = cos b holds
a = b
proofend;

begin

:: ALL these to be changed (mainly deleted) after the change in COMPTRIG
theorem Th12: :: COMPLEX2:12
for z being complex number holds z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i>)
proofend;

Lm1:  Arg 0 = 0
by COMPTRIG:35;

theorem Th13: :: COMPLEX2:13
for z being complex number st z <> 0 holds
( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) &amp; ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) )
proofend;

theorem Th14: :: COMPLEX2:14
for r being Real st r >= 0 holds
Arg r = 0
proofend;

theorem Th15: :: COMPLEX2:15
for z being complex number holds
( Arg z = 0 iff z = |.z.| )
proofend;

theorem Th16: :: COMPLEX2:16
for z being complex number st z <> 0 holds
( Arg z < PI iff Arg (- z) >= PI )
proofend;

theorem Th17: :: COMPLEX2:17
for x, y being complex number st ( x <> y or x - y <> 0 ) holds
( Arg (x - y) < PI iff Arg (y - x) >= PI )
proofend;

theorem Th18: :: COMPLEX2:18
for z being complex number holds
( Arg z in ].0,PI.[ iff Im z > 0 )
proofend;

theorem :: COMPLEX2:19
for z being complex number st Arg z <> 0 holds
( Arg z < PI iff sin (Arg z) > 0 )
proofend;

theorem :: COMPLEX2:20
for x, y being complex number st Arg x < PI &amp; Arg y < PI holds
Arg (x + y) < PI
proofend;

theorem Th21: :: COMPLEX2:21
for z being complex number holds
( Arg z = 0 iff ( Re z >= 0 &amp; Im z = 0 ) )
proofend;

theorem Th22: :: COMPLEX2:22
for z being complex number holds
( Arg z = PI iff ( Re z < 0 &amp; Im z = 0 ) )
proofend;

theorem Th23: :: COMPLEX2:23
for z being complex number holds
( Im z = 0 iff ( Arg z = 0 or Arg z = PI ) )
proofend;

theorem Th24: :: COMPLEX2:24
for z being complex number st Arg z <= PI holds
Im z >= 0
proofend;

theorem Th25: :: COMPLEX2:25
for z being Element of COMPLEX st z <> 0 holds
( cos (Arg (- z)) = - (cos (Arg z)) &amp; sin (Arg (- z)) = - (sin (Arg z)) )
proofend;

theorem Th26: :: COMPLEX2:26
for a being complex number st a <> 0 holds
( cos (Arg a) = (Re a) / |.a.| &amp; sin (Arg a) = (Im a) / |.a.| )
proofend;

theorem Th27: :: COMPLEX2:27
for a being complex number
for r being Real st r > 0 holds
Arg (a * r) = Arg a
proofend;

theorem Th28: :: COMPLEX2:28
for a being complex number
for r being Real st r < 0 holds
Arg (a * r) = Arg (- a)
proofend;

begin

definition
let x, y be complex number ;
funcx .|. y ->  Element of COMPLEX  equals :: COMPLEX2:def 1
x * (y *');
correctness
coherence
x * (y *') is Element of COMPLEX ;
by XCMPLX_0:def_2;
end;

:: deftheorem  defines .|. COMPLEX2:def_1_:_
 for x, y being complex number holds x .|. y = x * (y *');

theorem Th29: :: COMPLEX2:29
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))) * <i>)
proofend;

theorem Th30: :: COMPLEX2:30
for z being Element of COMPLEX holds
( z .|. z = ((Re z) * (Re z)) + ((Im z) * (Im z)) &amp; z .|. z = ((Re z) ^2) + ((Im z) ^2) )
proofend;

theorem Th31: :: COMPLEX2:31
for z being Element of COMPLEX holds
( z .|. z = |.z.| ^2 &amp; |.z.| ^2 = Re (z .|. z) )
proofend;

theorem Th32: :: COMPLEX2:32
for x, y being Element of COMPLEX holds |.(x .|. y).| = |.x.| * |.y.|
proofend;

theorem :: COMPLEX2:33
for x being Element of COMPLEX st x .|. x = 0 holds
x = 0
proofend;

theorem Th34: :: COMPLEX2:34
for y, x being Element of COMPLEX holds y .|. x = (x .|. y) *'
proofend;

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

theorem Th36: :: COMPLEX2:36
for x, y, z being Element of COMPLEX holds x .|. (y + z) = (x .|. y) + (x .|. z)
proofend;

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

theorem Th38: :: COMPLEX2:38
for x, a, y being Element of COMPLEX holds x .|. (a * y) = (a *') * (x .|. y)
proofend;

theorem :: COMPLEX2:39
for a, x, y being Element of COMPLEX holds (a * x) .|. y = x .|. ((a *') * y)
proofend;

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

theorem :: COMPLEX2:41
for x, a, y, b, z being Element of COMPLEX holds x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z))
proofend;

theorem Th42: :: COMPLEX2:42
for x, y being Element of COMPLEX holds (- x) .|. y = x .|. (- y)
proofend;

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

theorem Th44: :: COMPLEX2:44
for x, y being Element of COMPLEX holds - (x .|. y) = x .|. (- y)
proofend;

theorem :: COMPLEX2:45
for x, y being Element of COMPLEX holds (- x) .|. (- y) = x .|. y
proofend;

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

theorem Th47: :: COMPLEX2:47
for x, y, z being Element of COMPLEX holds x .|. (y - z) = (x .|. y) - (x .|. z)
proofend;

theorem :: COMPLEX2:48
for x, y being Element of COMPLEX holds (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)
proofend;

theorem Th49: :: COMPLEX2:49
for x, y being Element of COMPLEX holds (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y)
proofend;

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

theorem Th50: :: COMPLEX2:50
for x, y being Element of COMPLEX holds
( Re (x .|. y) = 0 iff ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) )
proofend;

begin

definition
let a be complex number ;
let r be Real;
func Rotate (a,r) ->  Element of COMPLEX  equals :: COMPLEX2:def 2
(|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>);
correctness
coherence
(|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>) is Element of COMPLEX ;
by XCMPLX_0:def_2;
end;

:: deftheorem  defines Rotate COMPLEX2:def_2_:_
 for a being complex number
for r being Real holds Rotate (a,r) = (|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>);

theorem :: COMPLEX2:51
for a being Element of COMPLEX holds Rotate (a,0) = a by Th12;

theorem Th52: :: COMPLEX2:52
for r being Real
for a being complex number holds
( Rotate (a,r) = 0 iff a = 0 )
proofend;

theorem Th53: :: COMPLEX2:53
for r being Real
for a being complex number holds |.(Rotate (a,r)).| = |.a.|
proofend;

theorem Th54: :: COMPLEX2:54
for r being Real
for a being complex number st a <> 0 holds
ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a))
proofend;

theorem :: COMPLEX2:55
for a being Element of COMPLEX holds Rotate (a,(- (Arg a))) = |.a.| by SIN_COS:31;

theorem Th56: :: COMPLEX2:56
for a being Element of COMPLEX
for r being Real holds
( Re (Rotate (a,r)) = ((Re a) * (cos r)) - ((Im a) * (sin r)) &amp; Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r)) )
proofend;

theorem Th57: :: COMPLEX2:57
for a, b being Element of COMPLEX
for r being Real holds Rotate ((a + b),r) = (Rotate (a,r)) + (Rotate (b,r))
proofend;

theorem Th58: :: COMPLEX2:58
for a being Element of COMPLEX
for r being Real holds Rotate ((- a),r) = - (Rotate (a,r))
proofend;

theorem Th59: :: COMPLEX2:59
for a, b being Element of COMPLEX
for r being Real holds Rotate ((a - b),r) = (Rotate (a,r)) - (Rotate (b,r))
proofend;

theorem Th60: :: COMPLEX2:60
for a being Element of COMPLEX holds Rotate (a,PI) = - a
proofend;

begin

definition
let a, b be complex number ;
func angle (a,b) ->  Real equals :Def3: :: COMPLEX2:def 3
 Arg (Rotate (b,(- (Arg a)))) if ( Arg a = 0 or b <> 0 )
otherwise (2 * PI) - (Arg a);
correctness
coherence
( ( ( Arg a = 0 or b <> 0 ) implies Arg (Rotate (b,(- (Arg a)))) is Real ) &amp; ( Arg a = 0 or b <> 0 or (2 * PI) - (Arg a) is Real ) );
consistency
for b1 being Real holds verum;
;
end;

:: deftheorem Def3 defines angle COMPLEX2:def_3_:_
 for a, b being complex number holds
( ( ( Arg a = 0 or b <> 0 ) implies angle (a,b) = Arg (Rotate (b,(- (Arg a)))) ) &amp; ( Arg a = 0 or b <> 0 or angle (a,b) = (2 * PI) - (Arg a) ) );

theorem Th61: :: COMPLEX2:61
for r being Real
for a being complex number st r >= 0 holds
angle (r,a) = Arg a
proofend;

theorem Th62: :: COMPLEX2:62
for r being Real
for a, b being complex number st Arg a = Arg b &amp; a <> 0 &amp; b <> 0 holds
Arg (Rotate (a,r)) = Arg (Rotate (b,r))
proofend;

theorem Th63: :: COMPLEX2:63
for a, b being Element of COMPLEX
for r being Real st r > 0 holds
angle (a,b) = angle ((a * r),(b * r))
proofend;

theorem Th64: :: COMPLEX2:64
for a, b being Element of COMPLEX st a <> 0 &amp; b <> 0 &amp; Arg a = Arg b holds
Arg (- a) = Arg (- b)
proofend;

theorem Th65: :: COMPLEX2:65
for a, b being Element of COMPLEX
for r being Real st a <> 0 &amp; b <> 0 holds
angle (a,b) = angle ((Rotate (a,r)),(Rotate (b,r)))
proofend;

theorem :: COMPLEX2:66
for a, b being Element of COMPLEX
for r being Real st r < 0 &amp; a <> 0 &amp; b <> 0 holds
angle (a,b) = angle ((a * r),(b * r))
proofend;

theorem :: COMPLEX2:67
for a, b being Element of COMPLEX st a <> 0 &amp; b <> 0 holds
angle (a,b) = angle ((- a),(- b))
proofend;

theorem :: COMPLEX2:68
for b, a being Element of COMPLEX st b <> 0 &amp; angle (a,b) = 0 holds
angle (a,(- b)) = PI
proofend;

theorem Th69: :: COMPLEX2:69
for a, b being Element of COMPLEX st a <> 0 &amp; b <> 0 holds
( cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) &amp; sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) )
proofend;

definition
let x, y, z be complex number ;
func angle (x,y,z) ->  real number  equals :Def4: :: COMPLEX2:def 4
(Arg (z - y)) - (Arg (x - y)) if (Arg (z - y)) - (Arg (x - y)) >= 0
otherwise (2 * PI) + ((Arg (z - y)) - (Arg (x - y)));
correctness
coherence
( ( (Arg (z - y)) - (Arg (x - y)) >= 0 implies (Arg (z - y)) - (Arg (x - y)) is real number ) &amp; ( not (Arg (z - y)) - (Arg (x - y)) >= 0 implies (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) is real number ) );
consistency
for b1 being real number holds verum;
;
end;

:: deftheorem Def4 defines angle COMPLEX2:def_4_:_
 for x, y, z being complex number holds
( ( (Arg (z - y)) - (Arg (x - y)) >= 0 implies angle (x,y,z) = (Arg (z - y)) - (Arg (x - y)) ) &amp; ( not (Arg (z - y)) - (Arg (x - y)) >= 0 implies angle (x,y,z) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) ) );

theorem Th70: :: COMPLEX2:70
for x, y, z being Element of COMPLEX holds
( 0 <= angle (x,y,z) &amp; angle (x,y,z) < 2 * PI )
proofend;

theorem Th71: :: COMPLEX2:71
for x, y, z being Element of COMPLEX holds angle (x,y,z) = angle ((x - y),0,(z - y))
proofend;

theorem Th72: :: COMPLEX2:72
for a, b, c, d being Element of COMPLEX holds angle (a,b,c) = angle ((a + d),(b + d),(c + d))
proofend;

theorem Th73: :: COMPLEX2:73
for a, b being Element of COMPLEX holds angle (a,b) = angle (a,0,b)
proofend;

theorem Th74: :: COMPLEX2:74
for x, y, z being Element of COMPLEX st angle (x,y,z) = 0 holds
( Arg (x - y) = Arg (z - y) &amp; angle (z,y,x) = 0 )
proofend;

theorem Th75: :: COMPLEX2:75
for a, b being Element of COMPLEX st a <> 0 &amp; b <> 0 holds
( Re (a .|. b) = 0 iff ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) )
proofend;

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

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

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

theorem Th78: :: COMPLEX2:78
for a, b, c being Element of COMPLEX
for r being Real st a <> b &amp; b <> c holds
angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))
proofend;

theorem Th79: :: COMPLEX2:79
for a, b being Element of COMPLEX holds angle (a,b,a) = 0
proofend;

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

theorem Th80: :: COMPLEX2:80
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 )
proofend;

theorem :: COMPLEX2:81
for a, b, c being Element of COMPLEX st angle (a,b,c) <> 0 holds
angle (c,b,a) <> 0
proofend;

theorem :: COMPLEX2:82
for a, b, c being Element of COMPLEX st angle (a,b,c) = PI holds
angle (c,b,a) = PI
proofend;

theorem Th83: :: COMPLEX2:83
for a, b, c being Element of COMPLEX st a <> b &amp; a <> c &amp; b <> c &amp; not angle (a,b,c) <> 0 &amp; not angle (b,c,a) <> 0 holds
angle (c,a,b) <> 0
proofend;

Lm5:  for a, b being Element of COMPLEX st Im a = 0 &amp; Re a > 0 &amp; 0 < Arg b &amp; Arg b < PI holds
( ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = PI &amp; 0 < angle (0c,b,a) &amp; 0 < angle (b,a,0c) )
proofend;

theorem Th84: :: COMPLEX2:84
for a, b, c being Element of COMPLEX st a <> b &amp; b <> c &amp; 0 < angle (a,b,c) &amp; angle (a,b,c) < PI holds
( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI &amp; 0 < angle (b,c,a) &amp; 0 < angle (c,a,b) )
proofend;

theorem Th85: :: COMPLEX2:85
for a, b, c being Element of COMPLEX st a <> b &amp; b <> c &amp; angle (a,b,c) > PI holds
( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI &amp; angle (b,c,a) > PI &amp; angle (c,a,b) > PI )
proofend;

Lm6:  for a, b being Element of COMPLEX st Im a = 0 &amp; Re a > 0 &amp; Arg b = PI holds
( ((angle (a,0,b)) + (angle (0,b,a))) + (angle (b,a,0)) = PI &amp; 0 = angle (0,b,a) &amp; 0 = angle (b,a,0) )
proofend;

theorem Th86: :: COMPLEX2:86
for a, b, c being Element of COMPLEX st a <> b &amp; b <> c &amp; angle (a,b,c) = PI holds
( angle (b,c,a) = 0 &amp; angle (c,a,b) = 0 )
proofend;

theorem Th87: :: COMPLEX2:87
for a, b, c being Element of COMPLEX st a <> b &amp; a <> c &amp; b <> c &amp; angle (a,b,c) = 0 &amp; not ( angle (b,c,a) = 0 &amp; angle (c,a,b) = PI ) holds
( angle (b,c,a) = PI &amp; angle (c,a,b) = 0 )
proofend;

theorem :: COMPLEX2:88
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 &amp; a <> c &amp; b <> c ) )
proofend;