:: Trigonometric Form of Complex Numbers
::  by Robert Milewski
::
:: Received July 21, 2000
:: Copyright (c) 2000-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, 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, 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 * <i> & 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*<i>) = PI/2;

theorem :: COMPTRIG:38
  for x be Real st x < 0 holds Arg (x*<i>) = 3/2*PI;

theorem :: COMPTRIG:39
  Arg 1 = 0;

theorem :: COMPTRIG:40
  Arg <i> = 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)*<i>)|^n =
  cos (n*x)+sin (n*x)*<i>;

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)*<i>;

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)*<i>)|^n = (cos x+(sin x)*<i>);

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)*<i>)|^
  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)*
  <i> 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 * <i>;