:: Inner Products and Angles of Complex Numbers
:: by Wenpai Chang, Yatsuka Nakamura and Piotr Rudnicki
::
:: Received May 29, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XXREAL_0, CARD_1, RELAT_1, ARYTM_1, INT_1, ARYTM_3,
SIN_COS, FUNCT_1, XXREAL_1, XBOOLE_0, SUBSET_1, REAL_1, XCMPLX_0,
COMPLEX1, COMPTRIG, TARSKI, PROB_2, SQUARE_1, FINSEQ_6, COMPLEX2;
notations TARSKI, SUBSET_1, SQUARE_1, RELAT_1, FUNCT_1, RCOMP_1, SIN_COS,
XXREAL_0, COMPTRIG, XREAL_0, ORDINAL1, NUMBERS, INT_1, XCMPLX_0, REAL_1,
COMPLEX1;
constructors FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, BINOP_2, RCOMP_1, RFUNCT_2,
COMSEQ_3, SIN_COS, COMPTRIG, PARTFUN1, RVSUM_1, RELSET_1, NUMBERS;
registrations RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, SIN_COS, VALUED_0,
ORDINAL1, SQUARE_1;
requirements SUBSET, REAL, NUMERALS, ARITHM;
equalities SQUARE_1, XCMPLX_0;
theorems SQUARE_1, COMPLEX1, SIN_COS, COMPTRIG, XCMPLX_0, XCMPLX_1, RFUNCT_2,
SIN_COS2, XREAL_0, XBOOLE_0, INT_1, ABSVALUE, XREAL_1, XXREAL_0,
XXREAL_1;
begin
theorem Th1:
for a, b being Real st b > 0 ex r being Real st r =
b*-[\ a/b /]+a & 0 <= r & r < b
proof
let a, b be Real such that
A1: b > 0;
set ab = [\ a/b /];
set i = -ab;
take r = b*i+a;
thus r = b*i+a;
ab <= a/b by INT_1:def 6;
then ab*b <= a/b*b by A1,XREAL_1:64;
then ab*b <= a by A1,XCMPLX_1:87;
then -(ab*b) >= -a by XREAL_1:24;
then b*i+a >= a+-a by XREAL_1:6;
hence 0 <= r;
a/b-1 < ab by INT_1:def 6;
then -(a/b-1) > i by XREAL_1:24;
then (-(a/b)+1)*b > i*b by A1,XREAL_1:68;
then -(a/b*b)+b > i*b;
then -a+b > i*b by A1,XCMPLX_1:87;
then -a+b+a > r by XREAL_1:8;
hence thesis;
end;
theorem Th2:
for a, b, c being Real st a > 0 & b >= 0 & c >= 0 & b < a
& c < a for i being Integer st b = c + a*i holds b = c
proof
let a, b, c be Real such that
A1: a > 0 and
A2: b >= 0 and
A3: c >= 0 and
A4: b < a and
A5: c < a;
A6: 0+a <= c+a by A3,XREAL_1:7;
let i be Integer such that
A7: b = c + a*i;
per cases;
suppose
i < 0;
then i <= -1 by INT_1:8;
then a*i <= a*(-1) by A1,XREAL_1:64;
then c+a*i <= c-a by XREAL_1:7;
hence thesis by A2,A5,A7,XREAL_1:49;
end;
suppose
i = 0;
hence thesis by A7;
end;
suppose
i > 0;
then 0+1 <= i by INT_1:7;
then a*i >= a by A1,XREAL_1:151;
then c+a*i >= c+a by XREAL_1:7;
hence thesis by A4,A7,A6,XXREAL_0:2;
end;
end;
theorem Th3:
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)
proof
let th1, th2 be Real;
thus sin(th1-th2)=sin.(th1+(-th2)) by SIN_COS:def 17
.=(sin.(th1)) *(cos.(-th2))+(cos.(th1)) * (sin.(-th2)) by SIN_COS:74
.=(sin.(th1)) *(cos.(th2))+(cos.(th1)) * (sin.(-th2)) by SIN_COS:30
.=(sin.(th1)) *(cos.(th2))+(cos.(th1)) * -(sin.(th2)) by SIN_COS:30
.=(sin(th1)) *(cos.(th2))-(cos.(th1)) * (sin.(th2)) by SIN_COS:def 17
.=(sin(th1)) *(cos(th2))-(cos.(th1)) * (sin.(th2)) by SIN_COS:def 19
.=(sin(th1)) *(cos(th2))-(cos(th1)) * (sin.(th2)) by SIN_COS:def 19
.=(sin(th1)) *(cos(th2))-(cos(th1)) * (sin(th2)) by SIN_COS:def 17;
thus cos(th1-th2)=cos.(th1+(-th2)) by SIN_COS:def 19
.=(cos.(th1)) *(cos.(-th2))-(sin.(th1)) * (sin.(-th2)) by SIN_COS:74
.=(cos.(th1)) *(cos.(th2))-(sin.(th1)) * (sin.(-th2)) by SIN_COS:30
.=(cos.(th1)) *(cos.(th2))-(sin.(th1)) * -(sin.(th2)) by SIN_COS:30
.=(cos(th1)) *(cos.(th2))+(sin.(th1)) * (sin.(th2)) by SIN_COS:def 19
.=(cos(th1)) *(cos(th2))+(sin.(th1)) * (sin.(th2)) by SIN_COS:def 19
.=(cos(th1)) *(cos(th2))+(sin(th1)) * (sin.(th2)) by SIN_COS:def 17
.=(cos(th1)) *(cos(th2))+(sin(th1)) * (sin(th2)) by SIN_COS:def 17;
end;
theorem
for a being Real holds sin.(a-PI) = -sin.a & cos.(a-PI) = -cos. a
proof
let th be Real;
thus sin.(th- PI) = (sin.(th))* (cos.(-PI)) + (cos.(th)) *( sin.(-PI)) by
SIN_COS:74
.= (sin.(th))* (cos.(PI)) + (cos.(th)) *(sin.(-PI)) by SIN_COS:30
.= (sin.(th))* (cos.(PI)) + (cos.(th)) *(-(sin.(PI))) by SIN_COS:30
.= -sin.th by SIN_COS:76;
thus cos.(th- PI) = (cos.(th)) * (cos.(-PI)) - ( sin.(th)) *( sin.(-PI)) by
SIN_COS:74
.= (cos.(th)) * (cos.(PI)) - ( sin.(th)) *( sin.(-PI)) by SIN_COS:30
.= (cos.(th)) * (cos.(PI)) - ( sin.(th)) *(-(sin.(PI))) by SIN_COS:30
.= -cos.th by SIN_COS:76;
end;
theorem Th5:
for a being Real holds sin(a-PI) = -sin a & cos(a-PI) = - cos a
proof
let r be Real;
thus sin (r-PI) = sin(r)*cos(PI)-cos(r)*sin(PI) by Th3
.= -sin r by SIN_COS:77;
thus cos (r-PI) = cos(r)*cos(PI)+sin(r)*sin(PI) by Th3
.= -cos r by SIN_COS:77;
end;
theorem Th6:
for a, b being Real st a in ].0,PI/2.[ & b in ].0,PI/2.[
holds a < b iff sin a < sin b
proof
let a, b be Real;
assume a in ].0,PI/2.[ & b in ].0,PI/2.[;
then
A1: a in ].0,PI/2.[ /\ dom sin & b in ].0,PI/2.[ /\ dom sin by SIN_COS:24
,XBOOLE_0:def 4;
A2: sin a = sin.a & sin b = sin.b by SIN_COS:def 17;
hence a < b implies sin a < sin b by A1,RFUNCT_2:20,SIN_COS2:2;
assume
A3: sin a < sin b;
assume a >= b;
then a > b by A3,XXREAL_0:1;
hence contradiction by A2,A1,A3,RFUNCT_2:20,SIN_COS2:2;
end;
theorem Th7:
for a, b being Real st a in ].PI/2,PI.[ & b in ].PI/2,PI.[
holds a < b iff sin a > sin b
proof
let a, b be Real;
assume a in ].PI/2,PI.[ & b in ].PI/2,PI.[;
then
A1: a in ].PI/2,PI.[ /\ dom sin & b in ].PI/2,PI.[ /\ dom sin by SIN_COS:24
,XBOOLE_0:def 4;
A2: sin a = sin.a & sin b = sin.b by SIN_COS:def 17;
hence a < b implies sin a > sin b by A1,RFUNCT_2:21,SIN_COS2:3;
assume
A3: sin a > sin b;
assume a >= b;
then a > b by A3,XXREAL_0:1;
hence contradiction by A2,A1,A3,RFUNCT_2:21,SIN_COS2:3;
end;
theorem Th8:
for a being Real, i being Integer holds sin a = sin (2*PI* i+a)
proof
let r being Real, i being Integer;
A1: sin.r = sin r by SIN_COS:def 17;
A2: sin.(2*PI*i+r) = sin (2*PI*i+r) by SIN_COS:def 17;
A3: sin.(2*PI*(-i)+(2*PI*i+r)) = sin (2*PI*(-i)+(2*PI*i+r)) by SIN_COS:def 17;
per cases;
suppose
i >= 0;
then reconsider iN = i as Element of NAT by INT_1:3;
sin r = sin (2*PI*iN+r) by A1,A2,SIN_COS2:10;
hence thesis;
end;
suppose
i < 0;
then reconsider iN = -i as Element of NAT by INT_1:3;
set aa = 2*PI*i+r;
sin (aa) = sin (2*PI*iN+aa) by A2,A3,SIN_COS2:10;
hence thesis;
end;
end;
theorem Th9:
for a being Real, i being Integer holds cos a = cos (2*PI *i+a)
proof
let r be Real, i being Integer;
A1: cos.r = cos r by SIN_COS:def 19;
A2: cos.(2*PI*i+r) = cos (2*PI*i+r) by SIN_COS:def 19;
A3: cos.(2*PI*(-i)+(2*PI*i+r)) = cos (2*PI*(-i)+(2*PI*i+r)) by SIN_COS:def 19;
per cases;
suppose
i >= 0;
then reconsider iN = i as Element of NAT by INT_1:3;
cos r = cos (2*PI*iN+r) by A1,A2,SIN_COS2:11;
hence thesis;
end;
suppose
i < 0;
then reconsider iN = -i as Element of NAT by INT_1:3;
set aa = 2*PI*i+r;
cos (aa) = cos (2*PI*iN+aa) by A2,A3,SIN_COS2:11;
hence thesis;
end;
end;
theorem Th10:
for a being Real st sin a = 0 holds cos a <> 0
proof
let a be Real;
assume that
A1: sin a = 0 and
A2: cos a = 0;
consider r being Real such that
A3: r = 2*PI*-[\ a/(2*PI) /]+a and
A4: 0 <= r & r < 2*PI by Th1,COMPTRIG:5;
A5: cos a = cos r by A3,Th9;
sin a = sin r by A3,Th8;
then r = 0 or r = PI by A4,A1,COMPTRIG:17;
hence thesis by A5,A2,COMPTRIG:5,18;
end;
theorem Th11:
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
proof
let r, s be Real such that
A1: 0 <= r and
A2: r < 2*PI & 0 <= s and
A3: s < 2*PI and
A4: sin r = sin s & cos r = cos s;
A5: cos(r-s)=(cos r)*(cos s)+(sin r)*(sin s) by Th3
.= 1 by A4,SIN_COS:29;
A6: sin(r-s)=(sin r)*(cos s)-(cos r)*(sin s) by Th3
.= 0 by A4;
A7: cos (s-r)=(cos r)*(cos s)+(sin r)*(sin s) by Th3
.= 1 by A4,SIN_COS:29;
A8: sin (s-r)=(sin s)*(cos r)-(cos s)*(sin r) by Th3
.= 0 by A4;
per cases by XXREAL_0:1;
suppose
A9: r > s;
r+0 < 2*PI+s by A2,XREAL_1:8;
then
A10: r-s < 2*PI by XREAL_1:19;
r > s+0 by A9;
then 0 <= r-s by XREAL_1:20;
then r-s = 0 or r-s = PI by A6,A10,COMPTRIG:17;
hence thesis by A5,SIN_COS:77;
end;
suppose
r < s;
then s > r+0;
then
A11: 0 <= s-r by XREAL_1:20;
s+0 < 2*PI+r by A1,A3,XREAL_1:8;
then s-r < 2*PI by XREAL_1:19;
then s-r = 0 or s-r = PI by A8,A11,COMPTRIG:17;
hence thesis by A7,SIN_COS:77;
end;
suppose
r = s;
hence thesis;
end;
end;
begin :: More on the argument of a complex number
:: ALL these to be changed (mainly deleted) after the change in COMPTRIG
Lm1: Arg 0 = 0 by COMPTRIG:35;
::$CT
theorem Th12:
for z being Complex st z <> 0 holds (Arg z < PI implies
Arg -z = Arg z +PI) & (Arg z >= PI implies Arg -z = Arg z -PI)
proof
let z be Complex;
assume
A1: z <> 0;
then
A2: |.z.| <> 0 by COMPLEX1:45;
z = |.z.|*cos Arg z + (|.z.|*sin Arg z)*<i> by COMPTRIG:62;
then
A3: -z= -|.z.|*cos Arg z +(-|.z.|*sin Arg z)*<i>;
Arg z < 2*PI by COMPTRIG:34;
then Arg z +0 < 2*PI+PI by COMPTRIG:5,XREAL_1:8;
then
A4: Arg z -PI < 2*PI by XREAL_1:19;
A5: -z = |.-z.|*cos Arg -z + |.-z.|*(sin Arg -z)*<i> by COMPTRIG:62;
A6: |.z.| = |.-z.| by COMPLEX1:52;
then |.z.|*sin Arg -z = |.z.|*-sin Arg z by A5,A3,COMPLEX1:77;
then
A7: sin Arg -z = -sin Arg z by A2,XCMPLX_1:5;
then
A8: sin Arg -z = sin (Arg z +PI) by SIN_COS:79;
|.z.|*cos Arg -z = |.z.|*-cos Arg z by A5,A3,A6,COMPLEX1:77;
then
A9: cos Arg -z = -cos Arg z by A2,XCMPLX_1:5;
then
A10: cos Arg -z = cos (Arg z +PI) by SIN_COS:79;
hereby
assume Arg z<PI;
then
A11: Arg z+PI<PI+PI by XREAL_1:8;
0 <= Arg z by COMPTRIG:34;
hence Arg -z = Arg z +PI by A1,A5,A10,A8,A11,COMPTRIG:5,def 1;
end;
assume Arg z >= PI;
then
A12: Arg z -PI >= PI-PI by XREAL_1:9;
A13: sin Arg -z = sin (Arg z -PI) by A7,Th5;
cos Arg -z = cos (Arg z -PI) by A9,Th5;
hence thesis by A1,A5,A13,A12,A4,COMPTRIG:def 1;
end;
::$CT
theorem Th13:
for z being Complex holds Arg z = 0 iff z = |.z.|
proof
let z be Complex;
hereby
assume Arg z=0;
then z= |.z.|*cos 0 + |.z.|*sin 0 *<i> by COMPTRIG:62;
hence z= |.z.| by SIN_COS:31;
end;
assume z= |.z.|;
hence thesis by COMPTRIG:35,COMPLEX1:46;
end;
theorem Th14:
for z being Complex st z <> 0 holds Arg(z) < PI iff Arg - z >= PI
proof
let z be Complex;
assume
A1: z<>0;
thus Arg(z)<PI implies Arg(-z)>=PI
proof
Arg(z)>=0 by COMPTRIG:34;
then
A2: PI+0<=PI+Arg(z) by XREAL_1:7;
assume Arg(z)<PI;
hence thesis by A1,A2,Th12;
end;
thus Arg(-z)>=PI implies Arg(z)<PI
proof
2*PI>Arg(-z) by COMPTRIG:34;
then
A3: PI+PI-PI>Arg(-z)-PI by XREAL_1:9;
assume Arg(-z)>=PI;
then Arg(--z)=Arg(-z)-PI by A1,Th12;
hence thesis by A3;
end;
end;
theorem Th15:
for x, y being Complex st x <> y or x - y <> 0 holds Arg(
x-y) < PI iff Arg(y-x) >= PI
proof
let z1,z2 be Complex;
assume z1<>z2 or z1 - z2 <> 0;
then z1-z2<>0c;
then Arg(z1-z2)<PI iff Arg(-(z1-z2))>=PI by Th14;
hence thesis;
end;
theorem Th16:
for z being Complex holds Arg z in ].0,PI.[ iff Im z > 0
proof
let z be Complex;
thus Arg z in ].0,PI.[ implies Im z > 0
proof
assume Arg z in ].0,PI.[;
then
A1: 0<Arg(z) & Arg(z)<PI by XXREAL_1:4;
A2: Arg(z)<PI/2 or Arg(z)=PI/2 or Arg(z)>PI/2 by XXREAL_0:1;
now
per cases by A1,A2,XXREAL_1:4;
case
Arg(z) in ].0,PI/2.[;
hence thesis by COMPTRIG:41;
end;
case
Arg(z)=PI/2;
hence thesis by COMPTRIG:48,SIN_COS:77;
end;
case
Arg(z) in ].PI/2,PI.[;
hence thesis by COMPTRIG:42;
end;
end;
hence thesis;
end;
A3: ].PI/2,PI.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
A4: ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
thus Im z > 0 implies Arg z in ].0,PI.[
proof
assume
A5: Im z >0;
now
per cases;
case
Re z>0;
then Arg(z) in ].0,PI/2.[ by A5,COMPTRIG:41;
hence thesis by A4;
end;
case
Re z=0;
then z= 0 + (Im z)*<i> by COMPLEX1:13;
then Arg(z)=PI/2 by A5,COMPTRIG:37;
hence thesis by COMPTRIG:5,XXREAL_1:4;
end;
case
Re z<0;
then Arg z in ].PI/2,PI.[ by A5,COMPTRIG:42;
hence thesis by A3;
end;
end;
hence thesis;
end;
end;
theorem
for z being Complex st Arg z <> 0 holds Arg z < PI iff sin Arg z> 0
proof
let z be Complex;
A1: Arg(z)>=0 by COMPTRIG:34;
assume
A2: Arg(z)<>0;
hereby
assume Arg(z)<PI;
then Arg(z) in ].0,PI.[ by A2,A1,XXREAL_1:4;
then Im (z)>0 by Th16;
hence sin (Arg(z))>0 by COMPTRIG:45;
end;
A3: ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
thus sin (Arg(z))>0 implies Arg(z)<PI
proof
assume
A4: sin (Arg(z))>0;
then
A5: Im (z)>0 by COMPTRIG:48;
now
per cases;
suppose
Re z>0;
then Arg(z) in ].0,PI/2.[ by A5,COMPTRIG:41;
hence thesis by A3,XXREAL_1:4;
end;
suppose
Re z=0;
then z= 0 + (Im z)*<i> by COMPLEX1:13;
hence thesis by A4,COMPTRIG:5,37,48;
end;
suppose
Re z<0;
then Arg(z) in ].PI/2,PI.[ by A5,COMPTRIG:42;
hence thesis by XXREAL_1:4;
end;
end;
hence thesis;
end;
end;
theorem
for x, y being Complex st Arg x < PI & Arg y < PI holds Arg(x+y ) < PI
proof
let z1,z2 be Complex;
assume that
A1: Arg(z1)<PI and
A2: Arg(z2)<PI;
A3: |.z2.| = |.z2.|+0*<i>;
A4: |.z1.| = |.z1.|+0*<i>;
per cases by COMPTRIG:34;
suppose
A5: Arg(z1)=0;
then z1= |.z1.| by Th13;
then
A6: Im z1=0 by A4,COMPLEX1:12;
per cases by COMPTRIG:34;
suppose
Arg(z2)=0;
then z2= |.z2.| by Th13;
then
A7: z1+z2= |.z1.| + |.z2.| + 0*<i> by A5,Th13;
0<= |.z1.| & 0<= |.z2.| by COMPLEX1:46;
hence thesis by A7,COMPTRIG:5,35;
end;
suppose
Arg(z2)>0;
then Arg(z2) in ].0,PI.[ by A2,XXREAL_1:4;
then
A8: Im z2>0 by Th16;
Im (z1+z2)=(Im z1)+(Im z2) by COMPLEX1:8;
then Arg(z1+z2) in ].0,PI.[ by A6,A8,Th16;
hence thesis by XXREAL_1:4;
end;
end;
suppose
Arg(z1)>0;
then Arg(z1) in ].0,PI.[ by A1,XXREAL_1:4;
then
A9: Im z1>0 by Th16;
per cases by COMPTRIG:34;
suppose
Arg(z2)=0;
then z2= |.z2.| by Th13;
then
A10: Im z2=0 by A3,COMPLEX1:12;
Im (z1+z2)=(Im z1)+(Im z2) by COMPLEX1:8;
then Arg(z1+z2) in ].0,PI.[ by A9,A10,Th16;
hence thesis by XXREAL_1:4;
end;
suppose
Arg(z2)>0;
then Arg(z2) in ].0,PI.[ by A2,XXREAL_1:4;
then
A11: Im z2>0 by Th16;
Im (z1+z2)=(Im z1)+(Im z2) by COMPLEX1:8;
then Arg(z1+z2) in ].0,PI.[ by A9,A11,Th16;
hence thesis by XXREAL_1:4;
end;
end;
end;
theorem Th19:
for z being Complex holds Arg z = 0 iff Re z >= 0 & Im z = 0
proof
let z being Complex;
A1: |.z.| = |.z.|+0*<i>;
hereby
assume Arg z = 0;
then
A2: z = |.z.| by Th13;
then Re z = |.z.| by A1,COMPLEX1:12;
hence Re z >= 0 & Im z = 0 by A1,A2,COMPLEX1:12,46;
end;
assume that
A3: Re z >= 0 and
A4: Im z = 0;
z = Re z +0*<i> by A4,COMPLEX1:13;
hence thesis by A3,COMPTRIG:35;
end;
theorem Th20:
for z being Complex holds Arg z = PI iff Re z < 0 & Im z= 0
proof
let z be Complex;
hereby
assume
A1: Arg z = PI;
per cases;
suppose
A2: z<>0;
reconsider zz=|.z.| as Element of REAL by XREAL_0:def 1;
A3: z=zz*cos PI+|.z.|*sin PI *<i> & --|.z.| > 0
by A1,COMPLEX1:47,COMPTRIG:def 1,A2;
cos PI = -1 & sin PI = 0 by SIN_COS:77;
then
A5: z =zz*(-1)+zz*0*<i> by A3;
hence Re z < 0 by COMPLEX1:def 1,A3;
thus Im z = 0 by COMPLEX1:def 2,A5;
end;
suppose
z=0;
hence Re z < 0 & Im z = 0 by A1,COMPTRIG:5,35;
end;
end;
assume that
A6: Re z < 0 and
A7: Im z=0;
z = Re z +0*<i> by A7,COMPLEX1:13;
hence thesis by A6,COMPTRIG:36;
end;
theorem Th21:
for z being Complex holds Im z = 0 iff Arg z = 0 or Arg z = PI
proof
let z be Complex;
hereby
A1: Arg(Re z+0*<i>) = 0 or Arg(Re z+0*<i>) = PI by COMPTRIG:35,36;
assume Im z = 0;
hence Arg z = 0 or Arg z = PI by A1,COMPLEX1:13;
end;
assume Arg z = 0 or Arg z = PI;
hence thesis by Th19,Th20;
end;
theorem Th22:
for z being Complex st Arg z <= PI holds Im z >= 0
proof
let z be Complex;
assume
A1: Arg z <= PI;
per cases by A1,COMPTRIG:34,XXREAL_0:1;
suppose
Arg z = PI or Arg z = 0;
hence thesis by Th21;
end;
suppose
0 < Arg z & Arg z < PI;
then Arg z in ].0,PI.[ by XXREAL_1:4;
hence thesis by Th16;
end;
end;
theorem Th23:
for z being Element of COMPLEX st z <> 0 holds cos Arg -z = -cos
Arg z & sin Arg -z = - sin Arg z
proof
let a be Element of COMPLEX;
A1: |.-a.| = |.a.| by COMPLEX1:52;
assume a <> 0;
then
A2: |.a.|<>0 by COMPLEX1:45;
a = |.a.|*cos Arg a+(|.a.|*sin Arg a)*<i> & -a = |.-a.|*cos Arg -a+(|.-a
.|* sin Arg -a)*<i> by COMPTRIG:62;
then
A3: 0+0*<i> = |.a.|*cos Arg a + (|.a.|*cos Arg -a)+ (|.a.|*sin Arg a + (|.a
.|*sin Arg -a))*<i> by A1;
then |.a.|*(sin Arg a+sin Arg -a)= 0 by COMPLEX1:4,12;
then
A4: sin Arg a +--sin Arg -a = 0 by A2;
|.a.|*(cos Arg a + cos Arg -a) = 0 by A3,COMPLEX1:4,12;
then cos Arg a +--cos Arg -a = 0 by A2;
hence thesis by A4;
end;
theorem Th24:
for a being Complex st a <> 0 holds cos Arg a = Re a / |.
a.| & sin Arg a = Im a / |.a.|
proof
let a be Complex;
a = |.a.|*cos Arg a+(|.a.|*sin Arg a)*<i> by COMPTRIG:62;
then
A1: Re a = |.a.|*cos Arg a & Im a = |.a.|*sin Arg a by COMPLEX1:12;
assume a <> 0;
hence thesis by A1,COMPLEX1:45,XCMPLX_1:89;
end;
theorem Th25:
for a being Complex, r being Real
st r > 0 holds Arg(a*r) = Arg a
proof
let a be Complex, r be Real such that
A1: r > 0;
per cases;
suppose
a = 0;
hence thesis;
end;
suppose
A2: a <> 0;
then
A3: sin Arg a = Im a/|.a.| by Th24;
set b = a*r;
A4: |.b.| = |.a.|*|.r.| by COMPLEX1:65
.= |.a.|*r by A1,ABSVALUE:def 1;
A5: cos Arg a = Re a/|.a.| by A2,Th24;
A6: 0 <= Arg a & Arg a < 2*PI by COMPTRIG:34;
r=r+0*<i>;
then
A7: Re r = r & Im r = 0 by COMPLEX1:12;
then
A8: Im b = Re a * 0 + r * Im a by COMPLEX1:9
.= r*Im a;
A9: sin Arg b = Im b /|.b.| by A1,A2,Th24
.=sin Arg a by A1,A8,A4,A3,XCMPLX_1:91;
A10: 0 <= Arg b & Arg b < 2*PI by COMPTRIG:34;
A11: Re b = Re a * r - 0*Im a by A7,COMPLEX1:9
.= r*Re a;
cos Arg b = Re b/|.b.|by A1,A2,Th24
.=cos Arg a by A1,A11,A4,A5,XCMPLX_1:91;
hence thesis by A9,A10,A6,Th11;
end;
end;
theorem Th26:
for a being Complex, r being Real
st r < 0 holds Arg(a*r) = Arg -a
proof
let a be Complex, r be Real such that
A1: r < 0;
per cases;
suppose
a = 0;
hence thesis;
end;
suppose
A2: a <> 0;
then
A3: cos Arg a = Re a/|.a.| by Th24;
A4: 0 <= Arg -a & Arg -a < 2*PI by COMPTRIG:34;
A5: sin Arg a = Im a/|.a.| by A2,Th24;
set b = a*r;
A6: a in COMPLEX by XCMPLX_0:def 2;
A7: 0 <= Arg b & Arg b < 2*PI by COMPTRIG:34;
A8: |.b.| = |.a.|*|.r.| by COMPLEX1:65
.= |.a.|*(-r) by A1,ABSVALUE:def 1;
r =r+0*<i>;
then
A9: Re r = r & Im r = 0 by COMPLEX1:12;
then Im b = Re a * 0 + r * Im a by COMPLEX1:9
.= r*Im a;
then
A10: sin Arg b = r*Im a/(-|.a.|*r) by A1,A2,A8,Th24
.= -r*Im a/( |.a.|*r) by XCMPLX_1:188
.= -sin Arg a by A1,A5,XCMPLX_1:91
.= sin Arg -a by A2,A6,Th23;
Re b = Re a * r - 0*Im a by A9,COMPLEX1:9
.= r*Re a;
then cos Arg b = r*Re a/(-|.a.|*r) by A1,A2,A8,Th24
.= -r*Re a/( |.a.|*r) by XCMPLX_1:188
.= -cos Arg a by A1,A3,XCMPLX_1:91
.= cos Arg -a by A2,A6,Th23;
hence thesis by A10,A7,A4,Th11;
end;
end;
begin :: Inner product
definition
let x, y be Complex;
func x .|. y -> Element of COMPLEX equals
x*(y*');
correctness by XCMPLX_0:def 2;
end;
reserve a, b, c, d, x, y, z for Complex;
theorem Th27:
x.|.y = (Re x)*(Re y)+(Im x)*(Im y) + (-(Re x)*(Im y)+(Im x)*(Re y))*<i>
proof
x = Re x+(Im x)*<i> & y*' = Re y-(Im y)*<i> by COMPLEX1:13,def 11;
hence thesis;
end;
theorem Th28:
z.|.z = (Re z)*(Re z)+(Im z)*(Im z) & z.|.z = (Re z)^2+(Im z)^2
proof
thus z.|.z = (Re z)*(Re z)+(Im z)*(Im z)+(-((Im z)*(Re z))+(Im z)*(Re z)
)*<i> by Th27
.= (Re z)*(Re z)+(Im z)*(Im z);
hence thesis;
end;
theorem Th29:
z.|.z = |.z.|^2 & |.z.|^2 = Re (z.|.z)
proof
A1: (Re z)^2>=0 & (Im z)^2>=0 by XREAL_1:63;
A2: |.z.|=sqrt((Re z)^2 + (Im z)^2) by COMPLEX1:def 12;
thus
A3: z.|.z = (Re z)^2+(Im z)^2 by Th28
.= |.z.|^2 by A1,A2,SQUARE_1:def 2;
|.z.|^2 = |.z.|^2+(0*<i> qua Complex);
hence thesis by A3,COMPLEX1:12;
end;
theorem Th30:
|. x.|.y .| = |.x.|*|.y.|
proof
thus |.(x.|.y).| =(|.x.|)*(|.y*'.|) by COMPLEX1:65
.=|.x.|*|.y.| by COMPLEX1:53;
end;
theorem
x.|.x = 0 implies x = 0
proof
assume x.|.x = 0;
then (Re x)^2+(Im x)^2 = 0 by Th28;
hence thesis by COMPLEX1:5;
end;
theorem Th32:
y.|.x = (x.|.y)*'
proof
thus (y.|.x)=(y*x*')*'*' .=((x*')*'*(y*'))*' by COMPLEX1:35
.=(x.|.y)*';
end;
theorem
(x+y).|.z = x.|.z + y.|.z;
theorem Th34:
x.|.(y+z) = x.|.y + x.|.z
proof
thus x.|.(y+z) =x*(y*'+z*') by COMPLEX1:32
.=(x.|.y)+(x.|.z);
end;
theorem
(a*x).|.y = a * x.|.y;
theorem Th36:
x.|.(a*y) = (a*') * x.|.y
proof
thus x.|.(a*y) =x*((a*')*(y*')) by COMPLEX1:35
.= (a*') * x.|.y;
end;
theorem
(a*x).|.y = x.|.((a*')*y)
proof
thus (a*x).|.y =x*((a*'*')*(y*')) .= x.|.((a*')*y) by COMPLEX1:35;
end;
theorem
(a*x+b*y).|.z = a * x.|.z + b * y.|.z;
theorem
x.|.(a*y + b*z) = (a*') * x.|.y + (b*') * x.|.z
proof
thus x.|.(a*y + b*z) = x.|.(a*y) +x.|.(b*z) by Th34
.=(a*')*x.|.y + x.|.(b*z) by Th36
.=(a*') * x.|.y + (b*') * x.|.z by Th36;
end;
theorem Th40:
(-x).|.y = x.|.(-y)
proof
thus (-x).|.y = (-(1r*')) * x.|.y by COMPLEX1:30,def 4
.=((-1r)*')* x.|.y by COMPLEX1:33
.= x.|.((-1r)*y) by Th36
.=x.|.(-y) by COMPLEX1:def 4;
end;
theorem
(-x).|.y = - x.|.y;
theorem Th42:
- x.|.y = x.|.(-y)
proof
thus - x.|.y = (-x).|.y .=x.|.(-y) by Th40;
end;
theorem
(-x).|.(-y) = x.|.y
proof
(-x).|.(-y) = - x.|.(-y) .= - ( - x.|.y ) by Th42;
hence thesis;
end;
theorem
(x - y).|.z = x.|.z - y.|.z;
theorem Th45:
x.|.(y - z) = x.|.y - x.|.z
proof
thus x.|.(y-z) =x*(y*'-z*') by COMPLEX1:34
.=(x.|.y)-(x.|.z);
end;
theorem
(x + y).|.(x + y) = x.|.x + x.|.y + y.|.x + y.|.y
proof
(x + y).|.(x + y) = x.|.(x+y) + y.|.(x+y)
.= x.|.x + x.|.y + y.|.(x+y) by Th34
.= x.|.x + x.|.y + (y.|.x + y.|.y) by Th34
.= x.|.x + x.|.y + y.|.x + y.|.y;
hence thesis;
end;
theorem Th47:
(x-y).|.(x-y) = x.|.x - x.|.y - y.|.x + y.|.y
proof
(x - y).|.(x - y) =x.|.(x - y) - y.|.(x - y)
.=x.|.x - x.|.y - y.|.(x - y) by Th45
.=x.|.x - x.|.y - (y.|.x - y.|.y) by Th45
.=x.|.x - x.|.y - y.|.x + y.|.y;
hence thesis;
end;
Lm2: (|.z.|)^2 = (Re z)^2 + (Im z)^2
proof
thus (|.z.|)^2 =|.z*z.| by COMPLEX1:65
.= (Re z)^2 + (Im z)^2 by COMPLEX1:68;
end;
theorem Th48:
Re (x.|.y) = 0 iff Im (x.|.y) = |.x.|*|.y.| or Im (x.|.y) = -|.x .|*|.y.|
proof
hereby
assume
A1: Re (x.|.y)=0;
(|.x.|*|.y.|)^2=(|.(x.|.y).|)^2 by Th30
.=0^2+ (Im (x.|.y))^2 by A1,Lm2
.= (Im (x.|.y))^2;
hence Im (x.|.y)=|.x.|*|.y.| or Im (x.|.y)= - (|.x.|*|.y.|) by SQUARE_1:40;
end;
hereby
assume Im (x.|.y)=|.x.|*|.y.| or Im (x.|.y)= - (|.x.|*|.y.|);
then (Im (x.|.y))^2= (|.x.|*|.y.|)^2 .= (|.(x.|.y).|)^2 by Th30
.=(Re (x.|.y))^2+(Im (x.|.y))^2 by Lm2;
hence Re (x.|.y)=0;
end;
end;
begin :: Rotation
definition
let a be Complex, r be Real;
func Rotate(a, r) -> Element of COMPLEX equals
|.a.|*cos (r+Arg a) + |.a.|*
sin (r+Arg a) *<i>;
correctness by XCMPLX_0:def 2;
end;
reserve r for Real;
theorem
Rotate(a, 0) = a by COMPTRIG:62;
theorem Th50:
for a being Complex holds Rotate(a, r) = 0 iff a = 0
proof
let a be Complex;
hereby
assume Rotate(a, r) = 0;
then
A1: Rotate(a, r) = 0+0*<i>;
per cases by A1,COMPLEX1:77;
suppose
|.a.| = 0;
hence a = 0 by COMPLEX1:45;
end;
suppose
cos (r+Arg a) = 0 & sin (r+Arg a) = 0;
hence a = 0 by Th10;
end;
end;
assume a = 0;
hence thesis by COMPLEX1:44;
end;
theorem Th51:
for a being Complex holds |.Rotate(a,r).| = |.a.|
proof
let a be Complex;
Re Rotate(a,r) = |.a.|*cos (r+Arg a) & Im Rotate(a,r) = |.a.|*sin (r+
Arg a) by COMPLEX1:12;
hence |.Rotate(a,r).| = sqrt((|.a.|*cos (r+Arg a))^2 + (|.a.|*sin (r+Arg a))
^2) by COMPLEX1:def 12
.= sqrt(|.a.|^2*((cos (r+Arg a))^2 + (sin (r+Arg a))^2))
.= sqrt(|.a.|^2*1) by SIN_COS:29
.= |.a.| by COMPLEX1:46,SQUARE_1:22;
end;
theorem Th52:
for a being Complex st a <> 0 ex i being Integer st Arg(
Rotate(a,r)) = 2*PI*i+(r+Arg(a))
proof
let a be Complex;
A1: |.a.| = |.Rotate(a,r).| by Th51;
assume a <> 0;
then
A2: Rotate(a, r) <> 0c by Th50;
take -[\ (r+Arg a)/(2*PI) /];
consider AR being Real such that
A3: AR = 2*PI*-[\ (r+Arg a)/(2*PI) /]+(r+Arg a) and
A4: 0 <= AR & AR < 2*PI by Th1,COMPTRIG:5;
cos (r+Arg a) = cos AR & sin (r+Arg a) = sin AR by A3,Th8,Th9;
hence thesis by A2,A1,A3,A4,COMPTRIG:def 1;
end;
theorem
Rotate(a,-Arg a) = |.a.| by SIN_COS:31;
theorem Th54:
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
a = |.a.|*cos Arg a+(|.a.|*sin Arg a)*<i> by COMPTRIG:62;
then
A1: Re a = |.a.|*cos Arg a & Im a = |.a.|*sin Arg a by COMPLEX1:12;
thus Re Rotate(a,r) = |.a.|*cos (r+Arg a) by COMPLEX1:12
.= |.a.|*((cos r)*cos(Arg a)-(sin r)*sin(Arg a)) by SIN_COS:75
.= (Re a)*(cos r)-(Im a)*(sin r) by A1;
thus Im Rotate(a,r) = |.a.|*sin(r+Arg a) by COMPLEX1:12
.= |.a.|*((sin r)*cos(Arg a)+(cos r)*sin(Arg a)) by SIN_COS:75
.= (Re a)*(sin r)+(Im a)*(cos r) by A1;
end;
theorem Th55:
Rotate(a+b,r) = Rotate(a,r)+Rotate(b,r)
proof
set ab = a+b;
set rab = Rotate(ab,r),ra = Rotate(a,r), rb = Rotate(b,r);
A1: Re ab = Re a + Re b & Im ab = Im a + Im b by COMPLEX1:8;
A2: Im rab = (Re ab)*(sin r)+(Im ab)*(cos r) by Th54;
Im ra = (Re a)*(sin r)+(Im a)*(cos r) & Im rb = (Re b)*(sin r)+(Im b)*(
cos r ) by Th54;
then
A3: Im (ra+rb) = (Re a)*(sin r)+(Im a)*(cos r)+((Re b)*(sin r)+(Im b)*(cos
r)) by COMPLEX1:8
.= Im rab by A2,A1;
A4: Re rab = (Re ab)*(cos r)-(Im ab)*(sin r) by Th54;
Re ra = (Re a)*(cos r)-(Im a)*(sin r) & Re rb = (Re b)*(cos r)-(Im b)*(
sin r ) by Th54;
then
Re (ra+rb) = (Re a)*(cos r)-(Im a)*(sin r)+((Re b)*(cos r)-(Im b)*(sin r
)) by COMPLEX1:8
.= Re rab by A4,A1;
hence thesis by A3,COMPLEX1:3;
end;
theorem Th56:
Rotate(-a,r) = -Rotate(a,r)
proof
per cases;
suppose
A1: a <> 0c;
A2: cos (r+Arg-a) = -cos(r+Arg a) & sin (r+Arg-a) = -sin(r+Arg a)
proof
per cases;
suppose
Arg a < PI;
then Arg -a = PI+Arg a by A1,Th12;
then r+Arg-a = PI+(r+Arg a);
hence thesis by SIN_COS:79;
end;
suppose
Arg a >= PI;
then Arg -a = (Arg a)-PI by A1,Th12;
then r+Arg-a = (Arg a)+r-PI;
hence thesis by Th5;
end;
end;
|.a.| = |.-a.| by COMPLEX1:52;
hence thesis by A2;
end;
suppose
A3: a = 0c;
hence Rotate(-a,r) = -0 by Th50
.= -Rotate(a,r) by A3,Th50;
end;
end;
theorem Th57:
Rotate(a-b,r) = Rotate(a,r)-Rotate(b,r)
proof
thus Rotate(a-b,r) = Rotate(a,r)+Rotate(-b,r) by Th55
.= Rotate(a,r)-Rotate(b,r) by Th56;
end;
theorem Th58:
Rotate(a, PI) = -a
proof
A1: a = |.a.|*cos Arg a+(|.a.|*sin Arg a)*<i> by COMPTRIG:62;
A2: |.a.|*-sin Arg a = -(|.a.|*sin Arg a) .= - Im a by A1,COMPLEX1:12;
A3: |.a.|*-cos Arg a = -(|.a.|*cos Arg a) .= - Re a by A1,COMPLEX1:12;
thus Rotate(a, PI) = |.a.|*-cos Arg a + |.a.|*sin (PI+Arg a) *<i> by
SIN_COS:79
.= |.a.|*-cos Arg a + (|.a.|*-sin Arg a) *<i> by SIN_COS:79
.= -a by A3,A2,COMPLEX1:83;
end;
begin :: Angles
definition
let a, b be Complex;
func angle(a,b) -> Real equals
:Def3:
Arg(Rotate(b, -Arg a)) if Arg a = 0 or
b <> 0 otherwise 2*PI - Arg a;
correctness;
end;
theorem Th59:
for a being Complex holds r >= 0 implies angle(r,a) = Arg a
proof
let a be Complex;
assume r >= 0;
then Arg r = 0 by COMPTRIG:35;
hence angle(r,a) = Arg(Rotate(a,-0)) by Def3
.= Arg a by COMPTRIG:62;
end;
theorem Th60:
for a,b being Complex holds Arg a = Arg b & a <> 0 & b <>
0 implies Arg Rotate(a,r) = Arg Rotate(b,r)
proof
let a,b be Complex;
assume that
A1: Arg a = Arg b and
A2: a <> 0 and
A3: b <> 0;
consider i being Integer such that
A4: Arg(Rotate(a,r)) = 2*PI*i+(r+Arg(a)) by A2,Th52;
consider j being Integer such that
A5: Arg(Rotate(b,r)) = 2*PI*j+(r+Arg(b)) by A3,Th52;
A6: 0 <= Arg Rotate(a,r) & 0 <= Arg Rotate(b,r) by COMPTRIG:34;
A7: Arg Rotate(a,r) < 2*PI & Arg Rotate(b,r) < 2*PI by COMPTRIG:34;
Arg(Rotate(b,r)) = 2*PI*(j-i)+Arg(Rotate(a,r)) by A1,A4,A5;
hence thesis by A6,A7,Th2;
end;
theorem Th61:
r > 0 implies angle(a,b) = angle(a*r,b*r)
proof
assume
A1: r > 0;
then
A2: Arg(a*r) = Arg a by Th25;
per cases;
suppose
A3: b <> 0;
hence angle(a,b) = Arg(Rotate(b,-Arg a)) by Def3
.= Arg(Rotate(b*r,-Arg(a*r))) by A1,A2,A3,Th25,Th60
.= angle(a*r,b*r) by A1,A3,Def3;
end;
suppose
A4: b = 0;
thus thesis
proof
per cases;
suppose
A5: Arg a = 0;
hence angle(a,b) = Arg(Rotate(b,-Arg a)) by Def3
.= Arg 0c by A4,Th50
.= Arg(Rotate(b*r,-Arg(a*r))) by A4,Th50
.= angle(a*r,b*r) by A2,A5,Def3;
end;
suppose
A6: Arg a <> 0;
hence angle(a,b) = 2*PI-Arg a by A4,Def3
.= angle(a*r,b*r) by A2,A4,A6,Def3;
end;
end;
end;
end;
theorem Th62:
a <> 0 & b <> 0 & Arg a = Arg b implies Arg -a = Arg -b
proof
assume a <> 0 & b <> 0 & Arg a = Arg b;
then Arg Rotate(a,PI) = Arg Rotate(b,PI) by Th60;
then Arg -a = Arg Rotate(b,PI) by Th58;
hence thesis by Th58;
end;
theorem Th63:
a <> 0 & b <> 0 implies angle(a,b) = angle(Rotate(a,r),Rotate(b, r))
proof
assume that
A1: a <> 0 and
A2: b <> 0;
consider i being Integer such that
A3: Arg(Rotate(b, -Arg a)) = 2*PI*i+(-(Arg a) + Arg(b)) by A2,Th52;
consider l being Integer such that
A4: Arg Rotate(b,r) = 2*PI*l+(r+Arg(b)) by A2,Th52;
consider k being Integer such that
A5: Arg Rotate(a,r) = 2*PI*k+(r+Arg(a)) by A1,Th52;
A6: 0 <= Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r))) & Arg(Rotate(Rotate(b,r
), - Arg Rotate(a,r))) < 2*PI by COMPTRIG:34;
A7: 0 <= Arg(Rotate(b, -Arg a)) & Arg(Rotate(b, -Arg a)) < 2*PI by COMPTRIG:34;
A8: Rotate(b,r) <> 0 by A2,Th50;
then consider j being Integer such that
A9: Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r))) = 2*PI*j+(-(Arg Rotate(a,
r)) + Arg(Rotate(b,r))) by Th52;
A10: Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r))) = 2*PI*(j-k+l-i)+Arg(Rotate(b
, -Arg a)) by A3,A9,A5,A4;
thus angle(a,b) = Arg(Rotate(b, -Arg a)) by A2,Def3
.= Arg(Rotate(Rotate(b,r), -Arg Rotate(a,r))) by A10,A7,A6,Th2
.= angle(Rotate(a,r),Rotate(b,r)) by A8,Def3;
end;
theorem
r < 0 & a <> 0 & b <> 0 implies angle(a,b) = angle(a*r,b*r)
proof
assume that
A1: r < 0 and
A2: a <> 0 and
A3: b <> 0;
consider i being Integer such that
A4: Arg(Rotate(-b, -Arg -a)) = 2*PI*i+(-Arg -a + Arg -b) by A3,Th52;
set br = b*r, ar = a*r;
Arg(b*r) = Arg -b & Arg(a*r) = Arg -a by A1,Th26;
then consider j being Integer such that
A5: Arg(Rotate(br,-Arg ar)) = 2*PI*j+(-Arg -a + Arg -b) by A1,A3,Th52;
A6: Arg(Rotate(br,-Arg ar)) = 2*PI*(j-i)+Arg(Rotate(-b,-Arg -a)) by A4,A5;
A7: 0 <= Arg(Rotate(br,-Arg ar)) & Arg(Rotate(br,-Arg ar)) < 2*PI by
COMPTRIG:34;
A8: 0 <= Arg(Rotate(-b,-Arg -a)) & Arg(Rotate(-b,-Arg -a)) < 2*PI by
COMPTRIG:34;
thus angle(a,b) = angle(Rotate(a,PI),Rotate(b,PI)) by A2,A3,Th63
.= angle(-a,Rotate(b,PI)) by Th58
.= angle(-a,-b) by Th58
.= Arg(Rotate(-b,-Arg -a)) by A3,Def3
.= Arg(Rotate(br,-Arg ar)) by A6,A7,A8,Th2
.= angle(a*r,b*r) by A1,A3,Def3;
end;
theorem
a <> 0 & b <> 0 implies angle(a,b) = angle(-a,-b)
proof
assume a <> 0 & b <> 0;
hence angle(a,b) = angle(Rotate(a,PI),Rotate(b,PI)) by Th63
.= angle(-a,Rotate(b,PI)) by Th58
.= angle(-a,-b) by Th58;
end;
theorem
b <> 0 & angle(a,b) = 0 implies angle(a,-b) = PI
proof
assume that
A1: b <> 0 and
A2: angle(a,b) = 0;
A3: Arg(Rotate(b, -Arg a)) = 0 by A1,A2,Def3;
A4: Arg(Rotate(-b, -Arg a)) = Arg(-Rotate(b, -Arg a)) by Th56;
Rotate(b, -Arg a) <> 0 by A1,Th50;
then Arg -Rotate(b, -Arg a) = Arg Rotate(b, -Arg a)+PI by A3,Th12,COMPTRIG:5
.= PI by A3;
hence thesis by A1,A4,Def3;
end;
theorem Th67:
a <> 0 & b <> 0 implies cos angle(a,b) = Re (a.|.b)/(|.a.|*|.b.|
) & sin angle(a,b) = - Im (a.|.b)/(|.a.|*|.b.|)
proof
assume that
A1: a <> 0 and
A2: b <> 0;
A3: |.a.| <> 0 & |.b.| <> 0 by A1,A2,COMPLEX1:45;
set ra = Rotate(a,-Arg a), rb = Rotate(b,-Arg a), r = -Arg a;
set mabi = (|.a.|*|.b.|)";
A4: |.a.| >= 0 & |.b.| >= 0 by COMPLEX1:46;
angle(a,b) = angle(ra,rb) by A1,A2,Th63;
then
A5: angle(a,b) = angle(|.a.|*mabi,rb*mabi) by A3,A4,Th61,SIN_COS:31
.= Arg(rb*mabi) by A4,Th59;
A6: a = |.a.|*cos Arg a+(|.a.|*sin Arg a)*<i> by COMPTRIG:62;
then Re a = |.a.|*cos Arg a by COMPLEX1:12;
then
A7: cos Arg a = (Re a)/|.a.| by A1,COMPLEX1:45,XCMPLX_1:89;
Im a = |.a.|*sin Arg a by A6,COMPLEX1:12;
then
A8: sin Arg a = (Im a)/|.a.| by A1,COMPLEX1:45,XCMPLX_1:89;
A9: a.|.b = (Re a)*(Re b)+(Im a)*(Im b)+(-((Re a)*(Im b))+(Im a)*(Re b))*
<i> by Th27;
then
A10: Re (a.|.b) = (Re a)*(Re b)+(Im a)*(Im b) by COMPLEX1:12;
Re rb = (Re b)*(cos r)-(Im b)*(sin r) by Th54;
then
A11: Re rb = (Re b)*(cos r)-(Im b)*(-sin Arg a) by SIN_COS:31
.= (Re b)*((Re a)/|.a.|)+(Im b)*((Im a)/|.a.|) by A7,A8,SIN_COS:31
.= Re (a.|.b) / |.a.| by A10;
A12: (Im rb)^2 >= 0 by XREAL_1:63;
Im rb = (Re b)*(sin r)+(Im b)*(cos r) by Th54;
then
A13: Im rb = (Re b)*(-sin Arg a)+(Im b)*(cos r) by SIN_COS:31
.= (-(Re b))*((Im a)/|.a.|)+(Im b)*((Re a)/|.a.|) by A7,A8,SIN_COS:31
.= -(-((-(Re b))*(Im a)+(Im b)*(Re a)))/|.a.|
.= - Im (a.|.b)/|.a.| by A9,COMPLEX1:12;
set IT = rb*mabi;
set mab = (|.a.|*|.b.|);
A14: mabi^2 >= 0 & (Re rb)^2 >= 0 by XREAL_1:63;
mabi = mabi+0*<i>;
then
A15: Re mabi = mabi & Im mabi = 0 by COMPLEX1:12;
then
A16: Re IT = Re rb * mabi - (Im rb)*0 by COMPLEX1:9
.= Re rb * mabi;
A17: Im IT = Re rb * 0 + Im rb * mabi by A15,COMPLEX1:9
.= Im rb * mabi;
then
A18: |.IT.| = sqrt((Re rb * mabi)^2+(Im rb * mabi)^2) by A16,COMPLEX1:def 12
.= sqrt(mabi^2*((Re rb)^2+(Im rb)^2))
.= sqrt(mabi^2)*sqrt((Re rb)^2+(Im rb)^2) by A14,A12,SQUARE_1:29
.= mabi*sqrt((Re rb)^2+(Im rb)^2) by A4,SQUARE_1:22
.= mabi*|.rb.| by COMPLEX1:def 12
.= mabi*|.b.| by Th51;
A19: IT = |.IT.|*cos Arg IT+(|.IT.|*sin Arg IT)*<i> by COMPTRIG:62;
then |.IT.|*cos Arg IT = Re rb * mabi by A16,COMPLEX1:12;
hence cos angle(a,b) = Re rb * mabi/|.IT.| by A3,A5,A18,XCMPLX_1:89
.= Re rb *(mabi/|.IT.|)
.= Re (a.|.b) / |.a.|*(mabi/mabi/|.b.|) by A11,A18,XCMPLX_1:78
.= Re (a.|.b) / |.a.|*(1/|.b.|) by A3,XCMPLX_1:60
.= Re (a.|.b)*1 / (|.a.|*|.b.|) by XCMPLX_1:76
.= Re (a.|.b)/mab;
|.IT.|*sin Arg IT = Im rb * mabi by A19,A17,COMPLEX1:12;
hence sin angle(a,b) = Im rb * mabi/|.IT.| by A3,A5,A18,XCMPLX_1:89
.= Im rb * (mabi/|.IT.|)
.= (- Im (a.|.b) / |.a.|)*(mabi/mabi/|.b.|) by A13,A18,XCMPLX_1:78
.= ((- Im (a.|.b)) / |.a.|)*(1/|.b.|) by A3,XCMPLX_1:60
.= (- Im (a.|.b))*1/(|.a.|*|.b.|) by XCMPLX_1:76
.= - Im (a.|.b)/mab;
end;
definition
let x, y, z be Complex;
func angle(x,y,z) -> Real equals
:Def4:
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;
theorem Th68:
0 <= angle(x,y,z) & angle(x,y,z) < 2*PI
proof
now
per cases;
case
A1: Arg(z-y)-Arg(x-y)>=0;
Arg(x-y)>=0 by COMPTRIG:34;
then Arg(z-y)+0<=Arg(z-y)+Arg(x-y) by XREAL_1:7;
then
A2: Arg(z-y)<2*PI & Arg(z-y)-Arg(x-y)<=Arg(z-y) by COMPTRIG:34,XREAL_1:20;
angle(x,y,z)=Arg(z-y)-Arg(x-y) by A1,Def4;
hence thesis by A1,A2,XXREAL_0:2;
end;
case
A3: Arg(z-y)-Arg(x-y)<0;
Arg(z-y)>=0 by COMPTRIG:34;
then Arg(x-y)+0<=Arg(x-y)+Arg(z-y) by XREAL_1:7;
then Arg(x-y)<2*PI & Arg(x-y)-Arg(z-y)<=Arg(x-y) by COMPTRIG:34
,XREAL_1:20;
then (Arg(x-y)-Arg(z-y))<2*PI by XXREAL_0:2;
then
A4: 2*PI-(Arg(x-y)-Arg(z-y))>0 by XREAL_1:50;
Arg(z-y)-Arg(x-y) + 2*PI < 0 + 2*PI by A3,XREAL_1:8;
hence thesis by A3,A4,Def4;
end;
end;
hence thesis;
end;
theorem Th69:
angle(x,y,z)=angle(x-y,0,z-y)
proof
now
per cases;
case
A1: Arg((z-y)-0c)-Arg((x-y)-0c)>=0;
then angle(x-y,0c,z-y)=Arg(z-y)-Arg(x-y) by Def4;
hence angle(x-y,0c,z-y)=angle(x,y,z) by A1,Def4;
end;
case
A2: Arg((z-y)-0c)-Arg((x-y)-0c)<0;
then angle(x-y,0c,z-y)=2*PI+(Arg(z-y)-Arg(x-y)) by Def4;
hence angle(x-y,0c,z-y)=angle(x,y,z) by A2,Def4;
end;
end;
hence thesis;
end;
theorem Th70:
angle(a,b,c) = angle(a+d,b+d,c+d)
proof
thus angle(a,b,c) = angle(a-b,0c,c-b) by Th69
.= angle((a+d)-(b+d),0c,(c+d)-(b+d))
.= angle(a+d,b+d,c+d) by Th69;
end;
theorem Th71:
angle(a,b) = angle(a,0,b)
proof
set ab2 = angle(a,b);
A1: 0 <= Arg(Rotate(b,-Arg a)) & Arg(Rotate(b,-Arg a)) < 2*PI by COMPTRIG:34;
per cases;
suppose
A2: b <> 0;
then
A3: ab2 = Arg(Rotate(b, -Arg a)) by Def3;
thus thesis
proof
per cases;
suppose
Arg(b-0c)-Arg(a-0c) >= 0;
then
A4: angle(a,0c,b) = -Arg(a)+Arg(b) by Def4;
A5: angle(a,0c,b) < 2*PI by Th68;
(ex i being Integer st Arg(Rotate(b,-Arg a)) = 2*PI*i+(- Arg a +
Arg(b)) )& 0 <= angle(a,0c,b) by A2,Th52,Th68;
hence thesis by A1,A3,A4,A5,Th2;
end;
suppose
A6: Arg(b-0c)-Arg(a-0c) < 0;
consider i being Integer such that
A7: Arg(Rotate(b,-Arg a)) = 2*PI*i+(-Arg a + Arg(b)) by A2,Th52;
A8: 2*PI*i+(-Arg a + Arg(b)) = 2*PI*(i-1)+(2*PI+(-Arg a + Arg(b)));
A9: angle(a,0c,b) = 2*PI+(Arg(b)+-Arg(a)) by A6,Def4;
then 0 <= 2*PI+(-Arg a + Arg(b)) & 2*PI+(-Arg a + Arg(b)) < 2*PI by
Th68;
hence thesis by A1,A3,A9,A7,A8,Th2;
end;
end;
end;
suppose
A10: b = 0;
thus thesis
proof
per cases;
suppose
A11: Arg a = 0;
then
A12: Arg(b-0c)-Arg(a-0c) = 0 by A10,COMPTRIG:35;
ab2=Arg(Rotate(b, -Arg a)) by A11,Def3
.= 0 by A10,Lm1,Th50;
hence thesis by A12,Def4;
end;
suppose
A13: Arg a <> 0;
then
A14: 0 < --Arg a by COMPTRIG:34;
Arg(b-0c)-Arg(a-0c) = - Arg a by A10,Lm1;
then angle(a,0c,b) = 2*PI-Arg a by A14,Def4;
hence thesis by A10,A13,Def3;
end;
end;
end;
end;
theorem Th72:
angle(x,y,z) = 0 implies Arg(x-y) = Arg(z-y) & angle(z,y,x)=0
proof
assume
A1: angle(x,y,z) =0;
now
per cases;
case
Arg(z-y)-Arg(x-y)>=0;
then Arg(z-y)-Arg(x-y)=0 by A1,Def4;
hence thesis by Def4;
end;
case
A2: Arg(z-y)-Arg(x-y)<0;
then -(Arg(z-y)-Arg(x-y))>0;
then
A3: angle(z,y,x)=Arg(x-y)-Arg(z-y) by Def4;
angle(x,y,z)=2*PI+(Arg(z-y)-Arg(x-y)) by A2,Def4;
hence contradiction by A1,A3,Th68;
end;
end;
hence thesis;
end;
theorem Th73:
a <> 0 & b <> 0 implies (Re (a.|.b) = 0 iff angle(a,0,b) = PI/2
or angle(a,0,b) = 3/2*PI)
proof
A1: -Im (a.|.b)/(|.a.|*|.b.|) = (-Im (a.|.b))/(|.a.|*|.b.|);
assume
A2: a <> 0 & b <> 0;
then
A3: |.a.| <> 0 & |.b.| <> 0 by COMPLEX1:45;
A4: angle(a,b) = angle(a,0c,b) & 0 <= angle(a,0c,b) by Th68,Th71;
A5: angle(a,0c,b) < 2*PI & PI/2 < 2*PI by Th68,COMPTRIG:5,XXREAL_0:2;
A6: cos angle(a,b) = Re (a.|.b)/(|.a.|*|.b.|) by A2,Th67;
A7: sin angle(a,b) = - Im (a.|.b)/(|.a.|*|.b.|) by A2,Th67;
hereby
assume
A8: Re (a.|.b) = 0;
then Im (a.|.b)=|.a.|*|.b.| or Im (a.|.b)= - (|.a.|*|.b.|) by Th48;
then sin angle(a,b) = 1 or sin angle(a,b) = -1 by A7,A3,A1,XCMPLX_1:60;
hence angle(a,0,b) = PI/2 or angle(a,0,b) = 3/2*PI by A6,A4,A5,A8,Th11,
COMPTRIG:5,SIN_COS:77;
end;
assume angle(a,0,b) = PI/2 or angle(a,0,b) = 3/2*PI;
hence thesis by A6,A3,Th71,SIN_COS:77;
end;
theorem
a <> 0 & b <> 0 implies (Im(a.|.b) = |.a.|*|.b.| or Im(a.|.b) = -|.a.|
*|.b .| iff angle(a,0,b) = PI/2 or angle(a,0,b) = 3/2*PI)
proof
assume
A1: a<>0 & b<>0;
hereby
assume Im(a.|.b)=|.a.|*|.b.| or Im(a.|.b)=-(|.a.|*|.b.|);
then Re (a.|.b)=0 by Th48;
hence angle(a,0,b)=PI/2 or angle(a,0,b)=3/2*PI by A1,Th73;
end;
hereby
assume angle(a,0,b)=PI/2 or angle(a,0,b)=3/2*PI;
then Re (a.|.b)=0 by A1,Th73;
hence Im(a.|.b)=|.a.|*|.b.| or Im(a.|.b)=-(|.a.|*|.b.|) by Th48;
end;
end;
Lm3: for a, b, c being 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
let x, y,z be Complex;
assume x<>y & z<>y;
then
A1: x-y <> 0c & z-y <> 0c;
angle(x,y,z)=angle(x-y,0c,z-y) by Th69;
hence thesis by A1,Th73;
end;
theorem
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
proof
assume
A1: x<>y & z<>y &( angle(x,y,z)=PI/2 or angle(x,y,z)=3/2*PI);
set x3=x-z;
A2: |.x-y.|^2+|.z-y.|^2 =Re ((x-y).|.(x-y)) + |.z-y.|^2 by Th29
.=Re ((x-y).|.(x-y)) + Re ((z-y).|.(z-y)) by Th29
.=Re ((x-y).|.(x-y)+(z-y).|.(z-y)) by COMPLEX1:8;
x3=(x-y)-(z-y);
then
(x-z).|.(x-z) =(x-y).|.(x-y)-(x-y).|.(z-y)-(z-y).|.(x-y) +(z-y).|.(z-y)
by Th47;
then Re((x-z).|.(x-z)) =Re((x-y).|.(x-y)+(z-y).|.(z-y)-((x-y).|.(z-y)+(z-y)
.|.(x-y)))
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-Re((x-y).|.(z-y)+(z-y).|.(x-y))by
COMPLEX1:19
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-(Re((x-y).|.(z-y))+Re((z-y).|.(x-y)))
by COMPLEX1:8
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-(Re((x-y).|.(z-y))+Re(((x-y).|.(z-y))
*')) by Th32
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-(Re((x-y).|.(z-y))+Re((x-y).|.(z-y)))
by COMPLEX1:27
.=Re((x-y).|.(x-y)+(z-y).|.(z-y))-(0+Re((x-y).|.(z-y))) by A1,Lm3
.=Re((x-y).|.(x-y)+(z-y).|.(z-y)) -0 by A1,Lm3
.=Re((x-y).|.(x-y)+(z-y).|.(z- y));
hence thesis by A2,Th29;
end;
theorem Th76:
a <> b & b <> c implies angle(a,b,c) = angle(Rotate(a,r), Rotate
(b,r), Rotate(c,r))
proof
set cb = c-b, ab = a-b;
set rc = Rotate(c,r), rb = Rotate(b,r), ra = Rotate(a,r);
set rcb = Rotate(c,r)-Rotate(b,r), rab = Rotate(a,r)-Rotate(b,r);
assume that
A1: a <> b and
A2: b <> c;
A3: 0 <= angle(a,b,c) & angle(a,b,c) < 2*PI by Th68;
cb <> 0 by A2;
then consider cbi being Integer such that
A4: Arg(Rotate(cb,r)) = 2*PI*cbi+(r+Arg(cb)) by Th52;
ab <> 0 by A1;
then consider abi being Integer such that
A5: Arg(Rotate(ab,r)) = 2*PI*abi+(r+Arg(ab)) by Th52;
A6: 0 <= angle(Rotate(a,r),Rotate(b,r), Rotate(c,r)) & angle(Rotate(a,r),
Rotate( b,r), Rotate(c,r))< 2*PI by Th68;
rab = Rotate(ab,r) by Th57;
then
A7: Arg(rcb)-Arg(rab) = 2*PI*cbi+r+Arg(cb) - (2*PI*abi+r+Arg(ab)) by A5,A4,Th57
.= Arg(cb)-Arg(ab)+2*PI*(cbi-abi);
per cases;
suppose
Arg(c-b)-Arg(a-b) >= 0;
then
A8: angle(a,b,c) = Arg(c-b)-Arg(a-b) by Def4;
thus angle(a,b,c) = angle(Rotate(a,r),Rotate(b,r), Rotate(c,r))
proof
per cases;
suppose
Arg(rcb)-Arg(rab) >= 0;
then angle(ra,rb,rc) = Arg(rcb)-Arg(rab) by Def4;
hence thesis by A3,A6,A7,A8,Th2;
end;
suppose
Arg(rcb)-Arg(rab) < 0;
then angle(ra,rb,rc) = Arg(cb)-Arg(ab)+2*PI*(cbi-abi)+2*PI by A7,Def4
.= Arg(cb)-Arg(ab)+2*PI*(cbi-abi+1);
hence thesis by A3,A6,A8,Th2;
end;
end;
end;
suppose
Arg(cb)-Arg(ab) < 0;
then
A9: angle(a,b,c) = 2*PI+(Arg(cb)-Arg(ab)) by Def4;
thus thesis
proof
per cases;
suppose
Arg(rcb)-Arg(rab) >= 0;
then
angle(ra,rb,rc) = 2*PI+(Arg(cb)-Arg(ab))+2*PI*(cbi-abi+-1) by A7,Def4;
hence thesis by A3,A6,A9,Th2;
end;
suppose
Arg(rcb)-Arg(rab) < 0;
then angle(ra,rb,rc) = Arg(cb)-Arg(ab)+2*PI*(cbi-abi)+2*PI by A7,Def4
.= 2*PI+(Arg(cb)-Arg(ab))+2*PI*(cbi-abi);
hence thesis by A3,A6,A9,Th2;
end;
end;
end;
end;
theorem Th77:
angle(a,b,a) = 0
proof
Arg(a-b)-Arg(a-b) = 0;
hence thesis by Def4;
end;
Lm4: angle(x,y,z) <> 0 implies angle(z,y,x)=2*PI-angle(x,y,z)
proof
assume
A1: angle(x,y,z) <>0;
now
per cases;
case
A2: Arg(x-y)-Arg(z-y)>0;
then --(Arg(x-y)-Arg(z-y))>0;
then angle(x,y,z)=2*PI+(Arg(z-y)-Arg(x-y)) by Def4
.=2*PI -(Arg(x-y)-Arg(z-y));
hence thesis by A2,Def4;
end;
case
A3: Arg(x-y)-Arg(z-y)<=0;
Arg(x-y)-Arg(z-y)<>0 by A1,Def4;
then
A4: angle(z,y,x) =2*PI -(Arg(z-y)-Arg(x-y)) by A3,Def4;
--(Arg(x-y)-Arg(z-y))<=0 by A3;
then angle(x,y,z)+angle(z,y,x) =(2*PI -(Arg(z-y)-Arg(x-y)))+(Arg(z-y)-
Arg(x-y)) by A4,Def4
.=2*PI;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th78: :: COMPLEX2:47, 48
angle(a,b,c) <> 0 iff angle(a,b,c)+angle(c,b,a) = 2*PI
proof
hereby
assume angle(a,b,c) <> 0;
then angle(c,b,a) = 2*PI-angle(a,b,c) by Lm4;
hence angle(a,b,c)+angle(c,b,a) = 2*PI;
end;
assume angle(a,b,c)+angle(c,b,a) = 2*PI & angle(a,b,c) = 0;
hence contradiction by Th68;
end;
theorem
angle(a,b,c) <> 0 implies angle(c,b,a) <> 0
proof
assume angle(a,b,c) <> 0;
then
A1: angle(a,b,c)+angle(c,b,a) = 2*PI by Th78;
assume not thesis;
hence contradiction by A1,Th68;
end;
theorem
angle(a,b,c) = PI implies angle(c,b,a) = PI
proof
assume
A1: angle(a,b,c) = PI;
then angle(a,b,c)+angle(c,b,a) = 0+2*PI by Th78,COMPTRIG:5;
hence thesis by A1;
end;
theorem Th81:
a <> b & a <> c & b <> c implies angle(a,b,c) <> 0 or angle(b,c,
a) <> 0 or angle(c,a,b) <> 0
proof
assume that
A1: a <> b & a <> c and
A2: b <> c;
A3: b-a <> 0 & a-c <> 0 by A1;
c-b <> 0 by A2;
then
A4: Arg(c-b) < PI iff Arg (-(c-b)) >= PI by Th14;
A5: -(b-a) = a-b & -(a-c) = c-a;
A6: -(c-a) = a-c;
assume
A7: not thesis;
then
A8: Arg(a-c) = Arg (b-c) by Th72;
Arg(b-a) = Arg (c-a) by A7,Th72;
then Arg(a-b) = Arg (a-c) by A3,A5,A6,Th62;
hence thesis by A7,A8,A4,Th72;
end;
Lm5: Im a = 0 & Re a > 0 & 0 < Arg(b) & Arg(b) < PI implies angle(a,0c,b)+
angle(0c,b,a)+angle(b,a,0c) = PI & 0 < angle(0c,b,a) & 0 < angle(b,a,0c)
proof
assume that
A1: Im a = 0 and
A2: Re a > 0 and
A3: 0 < Arg(b) and
A4: Arg(b) < PI;
a = Re a + 0*<i> by A1,COMPLEX1:13;
then
A5: Arg(a) = 0 by A2,COMPTRIG:35;
then
A6: Arg(a)-Arg(-a) = Arg(a)-(Arg(a)+PI) by A2,Th12,COMPLEX1:4,COMPTRIG:5
.= -PI;
Arg(b-0c)-Arg(a-0c) >= 0 by A3,A5;
then
A7: angle(a,0c,b) = Arg(b)-Arg(a) by Def4;
Arg b in ].0,PI.[ by A3,A4,XXREAL_1:4;
then
A8: Im b > 0 by Th16;
then
A9: Arg(b)-Arg(-b) = Arg(b)-(Arg(b)+PI) by A4,Th12,COMPLEX1:4
.= -PI;
A10: Im (a-b) = Im a - Im b by COMPLEX1:19
.= - Im b by A1;
then
A11: Arg(a-b) > PI by A8,Th22;
then Arg(b-a) <= PI by A8,A10,Th15,COMPLEX1:4;
then
A12: -Arg(b-a) >= -PI by XREAL_1:24;
A13: Arg(a-b)-Arg(b-a) = Arg(a-b)-Arg(-(a-b))
.= Arg(a-b)-(Arg(a-b)-PI) by A8,A10,A11,Th12,COMPLEX1:4
.= PI;
Arg(-a) = Arg(a)+PI by A2,A5,Th12,COMPLEX1:4,COMPTRIG:5
.= PI by A5;
then Arg(-a)+-Arg(b-a) >= 0-PI+PI by A12,XREAL_1:7;
then
A14: angle(b,a,0c) = Arg(0c-a)-Arg(b-a) by Def4;
now
let a, b be Complex such that
A15: Im a = 0 and
A16: Re a > 0 and
A17: 0 < Arg(b) & Arg(b) < PI;
A18: Re b + -Re a < Re b + 0 by A16,XREAL_1:8;
set ba = b-a;
set B = Arg b, BA = Arg ba, mb = |.b.|, mba = |.b-a.|;
A19: Re (b-a) = Re b - Re a by COMPLEX1:19;
b-a = mba*cos BA + mba*sin BA *<i> & b-a = Re ba+(Im ba)*<i>
by COMPTRIG:62,
COMPLEX1:13;
then
A20: Im ba = mba*sin BA by COMPLEX1:77;
set Rb = Re b, Rba = Re ba, Ib = Im b, Iba = Im ba;
A21: Im (b-a) = Im b - Im a by COMPLEX1:19
.= Im b by A15;
then
A22: mb = sqrt(Rb^2+Ib^2) & mba = sqrt(Rba^2+Ib^2) by COMPLEX1:def 12;
A23: Rb^2 >= 0 & Ib^2 >= 0 by XREAL_1:63;
A24: Rba^2 >= 0 & Ib^2 >= 0 by XREAL_1:63;
Arg b in ].0,PI.[ by A17,XXREAL_1:4;
then
A25: Im b > 0 by Th16;
then
A26: mb >= 0 by COMPLEX1:4,47;
A27: mba >= 0 by A25,A21,COMPLEX1:4,47;
A28: sin BA > 0 by A25,A21,COMPTRIG:45;
A29: mb <> 0 by A25,COMPLEX1:4,47;
b = mb*cos B + mb*sin B *<i> & b = Re b+(Im b)*<i>
by COMPTRIG:62,COMPLEX1:13;
then Im b = mb*sin B by COMPLEX1:77;
then
A30: mba/mb = (sin B)/sin BA by A21,A20,A29,A28,XCMPLX_1:94;
per cases;
suppose
A31: 0 < Re ba;
then Rb^2 > Rba^2 by A19,A18,SQUARE_1:16;
then Rb^2 + Ib^2 > Rba^2 + Ib^2 by XREAL_1:8;
then mb > mba by A22,A24,SQUARE_1:27;
then mba/mb < 1 by A27,XREAL_1:189;
then ((sin B)/sin BA)*sin BA < 1*sin BA by A28,A30,XREAL_1:68;
then
A32: sin B < 1*sin BA by A28,XCMPLX_1:87;
B in ].0,PI/2.[ & BA in ].0,PI/2.[ by A25,A21,A19,A18,A31,COMPTRIG:41;
then BA > B by A32,Th6;
then BA+-B > B+-B by XREAL_1:8;
hence Arg ba - Arg b > 0;
end;
suppose
A33: 0 = Rba;
then ba = 0+Iba*<i> by COMPLEX1:13;
then
A34: BA = PI/2 by A25,A21,COMPTRIG:37;
B in ].0,PI/2.[ by A16,A25,A19,A33,COMPTRIG:41;
then B < BA by A34,XXREAL_1:4;
then B+-B < BA+-B by XREAL_1:8;
hence Arg ba - Arg(b) > 0;
end;
suppose
A35: 0 > Re ba;
thus Arg ba - Arg(b) > 0
proof
per cases;
suppose
0 < Re b;
then B in ].0,PI/2.[ by A25,COMPTRIG:41;
then
A36: B < PI/2 by XXREAL_1:4;
BA in ].PI/2,PI.[ by A25,A21,A35,COMPTRIG:42;
then BA > PI/2 by XXREAL_1:4;
then BA > B by A36,XXREAL_0:2;
then B+-B < BA+-B by XREAL_1:8;
hence thesis;
end;
suppose
0 = Re b;
then b = 0+Ib*<i> by COMPLEX1:13;
then
A37: B = PI/2 by A25,COMPTRIG:37;
BA in ].PI/2,PI.[ by A25,A21,A35,COMPTRIG:42;
then B < BA by A37,XXREAL_1:4;
then B+-B < BA+-B by XREAL_1:8;
hence thesis;
end;
suppose
A38: 0 > Re b;
then Rb^2 < Rba^2 by A19,A18,SQUARE_1:44;
then Rb^2 + Ib^2 < Rba^2 + Ib^2 by XREAL_1:8;
then mb < mba by A22,A23,SQUARE_1:27;
then mba/mb > 1 by A26,A29,XREAL_1:187;
then ((sin B)/sin BA)*sin BA > 1*sin BA by A28,A30,XREAL_1:68;
then
A39: sin B > 1*sin BA by A28,XCMPLX_1:87;
A40: B in ].PI/2,PI.[ by A25,A38,COMPTRIG:42;
BA in ].PI/2,PI.[ by A25,A21,A35,COMPTRIG:42;
then BA > B by A40,A39,Th7;
then BA+-B > B+-B by XREAL_1:8;
hence thesis;
end;
end;
end;
end;
then Arg(b-a)-Arg(b) > 0 by A1,A2,A3,A4;
then Arg(-(a-b))-Arg(b) > 0;
then Arg(a-b)-PI-Arg(b) > 0 by A8,A10,A11,Th12,COMPLEX1:4;
then
A41: Arg(a-b)-(Arg(b)+PI) > 0;
then Arg(a-b)-Arg(-b) > 0 by A4,A8,Th12,COMPLEX1:4;
then angle(0c,b,a) = Arg(a-b)-Arg(0c-b) by Def4;
hence
angle(a,0c,b)+angle(0c,b,a)+angle(b,a,0c) = Arg(b)-Arg(-b)-Arg(a)+Arg(a
-b)+(Arg(-a)-Arg(b-a)) by A7,A14
.= PI by A9,A6,A13;
Arg(a-b)-Arg(0c-b) > 0 by A4,A8,A41,Th12,COMPLEX1:4;
hence 0 < angle(0c,b,a) by Def4;
A42: Arg(a) >= 0 by COMPTRIG:34;
2*PI > 0+Arg(a-b) by COMPTRIG:34;
then
A43: 2*PI-Arg(a-b) > 0 by XREAL_1:20;
Arg(-a)-(Arg(a-b)-PI) = Arg(a)+(2*PI-Arg(a-b))by A6;
hence thesis by A14,A13,A43,A42;
end;
::$L https://en.wikipedia.org/wiki/Sum_of_angles_of_a_triangle Sum of angles of a triangle
theorem Th82:
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)
proof
assume that
A1: a <> b and
A2: b <> c and
A3: 0 < angle(a,b,c) and
A4: angle(a,b,c) < PI;
A5: c-b <> 0 by A2;
set r = -Arg (a+-b);
set A = Rotate(a+-b,r), B = Rotate(c+-b, r);
A6: Rotate(0c,r) = 0c by Th50;
A7: c+-b <> a+-b by A3,Th77;
A8: angle(b,c,a) = angle(b+-b,c+-b,a+-b) by Th70
.=angle(0c,B,A) by A6,A7,A5,Th76;
A9: angle(a+-b,0c,c+-b) = angle(a+-b,b+-b,c+-b) .= angle(a,b,c) by Th70;
A10: a-b <> 0 by A1;
then
A11: angle(a+-b,0c,c+-b) = angle(A,0c,B) by A6,A5,Th76;
a+-b <> 0c by A1;
then |.a+-b.| > 0 by COMPLEX1:47;
then
A12: Im A = 0 & Re A > 0 by COMPLEX1:12,SIN_COS:31;
then
A13: Arg A = 0c by Th19;
then Arg(B-0c)-Arg(A-0c)>= 0 by COMPTRIG:34;
then
A14: angle(a,b,c) = Arg B by A9,A11,A13,Def4;
A15: angle(c,a,b) = angle(c+-b,a+-b,b+-b) by Th70
.= angle(B,A,0c) by A6,A10,A7,Th76;
hence
angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI by A3,A4,A9,A11,A12,A14,A8,Lm5;
thus 0 < angle(b,c,a) by A3,A4,A12,A14,A8,Lm5;
thus thesis by A3,A4,A12,A14,A15,Lm5;
end;
theorem Th83:
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
proof
assume that
A1: a <> b & b <> c and
A2: angle(a,b,c) > PI;
A3: angle(c,b,a) < PI
proof
assume not thesis;
then angle(a,b,c) + angle(c,b,a) > PI+PI by A2,XREAL_1:8;
hence contradiction by A2,Th78,COMPTRIG:5;
end;
A4: angle(a,b,c) + angle(c,b,a)= 2*PI+0 by A2,Th78,COMPTRIG:5;
then
A5: angle(c,b,a) <> 0 by Th68;
A6: 0 <= angle(c,b,a) by Th68;
then angle(b,a,c) > 0 by A1,A5,A3,Th82;
then
A7: angle(c,a,b)+angle(b,a,c)=2*PI+0 by Th78;
angle(a,c,b) > 0 by A1,A6,A5,A3,Th82;
then angle(b,c,a) + angle(a,c,b)= 2*PI+0 by Th78;
then
angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = 2*PI+2*PI+2*PI - (angle(c,b,a)
+angle(b,a,c)+angle(a,c,b)) by A4,A7;
hence
A8: angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = 2*PI+2*PI+PI+PI-PI by A1,A6,A5,A3
,Th82
.= 5*PI;
A9: angle(a,b,c) < 2*PI by Th68;
angle(b,c,a) < 2*PI by Th68;
then
A10: 2*PI+2*PI+PI= 5*PI & angle(a,b,c)+angle(b,c,a) < 2*PI+2*PI by A9,XREAL_1:8
;
A11: 2*PI+PI+2*PI = 5*PI;
hereby
assume angle(b,c,a) <= PI;
then
A12: angle(a,b,c)+angle(b,c,a) < 2*PI+PI by A9,XREAL_1:8;
angle(c,a,b) < 2*PI by Th68;
hence contradiction by A8,A11,A12,XREAL_1:8;
end;
assume angle(c,a,b) <= PI;
hence contradiction by A8,A10,XREAL_1:8;
end;
Lm6: Im a = 0 & Re a > 0 & Arg(b) = PI implies angle(a,0,b)+angle(0,b,a)+angle
(b,a,0) = PI & 0 = angle(0,b,a) & 0 = angle(b,a,0)
proof
assume that
A1: Im a = 0 and
A2: Re a > 0 and
A3: Arg(b) = PI;
A4: Im (a-b) = Im a - Im b by COMPLEX1:19
.= - Im b by A1;
A5: Re b +0 < Re a by A2,A3,Th20;
then Re a - Re b > 0 by XREAL_1:20;
then
A6: Re (a-b) > 0 by COMPLEX1:19;
a = Re a + 0*<i> by A1,COMPLEX1:13;
then
A7: Arg(a) = 0 by A2,COMPTRIG:35;
then
A8: Arg(b-0c)-Arg(a-0c) > 0 by A3,COMPTRIG:5;
--(Re a - Re b) > 0 by A5,XREAL_1:20;
then Re b - Re a < 0;
then
A9: Re (b-a) < 0 by COMPLEX1:19;
A10: Im (b-a) = Im b - Im a by COMPLEX1:19
.= 0 by A1,A3,Th20;
then
A11: -Arg(b-a) = -PI by A9,Th20;
A12: Arg(b-a) = PI by A9,A10,Th20;
A13: Arg -b = Arg b -PI by A3,Lm1,Th12,COMPTRIG:5;
A14: Im b = 0 by A3,Th20;
then
A15: Arg(a-b) = 0 by A4,A6,Th19;
Arg(-a) = Arg(a)+PI by A2,A7,Th12,COMPLEX1:4,COMPTRIG:5
.= PI by A7;
then
A16: angle(b,a,0c) = Arg(0c-a)-Arg(b-a) by A11,Def4;
A17: Arg(a)-Arg(-a) = Arg(a)-(Arg(a)+PI) by A2,A7,Th12,COMPLEX1:4,COMPTRIG:5
.=-PI;
A18: Arg -b = Arg b -PI by A3,Lm1,Th12,COMPTRIG:5;
then
A19: Arg(a-b)-Arg(0c-b) = 0 by A3,A14,A4,A6,Th19;
then angle(0c,b,a) = Arg(a-b)-Arg(-b) by Def4;
hence
A20: angle(a,0,b)+angle(0,b,a)+angle(b,a,0) = Arg(b)-Arg(a)+(Arg(a-b)-
Arg(-b))+(Arg(0-a)-Arg(b-a)) by A8,A16,Def4
.= Arg(b)-Arg(-b)-Arg(a)+Arg(a-b)+(Arg(-a)-Arg(b-a))
.= PI by A15,A12,A13,A17;
Arg(a-b)+PI-Arg(b) = 0 by A3,A14,A4,A6,Th19;
then
A21: angle(0c,b,a) = Arg(a-b)-Arg(0c-b) by A18,Def4;
thus 0 = angle(0,b,a) by A19,Def4;
angle(a,0c,b) = Arg(b)-Arg(a) by A8,Def4;
hence thesis by A3,A7,A19,A21,A20,XCMPLX_1:3;
end;
theorem Th84:
a <> b & b <> c & angle(a,b,c) = PI implies angle(b,c,a) = 0 &
angle(c,a,b) = 0
proof
assume that
A1: a <> b and
A2: b <> c and
A3: angle(a,b,c) = PI;
A4: c-b <> 0 by A2;
set r = -Arg (a+-b);
set A = Rotate(a+-b,r), B = Rotate(c+-b, r);
A5: Rotate(0c,r) = 0c by Th50;
A6: angle(a+-b,0c,c+-b) = angle(a+-b,b+-b,c+-b) .= angle(a,b,c) by Th70;
A7: c+-b <> a+-b by A3,Th77,COMPTRIG:5;
A8: a-b <> 0 by A1;
then
A9: angle(a+-b,0c,c+-b) = angle(A,0c,B) by A5,A4,Th76;
a+-b <> 0c by A1;
then |.a+-b.| > 0 by COMPLEX1:47;
then
A10: Im A = 0 & Re A > 0 by COMPLEX1:12,SIN_COS:31;
then
A11: Arg A = 0c by Th19;
then Arg(B-0c)-Arg(A-0c)>=0 by COMPTRIG:34;
then
A12: angle(a,b,c) = Arg B by A6,A9,A11,Def4;
angle(b,c,a) = angle(b+-b,c+-b,a+-b) by Th70
.= angle(0c,B,A) by A5,A7,A4,Th76;
hence angle(b,c,a) = 0 by A3,A10,A12,Lm6;
angle(c,a,b) = angle(c+-b,a+-b,b+-b) by Th70
.=angle(B,A,0c) by A5,A8,A7,Th76;
hence thesis by A3,A10,A12,Lm6;
end;
theorem Th85:
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
proof
assume that
A1: a <> b and
A2: a <> c and
A3: b <> c and
A4: angle(a,b,c) = 0;
per cases by A1,A2,A3,A4,Th81;
suppose
A5: angle(b,c,a) <> 0;
A6: 0 <= angle(b,c,a) by Th68;
thus thesis
proof
per cases by XXREAL_0:1;
suppose
angle(b,c,a) < PI;
hence thesis by A2,A3,A4,A5,A6,Th82;
end;
suppose
angle(b,c,a) = PI;
hence thesis by A2,A3,Th84;
end;
suppose
angle(b,c,a) > PI;
hence thesis by A2,A3,A4,Th83,COMPTRIG:5;
end;
end;
end;
suppose
A7: angle(c,a,b) <> 0;
A8: 0 <= angle(c,a,b) by Th68;
thus thesis
proof
per cases by XXREAL_0:1;
suppose
angle(c,a,b) < PI;
hence thesis by A1,A2,A4,A7,A8,Th82;
end;
suppose
angle(c,a,b) = PI;
hence thesis by A1,A2,Th84;
end;
suppose
angle(c,a,b) > PI;
hence thesis by A1,A2,A4,Th83,COMPTRIG:5;
end;
end;
end;
end;
theorem
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
hereby
assume
A1: 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;
per cases by A1;
suppose
A2: angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI;
thus a <> b & a <> c & b <> c
proof
assume
A3: not (a <> b & a <> c & b <> c);
per cases by A3;
suppose
A4: a=b;
A5: angle(a,c,a) = 0 by Th77;
not (angle(a,a,c) = 0 & angle(c,a,a) = 0) by A2,A4,Th77,COMPTRIG:5;
hence contradiction by A2,A4,A5,Th78,COMPTRIG:5;
end;
suppose
A6: a=c;
A7: angle(a,b,a) = 0 by Th77;
not (angle(a,a,b) = 0 & angle(b,a,a) = 0) by A2,A6,Th77,COMPTRIG:5;
hence contradiction by A2,A6,A7,Th78,COMPTRIG:5;
end;
suppose
A8: b=c;
A9: angle(b,a,b) = 0 by Th77;
not (angle(a,b,b) = 0 & angle(b,b,a) = 0) by A2,A8,Th77,COMPTRIG:5;
hence contradiction by A2,A8,A9,Th78,COMPTRIG:5;
end;
end;
end;
suppose
A10: angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = 5*PI;
A11: (2+2)*PI < 5*PI by COMPTRIG:5,XREAL_1:68;
then
A12: 2*PI+2*PI < 5*PI;
thus a <> b & a <> c & b <> c
proof
assume
A13: not (a <> b & a <> c & b <> c);
per cases by A13;
suppose
a=b;
then angle(b,c,a) = 0 by Th77;
then
A14: angle(a,b,c)+angle(b,c,a) < 2*PI by Th68;
angle(c,a,b) < 2*PI by Th68;
hence contradiction by A10,A12,A14,XREAL_1:8;
end;
suppose
A15: b=c;
angle(a,b,c) < 2*PI & angle(b,c,a) < 2*PI by Th68;
then
A16: angle(a,b,c)+angle(b,c,a) < 2*PI+2*PI by XREAL_1:8;
angle(c,a,b) = 0 by A15,Th77;
hence contradiction by A10,A11,A16;
end;
suppose
a=c;
then angle(a,b,c) = 0 by Th77;
then
A17: angle(a,b,c)+angle(b,c,a) < 2*PI by Th68;
angle(c,a,b) < 2*PI by Th68;
hence contradiction by A10,A12,A17,XREAL_1:8;
end;
end;
end;
end;
assume that
A18: a <> b and
A19: a <> c and
A20: b <> c;
per cases by XXREAL_0:1;
suppose
A21: angle(a,b,c) = 0;
angle(b,c,a)+angle(c,a,b) = PI
proof
per cases by A18,A19,A20,A21,Th85;
suppose
angle(b,c,a) = 0 & angle(c,a,b) = PI;
hence thesis;
end;
suppose
angle(b,c,a) = PI & angle(c,a,b) = 0;
hence thesis;
end;
end;
hence thesis by A21;
end;
suppose
A22: 0 <> angle(a,b,c) & angle(a,b,c) < PI;
0 <= angle(a,b,c) by Th68;
hence thesis by A18,A20,A22,Th82;
end;
suppose
A23: 0 <> angle(a,b,c) & angle(a,b,c) = PI;
then angle(b,c,a) = 0 by A18,A20,Th84;
hence thesis by A18,A20,A23,Th84;
end;
suppose
0 <> angle(a,b,c) & angle(a,b,c) > PI;
hence thesis by A18,A20,Th83;
end;
end;