:: Inner Products and Angles of Complex Numbers :: by Wenpai Chang, Yatsuka Nakamura and Piotr Rudnicki :: :: Received May 29, 2003 :: Copyright (c) 2003-2021 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; begin theorem :: COMPLEX2:1 for a, b being Real st b > 0 ex r being Real st r = b*-[\ a/b /]+a & 0 <= r & r < b; theorem :: COMPLEX2:2 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; theorem :: COMPLEX2:3 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:4 for a being Real holds sin.(a-PI) = -sin.a & cos.(a-PI) = -cos. a; theorem :: COMPLEX2:5 for a being Real holds sin(a-PI) = -sin a & cos(a-PI) = - cos a; theorem :: COMPLEX2:6 for a, b being Real st a in ].0,PI/2.[ & b in ].0,PI/2.[ holds a < b iff sin a < sin b; theorem :: COMPLEX2:7 for a, b being Real st a in ].PI/2,PI.[ & b in ].PI/2,PI.[ holds a < b iff sin a > sin b; theorem :: COMPLEX2:8 for a being Real, i being Integer holds sin a = sin (2*PI* i+a); theorem :: COMPLEX2:9 for a being Real, i being Integer holds cos a = cos (2*PI *i+a); theorem :: COMPLEX2:10 for a being Real st sin a = 0 holds cos a <> 0; theorem :: COMPLEX2:11 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 ::$CT theorem :: COMPLEX2:13 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); ::$CT theorem :: COMPLEX2:15 for z being Complex holds Arg z = 0 iff z = |.z.|; theorem :: COMPLEX2:16 for z being Complex st z <> 0 holds Arg(z) < PI iff Arg - z >= PI; theorem :: COMPLEX2:17 for x, y being Complex st x <> y or x - y <> 0 holds Arg( x-y) < PI iff Arg(y-x) >= PI; theorem :: COMPLEX2:18 for z being Complex holds Arg z in ].0,PI.[ iff Im z > 0; theorem :: COMPLEX2:19 for z being Complex st Arg z <> 0 holds Arg z < PI iff sin Arg z> 0; theorem :: COMPLEX2:20 for x, y being Complex st Arg x < PI & Arg y < PI holds Arg(x+y ) < PI; theorem :: COMPLEX2:21 for z being Complex holds Arg z = 0 iff Re z >= 0 & Im z = 0; theorem :: COMPLEX2:22 for z being Complex holds Arg z = PI iff Re z < 0 & Im z= 0; theorem :: COMPLEX2:23 for z being Complex holds Im z = 0 iff Arg z = 0 or Arg z = PI; theorem :: COMPLEX2:24 for z being Complex st Arg z <= PI holds Im z >= 0; theorem :: COMPLEX2:25 for z being Element of COMPLEX st z <> 0 holds cos Arg -z = -cos Arg z & sin Arg -z = - sin Arg z; theorem :: COMPLEX2:26 for a being Complex st a <> 0 holds cos Arg a = Re a / |. a.| & sin Arg a = Im a / |.a.|; theorem :: COMPLEX2:27 for a being Complex, r being Real st r > 0 holds Arg(a*r) = Arg a; theorem :: COMPLEX2:28 for a being Complex, r being Real st r < 0 holds Arg(a*r) = Arg -a; begin :: Inner product definition let x, y be Complex; func x .|. y -> Element of COMPLEX equals :: COMPLEX2:def 1 x*(y*'); end; reserve a, b, c, d, x, y, z for Complex; theorem :: COMPLEX2:29 x.|.y = (Re x)*(Re y)+(Im x)*(Im y) + (-(Re x)*(Im y)+(Im x)*(Re y))*; theorem :: COMPLEX2:30 z.|.z = (Re z)*(Re z)+(Im z)*(Im z) & z.|.z = (Re z)^2+(Im z)^2; theorem :: COMPLEX2:31 z.|.z = |.z.|^2 & |.z.|^2 = Re (z.|.z); theorem :: COMPLEX2:32 |. x.|.y .| = |.x.|*|.y.|; theorem :: COMPLEX2:33 x.|.x = 0 implies x = 0; theorem :: COMPLEX2:34 y.|.x = (x.|.y)*'; theorem :: COMPLEX2:35 (x+y).|.z = x.|.z + y.|.z; theorem :: COMPLEX2:36 x.|.(y+z) = x.|.y + x.|.z; theorem :: COMPLEX2:37 (a*x).|.y = a * x.|.y; theorem :: COMPLEX2:38 x.|.(a*y) = (a*') * x.|.y; theorem :: COMPLEX2:39 (a*x).|.y = x.|.((a*')*y); theorem :: COMPLEX2:40 (a*x+b*y).|.z = a * x.|.z + b * y.|.z; theorem :: COMPLEX2:41 x.|.(a*y + b*z) = (a*') * x.|.y + (b*') * x.|.z; theorem :: COMPLEX2:42 (-x).|.y = x.|.(-y); theorem :: COMPLEX2:43 (-x).|.y = - x.|.y; theorem :: COMPLEX2:44 - x.|.y = x.|.(-y); theorem :: COMPLEX2:45 (-x).|.(-y) = x.|.y; theorem :: COMPLEX2:46 (x - y).|.z = x.|.z - y.|.z; theorem :: COMPLEX2:47 x.|.(y - z) = x.|.y - x.|.z; theorem :: COMPLEX2:48 (x + y).|.(x + y) = x.|.x + x.|.y + y.|.x + y.|.y; theorem :: COMPLEX2:49 (x-y).|.(x-y) = x.|.x - x.|.y - y.|.x + y.|.y; theorem :: COMPLEX2:50 Re (x.|.y) = 0 iff Im (x.|.y) = |.x.|*|.y.| or Im (x.|.y) = -|.x .|*|.y.|; begin :: Rotation definition let a be Complex, r be Real; func Rotate(a, r) -> Element of COMPLEX equals :: COMPLEX2:def 2 |.a.|*cos (r+Arg a) + |.a.|* sin (r+Arg a) *; end; reserve r for Real; theorem :: COMPLEX2:51 Rotate(a, 0) = a; theorem :: COMPLEX2:52 for a being Complex holds Rotate(a, r) = 0 iff a = 0; theorem :: COMPLEX2:53 for a being Complex holds |.Rotate(a,r).| = |.a.|; theorem :: COMPLEX2:54 for a being Complex st a <> 0 ex i being Integer st Arg( Rotate(a,r)) = 2*PI*i+(r+Arg(a)); theorem :: COMPLEX2:55 Rotate(a,-Arg a) = |.a.|; theorem :: COMPLEX2:56 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:57 Rotate(a+b,r) = Rotate(a,r)+Rotate(b,r); theorem :: COMPLEX2:58 Rotate(-a,r) = -Rotate(a,r); theorem :: COMPLEX2:59 Rotate(a-b,r) = Rotate(a,r)-Rotate(b,r); theorem :: COMPLEX2:60 Rotate(a, PI) = -a; begin :: Angles definition let a, b be Complex; func angle(a,b) -> Real equals :: COMPLEX2:def 3 Arg(Rotate(b, -Arg a)) if Arg a = 0 or b <> 0 otherwise 2*PI - Arg a; end; theorem :: COMPLEX2:61 for a being Complex holds r >= 0 implies angle(r,a) = Arg a; theorem :: COMPLEX2:62 for a,b being Complex holds Arg a = Arg b & a <> 0 & b <> 0 implies Arg Rotate(a,r) = Arg Rotate(b,r); theorem :: COMPLEX2:63 r > 0 implies angle(a,b) = angle(a*r,b*r); theorem :: COMPLEX2:64 a <> 0 & b <> 0 & Arg a = Arg b implies Arg -a = Arg -b; theorem :: COMPLEX2:65 a <> 0 & b <> 0 implies angle(a,b) = angle(Rotate(a,r),Rotate(b, r)); theorem :: COMPLEX2:66 r < 0 & a <> 0 & b <> 0 implies angle(a,b) = angle(a*r,b*r); theorem :: COMPLEX2:67 a <> 0 & b <> 0 implies angle(a,b) = angle(-a,-b); theorem :: COMPLEX2:68 b <> 0 & angle(a,b) = 0 implies angle(a,-b) = PI; theorem :: COMPLEX2:69 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 Complex; func angle(x,y,z) -> Real equals :: 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)); end; theorem :: COMPLEX2:70 0 <= angle(x,y,z) & angle(x,y,z) < 2*PI; theorem :: COMPLEX2:71 angle(x,y,z)=angle(x-y,0,z-y); theorem :: COMPLEX2:72 angle(a,b,c) = angle(a+d,b+d,c+d); theorem :: COMPLEX2:73 angle(a,b) = angle(a,0,b); theorem :: COMPLEX2:74 angle(x,y,z) = 0 implies Arg(x-y) = Arg(z-y) & angle(z,y,x)=0; theorem :: COMPLEX2:75 a <> 0 & b <> 0 implies (Re (a.|.b) = 0 iff angle(a,0,b) = PI/2 or angle(a,0,b) = 3/2*PI); theorem :: COMPLEX2:76 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); theorem :: COMPLEX2:77 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:78 a <> b & b <> c implies angle(a,b,c) = angle(Rotate(a,r), Rotate (b,r), Rotate(c,r)); theorem :: COMPLEX2:79 angle(a,b,a) = 0; theorem :: COMPLEX2:80 :: COMPLEX2:47, 48 angle(a,b,c) <> 0 iff angle(a,b,c)+angle(c,b,a) = 2*PI; theorem :: COMPLEX2:81 angle(a,b,c) <> 0 implies angle(c,b,a) <> 0; theorem :: COMPLEX2:82 angle(a,b,c) = PI implies angle(c,b,a) = PI; theorem :: COMPLEX2:83 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:84 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:85 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:86 a <> b & b <> c & angle(a,b,c) = PI implies angle(b,c,a) = 0 & angle(c,a,b) = 0; theorem :: COMPLEX2:87 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:88 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;