Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

Inner Products and Angles of Complex Numbers

by
Wenpai Chang,
Yatsuka Nakamura, and
Piotr Rudnicki

MML identifier: COMPLEX2
[ Mizar article, MML identifier index ]

```environ

vocabulary RLVECT_1, COMPLEX1, ARYTM_1, SQUARE_1, COMPLFLD, ARYTM, HAHNBAN1,
FUNCT_1, RCOMP_1, SIN_COS, ARYTM_3, RELAT_1, COMPTRIG, COMPLEX2, PROB_2,
XCMPLX_0, BOOLE, FINSEQ_6, INT_1, ABSVALUE;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, SQUARE_1, NAT_1, RLVECT_1,
RELAT_1, SEQ_1, RCOMP_1, SIN_COS, HAHNBAN1, COMPTRIG, XREAL_0, ORDINAL1,
NUMBERS, ARYTM_0, INT_1, XCMPLX_0, REAL_1, COMPLEX1, COMPLFLD, ABSVALUE;
constructors REAL_1, SQUARE_1, SEQ_1, RFUNCT_2, COMSEQ_3, GROUP_1, RCOMP_1,
COMPLSP1, SIN_COS, HAHNBAN1, COMPTRIG, COMPLEX1, MEMBERED, ARYTM_0,
ARYTM_3, FUNCT_4;
clusters RELSET_1, SIN_COS, INT_1, COMPLEX1, XREAL_0, XCMPLX_0, MEMBERED,
NUMBERS;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;

begin

theorem :: COMPLEX2:1
for a, b being Real holds -[*a,b*] = [*-a,-b*];

theorem :: COMPLEX2:2
for a, b being real number st b > 0
ex r being real number st r = b*-[\ a/b /]+a & 0 <= r & r < b;

theorem :: COMPLEX2:3
for a, b, c being real number st a > 0 & b >= 0 & c >= 0 & b < a & c < a
for i being Integer st b = c + a*i holds b = c;

theorem :: COMPLEX2:4
for a, b being Real holds sin(a-b) = sin(a)*cos(b)-cos(a)*sin(b) &
cos(a-b) = cos(a)*cos(b)+sin(a)*sin(b);

theorem :: COMPLEX2:5
for a being Real holds sin.(a-PI) = -sin.a & cos.(a-PI) = -cos.a;

theorem :: COMPLEX2:6
for a being Real holds sin(a-PI) = -sin a & cos(a-PI) = -cos a;

theorem :: 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;

theorem :: 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;

theorem :: COMPLEX2:9
for a being Real, i being Integer holds sin a = sin (2*PI*i+a);

theorem :: COMPLEX2:10
for a being Real, i being Integer holds cos a = cos (2*PI*i+a);

theorem :: COMPLEX2:11
for a being Real st sin a = 0 holds cos a <> 0;

theorem :: COMPLEX2:12
for a, b being Real
st 0 <= a & a < 2*PI & 0 <= b & b < 2*PI & sin a = sin b & cos a = cos b
holds a = b;

begin :: More on the argument of a complex number
:: ALL these to be changed (mainly deleted) after the change in COMPTRIG

definition
cluster F_Complex -> non empty;
end;

definition let z be Element of COMPLEX;
func F_tize(z) -> Element of F_Complex equals
:: COMPLEX2:def 1
z;
end;

theorem :: COMPLEX2:13
for z being Element of COMPLEX holds Re z = Re F_tize z & Im z = Im F_tize z;

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 = 0c iff F_tize z = 0.F_Complex;

theorem :: COMPLEX2:16
for z being Element of COMPLEX holds |.z.| = |. F_tize z .|;

definition let z be Element of COMPLEX;
func Arg(z) -> Real equals
:: COMPLEX2:def 2
Arg(F_tize(z));
end;

theorem :: COMPLEX2:17
for z being Element of COMPLEX, u being Element of F_Complex
st z = u holds Arg z = Arg u;

theorem :: COMPLEX2:18
for z being Element of COMPLEX holds 0 <= Arg z & Arg z < 2*PI;

theorem :: COMPLEX2:19
for z being Element of COMPLEX holds z = [* |.z.|*cos Arg z, |.z.|*sin Arg z *]
;

theorem :: COMPLEX2:20
Arg 0c = 0;

theorem :: COMPLEX2:21
for z being Element of COMPLEX, r being Real
st z <> 0 & z = [* |.z.|*cos r, |.z.|*sin r *] & 0 <= r & r < 2*PI
holds r = Arg z;

theorem :: COMPLEX2:22
for z being Element of COMPLEX st z <> 0c
holds (Arg z < PI implies Arg -z = Arg z +PI) &
(Arg z >= PI implies Arg -z = Arg z -PI);

theorem :: COMPLEX2:23
for r being Real st r >= 0 holds Arg [*r,0*] = 0;

theorem :: COMPLEX2:24
for z being Element of COMPLEX holds Arg z = 0 iff z = [* |.z.|,0 *];

theorem :: COMPLEX2:25
for z being Element of COMPLEX st z <> 0c holds Arg(z) < PI iff Arg -z >= PI;

theorem :: COMPLEX2:26
for x, y being Element of COMPLEX st x <> y or x-y <> 0c
holds Arg(x-y) < PI iff Arg(y-x) >= PI;

theorem :: COMPLEX2:27
for z being Element of COMPLEX holds Arg z in ].0,PI.[ iff Im z > 0;

theorem :: COMPLEX2:28
for z being Element of COMPLEX st Arg z <> 0 holds Arg z < PI iff sin Arg z >
0;

theorem :: COMPLEX2:29
for x, y being Element of COMPLEX st Arg x < PI & Arg y < PI
holds Arg(x+y) < PI;

theorem :: COMPLEX2:30
for x be Real st x > 0 holds Arg [*0,x*] = PI/2;

theorem :: COMPLEX2:31
for z be Element of COMPLEX holds Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0;

theorem :: COMPLEX2:32
for z be Element of COMPLEX holds Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0;

theorem :: COMPLEX2:33
for z be Element of COMPLEX st Im z > 0 holds sin Arg z > 0;

theorem :: COMPLEX2:34
for z being Element of COMPLEX holds Arg z = 0 iff Re z >= 0 & Im z = 0;

theorem :: COMPLEX2:35
for z being Element of COMPLEX holds Arg z = PI iff Re z < 0 & Im z=0;

theorem :: COMPLEX2:36
for z being Element of COMPLEX holds Im z = 0 iff Arg z = 0 or Arg z = PI;

theorem :: COMPLEX2:37
for z being Element of COMPLEX st Arg z <= PI holds Im z >= 0;

theorem :: COMPLEX2:38
for z being Element of COMPLEX st z <> 0
holds cos Arg -z = -cos Arg z & sin Arg -z = - sin Arg z;

theorem :: COMPLEX2:39
for a being Element of COMPLEX st a <> 0
holds cos Arg a = Re a / |.a.| & sin Arg a = Im a / |.a.|;

theorem :: COMPLEX2:40
for a being Element of COMPLEX, r being Real st r > 0
holds Arg(a*[*r,0*]) = Arg a;

theorem :: COMPLEX2:41
for a being Element of COMPLEX, r being Real st r < 0
holds Arg(a*[*r,0*]) = Arg -a;

begin :: Inner product

definition ::Inner product of complex numbers
let x, y be Element of COMPLEX;
func x .|. y -> Element of COMPLEX equals
:: COMPLEX2:def 3
x*(y*');
end;

reserve a, b, c, d, x, y, z for Element of COMPLEX;

theorem :: COMPLEX2:42
x.|.y = [* (Re x)*(Re y)+(Im x)*(Im y), -(Re x)*(Im y)+(Im x)*(Re y) *];

theorem :: COMPLEX2:43
z.|.z = [* (Re z)*(Re z)+(Im z)*(Im z),0*] & z.|.z = [* (Re z)^2+(Im z)^2,0*];

theorem :: COMPLEX2:44
z.|.z = [* |.z.|^2,0*] & |.z.|^2 = Re (z.|.z);

theorem :: COMPLEX2:45
|. x.|.y .| = |.x.|*|.y.|;

theorem :: COMPLEX2:46
x.|.x = 0 implies x = 0;

theorem :: COMPLEX2:47
y.|.x = (x.|.y)*';

theorem :: COMPLEX2:48
(x+y).|.z = x.|.z + y.|.z;

theorem :: COMPLEX2:49
x.|.(y+z) = x.|.y + x.|.z;

theorem :: COMPLEX2:50
(a*x).|.y = a * x.|.y;

theorem :: COMPLEX2:51
x.|.(a*y) = (a*') * x.|.y;

theorem :: COMPLEX2:52
(a*x).|.y = x.|.((a*')*y);

theorem :: COMPLEX2:53
(a*x+b*y).|.z = a * x.|.z + b * y.|.z;

theorem :: COMPLEX2:54
x.|.(a*y + b*z) = (a*') * x.|.y + (b*') * x.|.z;

theorem :: COMPLEX2:55
(-x).|.y = x.|.(-y);

theorem :: COMPLEX2:56
(-x).|.y = - x.|.y;

theorem :: COMPLEX2:57
- x.|.y = x.|.(-y);

theorem :: COMPLEX2:58
(-x).|.(-y) = x.|.y;

theorem :: COMPLEX2:59
(x - y).|.z = x.|.z - y.|.z;

theorem :: COMPLEX2:60
x.|.(y - z) = x.|.y - x.|.z;

theorem :: COMPLEX2:61
0c.|.x = 0c & x.|.0c = 0c;

theorem :: COMPLEX2:62
(x + y).|.(x + y) = x.|.x + x.|.y + y.|.x + y.|.y;

theorem :: COMPLEX2:63
(x-y).|.(x-y) = x.|.x - x.|.y - y.|.x + y.|.y;

theorem :: COMPLEX2:64
Re (x.|.y) = 0 iff Im (x.|.y) = |.x.|*|.y.| or Im (x.|.y) = -|.x.|*|.y.|;

begin :: Rotation

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

reserve r for Real;

theorem :: COMPLEX2:65
Rotate(a, 0) = a;

theorem :: COMPLEX2:66
Rotate(a, r) = 0c iff a = 0c;

theorem :: COMPLEX2:67
|.Rotate(a,r).| = |.a.|;

theorem :: COMPLEX2:68
a <> 0c implies ex i being Integer st Arg(Rotate(a,r)) = 2*PI*i+(r+Arg(a));

theorem :: COMPLEX2:69
Rotate(a,-Arg a) = [* |.a.|, 0 *];

theorem :: COMPLEX2:70
Re Rotate(a,r) = (Re a)*(cos r)-(Im a)*(sin r) &
Im Rotate(a,r) = (Re a)*(sin r)+(Im a)*(cos r);

theorem :: COMPLEX2:71
Rotate(a+b,r) = Rotate(a,r)+Rotate(b,r);

theorem :: COMPLEX2:72
Rotate(-a,r) = -Rotate(a,r);

theorem :: COMPLEX2:73
Rotate(a-b,r) = Rotate(a,r)-Rotate(b,r);

theorem :: COMPLEX2:74
Rotate(a, PI) = -a;

begin :: Angles

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

theorem :: COMPLEX2:75
r >= 0 implies angle([*r,0*],a) = Arg a;

theorem :: COMPLEX2:76
Arg a = Arg b & a <> 0 & b <> 0 implies Arg Rotate(a,r) = Arg Rotate(b,r);

theorem :: COMPLEX2:77
r > 0 implies angle(a,b) = angle(a*[*r,0*],b*[*r,0*]);

theorem :: COMPLEX2:78
a <> 0 & b <> 0 & Arg a = Arg b implies Arg -a = Arg -b;

theorem :: COMPLEX2:79
a <> 0 & b <> 0 implies angle(a,b) = angle(Rotate(a,r),Rotate(b,r));

theorem :: COMPLEX2:80
r < 0 & a <> 0 & b <> 0 implies angle(a,b) = angle(a*[*r,0*],b*[*r,0*]);

theorem :: COMPLEX2:81
a <> 0 & b <> 0 implies angle(a,b) = angle(-a,-b);

theorem :: COMPLEX2:82
b <> 0 & angle(a,b) = 0 implies angle(a,-b) = PI;

theorem :: COMPLEX2:83
a <> 0 & b <> 0 implies cos angle(a,b) = Re (a.|.b)/(|.a.|*|.b.|) &
sin angle(a,b) = - Im (a.|.b)/(|.a.|*|.b.|);

definition let x, y, z be Element of COMPLEX;
func angle(x,y,z) -> real number equals
:: 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));
end;

theorem :: COMPLEX2:84
0 <= angle(x,y,z) & angle(x,y,z) < 2*PI;

theorem :: COMPLEX2:85
angle(x,y,z)=angle(x-y,0c,z-y);

theorem :: COMPLEX2:86
angle(a,b,c) = angle(a+d,b+d,c+d);

theorem :: COMPLEX2:87
angle(a,b) = angle(a,0c,b);

theorem :: COMPLEX2:88
angle(x,y,z) = 0 implies Arg(x-y) = Arg(z-y) & angle(z,y,x)=0;

theorem :: COMPLEX2:89
a <> 0c & b <> 0c implies (Re (a.|.b) = 0
iff angle(a,0c,b) = PI/2 or angle(a,0c,b) = 3/2*PI);

theorem :: COMPLEX2:90
a <> 0c & b <> 0c implies (Im(a.|.b) = |.a.|*|.b.| or Im(a.|.b) = -|.a.|*|.b.|
iff angle(a,0c,b) = PI/2 or angle(a,0c,b) = 3/2*PI);

theorem :: COMPLEX2:91
x <> y & z <> y & (angle(x,y,z) = PI/2 or angle(x,y,z) = 3/2*PI)
implies |.x-y.|^2+|.z-y.|^2 = |.x-z.|^2;

theorem :: COMPLEX2:92
a <> b & b <> c implies
angle(a,b,c) = angle(Rotate(a,r), Rotate(b,r), Rotate(c,r));

theorem :: COMPLEX2:93
angle(a,b,a) = 0;

theorem :: COMPLEX2:94  :: COMPLEX2:47, 48
angle(a,b,c) <> 0 iff angle(a,b,c)+angle(c,b,a) = 2*PI;

theorem :: COMPLEX2:95
angle(a,b,c) <> 0 implies angle(c,b,a) <> 0;

theorem :: COMPLEX2:96
angle(a,b,c) = PI implies angle(c,b,a) = PI;

theorem :: COMPLEX2:97
a <> b & a <> c & b <> c
implies angle(a,b,c) <> 0 or angle(b,c,a) <> 0 or angle(c,a,b) <> 0;

theorem :: COMPLEX2:98
a <> b & b <> c & 0 < angle(a,b,c) & angle(a,b,c) < PI
implies angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI &
0 < angle(b,c,a) & 0 < angle(c,a,b);

theorem :: COMPLEX2:99
a <> b & b <> c & angle(a,b,c) > PI
implies angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = 5*PI &
angle(b,c,a) > PI & angle(c,a,b) > PI;

theorem :: COMPLEX2:100
a <> b & b <> c & angle(a,b,c) = PI implies angle(b,c,a) = 0 & angle(c,a,b) = 0
;

theorem :: COMPLEX2:101
a <> b & a <> c & b <> c & angle(a,b,c) = 0
implies angle(b,c,a) = 0 & angle(c,a,b) = PI or
angle(b,c,a) = PI & angle(c,a,b) = 0;

theorem :: COMPLEX2:102
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;

```