Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Wenpai Chang,
- Yatsuka Nakamura,
and
- Piotr Rudnicki
- Received May 29, 2003
- 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;
Back to top