:: Trigonometric Form of Complex Numbers :: by Robert Milewski :: :: Received July 21, 2000 :: Copyright (c) 2000-2018 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, NAT_1, XBOOLE_0, ARYTM_3, CARD_1, SUBSET_1, XXREAL_0, XCMPLX_0, COMPLEX1, ARYTM_1, RELAT_1, SQUARE_1, POWER, NEWTON, SIN_COS, XXREAL_1, FUNCT_1, ORDINAL2, REAL_1, FDIFF_1, RCOMP_1, VALUED_0, TARSKI, PARTFUN1, COMPTRIG; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, NAT_1, NEWTON, POWER, RELAT_1, FUNCT_1, RFUNCT_2, FCONT_1, FDIFF_1, PARTFUN1, PARTFUN2, RCOMP_1, SIN_COS, XXREAL_0; constructors PARTFUN1, ARYTM_0, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, FDIFF_1, COMSEQ_3, BINARITH, SIN_COS, BINOP_2, POWER, RVSUM_1, RELSET_1, ABIAN; registrations RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, NEWTON, SIN_COS, VALUED_0, FCONT_1, FUNCT_1, SQUARE_1, ORDINAL1, CARD_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin reserve x for Real; scheme :: COMPTRIG:sch 1 Regrwithout0 { P[Nat] } : P[1] provided ex k be non zero Nat st P[k] and for k be non zero Nat st k <> 1 & P[k] ex n be non zero Nat st n < k & P[n]; theorem :: COMPTRIG:1 for z be Complex holds Re z >= -|.z.|; theorem :: COMPTRIG:2 for z be Complex holds Im z >= -|.z.|; theorem :: COMPTRIG:3 for z be Complex holds |.z.|^2 = (Re z)^2 + (Im z)^2; theorem :: COMPTRIG:4 for n be Nat st x >= 0 & n <> 0 holds (n-root x) |^ n = x; registration cluster PI -> non negative; end; begin theorem :: COMPTRIG:5 0 < PI/2 & PI/2 < PI & 0 < PI & -PI/2 < PI/2 & PI < 2*PI & PI/2 < 3/2* PI & -PI/2 < 0 & 0 < 2*PI & PI < 3/2*PI & 3/2*PI < 2*PI & 0 < 3/2*PI; theorem :: COMPTRIG:6 for a,b,c,x be Real st x in ].a,c.[ holds x in ].a,b.[ or x = b or x in ].b,c.[; theorem :: COMPTRIG:7 x in ].0,PI.[ implies sin.x > 0; theorem :: COMPTRIG:8 x in [.0,PI.] implies sin.x >= 0; theorem :: COMPTRIG:9 x in ].PI,2*PI.[ implies sin.x < 0; theorem :: COMPTRIG:10 x in [.PI,2*PI.] implies sin.x <= 0; theorem :: COMPTRIG:11 x in ].-PI/2,PI/2.[ implies cos.x > 0; theorem :: COMPTRIG:12 x in [.-PI/2,PI/2.] implies cos.x >= 0; theorem :: COMPTRIG:13 x in ].PI/2,3/2*PI.[ implies cos.x < 0; theorem :: COMPTRIG:14 x in [.PI/2,3/2*PI.] implies cos.x <= 0; theorem :: COMPTRIG:15 x in ].3/2*PI,2*PI.[ implies cos.x > 0; theorem :: COMPTRIG:16 x in [.3/2*PI,2*PI.] implies cos.x >= 0; theorem :: COMPTRIG:17 0 <= x & x < 2*PI & sin x = 0 implies x = 0 or x = PI; theorem :: COMPTRIG:18 0 <= x & x < 2*PI & cos x = 0 implies x = PI/2 or x = 3/2*PI; theorem :: COMPTRIG:19 sin|].-PI/2,PI/2.[ is increasing; theorem :: COMPTRIG:20 sin|].PI/2,3/2*PI.[ is decreasing; theorem :: COMPTRIG:21 cos|].0,PI.[ is decreasing; theorem :: COMPTRIG:22 cos|].PI,2*PI.[ is increasing; theorem :: COMPTRIG:23 sin|[.-PI/2,PI/2.] is increasing; theorem :: COMPTRIG:24 sin|[.PI/2,3/2*PI.] is decreasing; theorem :: COMPTRIG:25 cos|[.0,PI.] is decreasing; theorem :: COMPTRIG:26 cos|[.PI,2*PI.] is increasing; theorem :: COMPTRIG:27 sin.x in [.-1,1 .] & cos.x in [.-1,1 .]; theorem :: COMPTRIG:28 rng sin = [.-1,1 .]; theorem :: COMPTRIG:29 rng cos = [.-1,1 .]; theorem :: COMPTRIG:30 rng (sin|[.-PI/2,PI/2.]) = [.-1,1 .]; theorem :: COMPTRIG:31 rng (sin|[.PI/2,3/2*PI.]) = [.-1,1 .]; theorem :: COMPTRIG:32 rng (cos|[.0,PI.]) = [.-1,1 .]; theorem :: COMPTRIG:33 rng (cos|[.PI,2*PI.]) = [.-1,1 .]; begin :: Argument of Complex Number definition let z be Complex; func Arg z -> Real means :: COMPTRIG:def 1 z = |.z.|*cos it + |.z.|*sin it * & 0 <= it & it < 2*PI if z <> 0 otherwise it = 0; end; theorem :: COMPTRIG:34 for z be Complex holds 0 <= Arg z & Arg z < 2*PI; theorem :: COMPTRIG:35 for x be Real st x >= 0 holds Arg x = 0; theorem :: COMPTRIG:36 for x be Real st x < 0 holds Arg x = PI; theorem :: COMPTRIG:37 for x be Real st x > 0 holds Arg (x*) = PI/2; theorem :: COMPTRIG:38 for x be Real st x < 0 holds Arg (x*) = 3/2*PI; theorem :: COMPTRIG:39 Arg 1 = 0; theorem :: COMPTRIG:40 Arg = PI/2; theorem :: COMPTRIG:41 for z be Complex holds Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0; theorem :: COMPTRIG:42 for z be Complex holds Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0; theorem :: COMPTRIG:43 for z be Complex holds Arg z in ].PI,3/2*PI.[ iff Re z < 0 & Im z < 0; theorem :: COMPTRIG:44 for z be Complex holds Arg z in ].3/2*PI,2*PI.[ iff Re z > 0 & Im z < 0; theorem :: COMPTRIG:45 for z be Complex st Im z > 0 holds sin Arg z > 0; theorem :: COMPTRIG:46 for z be Complex st Im z < 0 holds sin Arg z < 0; theorem :: COMPTRIG:47 for z be Complex st Im z >= 0 holds sin Arg z >= 0; theorem :: COMPTRIG:48 for z be Complex st Im z <= 0 holds sin Arg z <= 0; theorem :: COMPTRIG:49 for z be Complex st Re z > 0 holds cos Arg z > 0; theorem :: COMPTRIG:50 for z be Complex st Re z < 0 holds cos Arg z < 0; theorem :: COMPTRIG:51 for z be Complex st Re z >= 0 holds cos Arg z >= 0; theorem :: COMPTRIG:52 for z be Complex st Re z <= 0 & z <> 0 holds cos Arg z <= 0; theorem :: COMPTRIG:53 for x be Real, n be Nat holds (cos x+(sin x)*)|^n = cos (n*x)+sin (n*x)*; theorem :: COMPTRIG:54 for z be Element of COMPLEX for n be Nat st z <> 0 or n <> 0 holds z|^ n = (|.z.| |^ n)*cos (n*Arg z)+(|.z.| |^ n)*sin (n*Arg z)*; theorem :: COMPTRIG:55 for x be Real, n,k be Nat st n <> 0 holds (cos((x+2*PI*k)/n)+sin ((x+2*PI*k)/n)*)|^n = (cos x+(sin x)*); theorem :: COMPTRIG:56 for z be Complex for n,k be Nat st n <> 0 holds z = ((n -root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI*k)/n)*)|^ n; definition let x be Complex; let n be non zero Nat; mode CRoot of n,x -> Complex means :: COMPTRIG:def 2 it|^n = x; end; theorem :: COMPTRIG:57 for x be Element of COMPLEX for n be non zero Nat for k be Nat holds (n-root |. x .|)*cos((Arg x+2*PI*k)/n)+ (n-root |. x .|)*sin((Arg x+2*PI*k)/n)* is CRoot of n,x; theorem :: COMPTRIG:58 for x be Element of COMPLEX for v be CRoot of 1,x holds v = x; theorem :: COMPTRIG:59 for n be non zero Nat for v be CRoot of n,0 holds v = 0; theorem :: COMPTRIG:60 for n be non zero Nat for x be Element of COMPLEX for v be CRoot of n ,x st v = 0 holds x = 0; theorem :: COMPTRIG:61 for a being Real st 0 <= a & a < 2*PI & cos(a) = 1 holds a = 0; theorem :: COMPTRIG:62 for z being Complex holds z = |.z.|*cos Arg z + |.z.|*sin Arg z * ;