The abstract of the Mizar article:

Trigonometric Form of Complex Numbers

by

Robert Milewski

Received July 21, 2000

MML identifier: COMPTRIG

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, VECTSP_1, COMPLEX1, ARYTM_1, SQUARE_1, ABSVALUE,
      COMPLFLD, HAHNBAN1, GROUP_1, FUNCT_1, BINOP_1, POWER, RAT_1, PREPOWER,
      RCOMP_1, SIN_COS, ARYTM_3, RFUNCT_2, FDIFF_1, PRE_TOPC, BOOLE, RELAT_1,
      FCONT_1, PARTFUN1, COMPTRIG, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ORDINAL1, NUMBERS, ARYTM_0,
      XREAL_0, REAL_1, SQUARE_1, NAT_1, RAT_1, ABSVALUE, PREPOWER, POWER,
      RLVECT_1, VECTSP_1, BINOP_1, RELAT_1, FUNCT_1, RFUNCT_2, FCONT_1,
      FDIFF_1, SEQ_1, PARTFUN1, PARTFUN2, COMPLEX1, BINARITH, RCOMP_1, GROUP_1,
      SIN_COS, COMPLFLD, HAHNBAN1;
 constructors REAL_1, BINOP_1, TRIANG_1, SQUARE_1, PREPOWER, POWER, SEQ_1,
      RFUNCT_1, RFUNCT_2, FCONT_1, BINARITH, COMSEQ_3, GROUP_1, ALGSTR_2,
      RCOMP_1, VECTSP_2, FDIFF_1, PARTFUN2, COMPLSP1, SIN_COS, HAHNBAN1,
      COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4;
 clusters XREAL_0, STRUCT_0, RELSET_1, PARTFUN2, BINARITH, GROUP_1, GCD_1,
      COMPLFLD, POLYNOM2, MONOID_0, NAT_1, MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

  scheme Regr_without_0 { P[Nat] } :
   P[1]
  provided
    ex k be non empty Nat st P[k] and
    for k be non empty Nat st k <> 1 & P[k]
    ex n be non empty Nat st n < k & P[n];

canceled 2;

  theorem :: COMPTRIG:3
   for z be Element of COMPLEX holds
    Re z >= -|.z.|;

  theorem :: COMPTRIG:4
   for z be Element of COMPLEX holds
    Im z >= -|.z.|;

  theorem :: COMPTRIG:5
   for z be Element of F_Complex holds
    Re z >= -|.z.|;

  theorem :: COMPTRIG:6
     for z be Element of F_Complex holds
    Im z >= -|.z.|;

  theorem :: COMPTRIG:7
   for z be Element of F_Complex holds
    |.z.|^2 = (Re z)^2 + (Im z)^2;

  theorem :: COMPTRIG:8
   for x1,x2,y1,y2 be Real holds
    [**x1,x2**] = [**y1,y2**] implies x1 = y1 & x2 = y2;

  theorem :: COMPTRIG:9
   for z be Element of F_Complex holds
    z = [**Re z,Im z**];

  theorem :: COMPTRIG:10
   0.F_Complex = [**0,0**];

canceled;

  theorem :: COMPTRIG:12
   for L be unital (non empty HGrStr)
   for x be Element of L holds
    (power L).(x,1) = x;

  theorem :: COMPTRIG:13
     for L be unital (non empty HGrStr)
   for x be Element of L holds
    (power L).(x,2) = x*x;

  theorem :: COMPTRIG:14
   for L be add-associative right_zeroed right_complementable
            right-distributive unital (non empty doubleLoopStr)
   for n be Nat st n > 0 holds
    (power L).(0.L,n) = 0.L;

  theorem :: COMPTRIG:15
   for L be associative commutative unital (non empty HGrStr)
   for x,y be Element of L
   for n be Nat holds
    (power L).(x*y,n) = (power L).(x,n) * (power L).(y,n);

  theorem :: COMPTRIG:16
   for x be Real st x > 0
   for n be Nat holds
    (power F_Complex).([**x,0**],n) = [**x to_power n,0**];

  theorem :: COMPTRIG:17
   for x be real number
   for n be Nat st x >= 0 & n <> 0 holds
    (n-root x) to_power n = x;

begin

canceled 2;

  theorem :: COMPTRIG:20
   PI+PI/2 = 3/2*PI & 3/2*PI+PI/2 = 2*PI & 3/2*PI - PI = PI/2;

  theorem :: COMPTRIG:21
   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:22
   for a,b,c,x be real number st x in ].a,c.[ holds
    x in ].a,b.[ or x = b or x in ].b,c.[;

  theorem :: COMPTRIG:23
   for x be Real st x in ].0,PI.[ holds sin.x > 0;

  theorem :: COMPTRIG:24
   for x be real number st x in [.0,PI.] holds sin.x >= 0;

  theorem :: COMPTRIG:25
   for x be Real st x in ].PI,2*PI.[ holds sin.x < 0;

  theorem :: COMPTRIG:26
   for x be real number st x in [.PI,2*PI.] holds sin.x <= 0;

reserve x for Real;

  theorem :: COMPTRIG:27
   x in ].-PI/2,PI/2.[ implies cos.x > 0;

  theorem :: COMPTRIG:28
   for x be real number st x in [.-PI/2,PI/2.] holds cos.x >= 0;

  theorem :: COMPTRIG:29
   x in ].PI/2,3/2*PI.[ implies cos.x < 0;

  theorem :: COMPTRIG:30
   for x be real number st x in [.PI/2,3/2*PI.] holds cos.x <= 0;

  theorem :: COMPTRIG:31
   x in ].3/2*PI,2*PI.[ implies cos.x > 0;

  theorem :: COMPTRIG:32
   for x be real number st x in [.3/2*PI,2*PI.] holds cos.x >= 0;

  theorem :: COMPTRIG:33
   for x be real number st 0 <= x & x < 2*PI & sin x = 0 holds
    x = 0 or x = PI;

  theorem :: COMPTRIG:34
   for x be real number st 0 <= x & x < 2*PI & cos x = 0 holds
    x = PI/2 or x = 3/2*PI;

  theorem :: COMPTRIG:35
   sin is_increasing_on ].-PI/2,PI/2.[;

  theorem :: COMPTRIG:36
   sin is_decreasing_on ].PI/2,3/2*PI.[;

  theorem :: COMPTRIG:37
   cos is_decreasing_on ].0,PI.[;

  theorem :: COMPTRIG:38
   cos is_increasing_on ].PI,2*PI.[;

  theorem :: COMPTRIG:39
     sin is_increasing_on [.-PI/2,PI/2.];

  theorem :: COMPTRIG:40
     sin is_decreasing_on [.PI/2,3/2*PI.];

  theorem :: COMPTRIG:41
   cos is_decreasing_on [.0,PI.];

  theorem :: COMPTRIG:42
   cos is_increasing_on [.PI,2*PI.];

  theorem :: COMPTRIG:43
   sin is_continuous_on REAL &
   for x,y be real number holds
    sin is_continuous_on [.x,y.] & sin is_continuous_on ].x,y.[;

  theorem :: COMPTRIG:44
   cos is_continuous_on REAL &
   for x,y be real number holds
    cos is_continuous_on [.x,y.] & cos is_continuous_on ].x,y.[;

  theorem :: COMPTRIG:45
    sin.x in [.-1,1 .] & cos.x in [.-1,1 .];

  theorem :: COMPTRIG:46
     rng sin = [.-1,1 .];

  theorem :: COMPTRIG:47
     rng cos = [.-1,1 .];

  theorem :: COMPTRIG:48
     rng (sin|[.-PI/2,PI/2.]) = [.-1,1 .];

  theorem :: COMPTRIG:49
     rng (sin|[.PI/2,3/2*PI.]) = [.-1,1 .];

  theorem :: COMPTRIG:50
   rng (cos|[.0,PI.]) = [.-1,1 .];

  theorem :: COMPTRIG:51
   rng (cos|[.PI,2*PI.]) = [.-1,1 .];

begin  :: Argument of Complex Number

  definition
   let z be Element of F_Complex;
   func Arg z -> Real means
:: COMPTRIG:def 1
    z = [**|.z.|*cos it,|.z.|*sin it**] & 0 <= it & it < 2*PI
     if z <> 0.F_Complex
     otherwise it = 0;
  end;

  theorem :: COMPTRIG:52
   for z be Element of F_Complex holds
    0 <= Arg z & Arg z < 2*PI;

  theorem :: COMPTRIG:53
   for x be Real st x >= 0 holds
    Arg [**x,0**] = 0;

  theorem :: COMPTRIG:54
   for x be Real st x < 0 holds
    Arg [**x,0**] = PI;

  theorem :: COMPTRIG:55
   for x be Real st x > 0 holds
    Arg [**0,x**] = PI/2;

  theorem :: COMPTRIG:56
   for x be Real st x < 0 holds
    Arg [**0,x**] = 3/2*PI;

  theorem :: COMPTRIG:57
     Arg 1_(F_Complex) = 0;

  theorem :: COMPTRIG:58
     Arg i_FC = PI/2;

  theorem :: COMPTRIG:59
   for z be Element of F_Complex holds
    Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0;

  theorem :: COMPTRIG:60
   for z be Element of F_Complex holds
    Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0;

  theorem :: COMPTRIG:61
   for z be Element of F_Complex holds
    Arg z in ].PI,3/2*PI.[ iff Re z < 0 & Im z < 0;

  theorem :: COMPTRIG:62
   for z be Element of F_Complex holds
    Arg z in ].3/2*PI,2*PI.[ iff Re z > 0 & Im z < 0;

  theorem :: COMPTRIG:63
   for z be Element of F_Complex st Im z > 0 holds
    sin Arg z > 0;

  theorem :: COMPTRIG:64
   for z be Element of F_Complex st Im z < 0 holds
    sin Arg z < 0;

  theorem :: COMPTRIG:65
     for z be Element of F_Complex st Im z >= 0 holds
    sin Arg z >= 0;

  theorem :: COMPTRIG:66
     for z be Element of F_Complex st Im z <= 0 holds
    sin Arg z <= 0;

  theorem :: COMPTRIG:67
   for z be Element of F_Complex st Re z > 0 holds
    cos Arg z > 0;

  theorem :: COMPTRIG:68
   for z be Element of F_Complex st Re z < 0 holds
    cos Arg z < 0;

  theorem :: COMPTRIG:69
     for z be Element of F_Complex st Re z >= 0 holds
    cos Arg z >= 0;

  theorem :: COMPTRIG:70
     for z be Element of F_Complex st Re z <= 0 &
    z <> 0.F_Complex holds
    cos Arg z <= 0;

  theorem :: COMPTRIG:71
   for n be Nat holds
    (power F_Complex).([**cos x,sin x**],n) = [**cos (n*x),sin (n*x)**];

  theorem :: COMPTRIG:72
     for z be Element of F_Complex
   for n be Nat st z <> 0.F_Complex or n <> 0 holds
    (power F_Complex).(z,n) =
    [**(|.z.| to_power n)*cos (n*Arg z),(|.z.| to_power n)*sin (n*Arg z)**];

  theorem :: COMPTRIG:73
   for n,k be Nat st n <> 0 holds
    (power F_Complex).([**cos((x+2*PI*k)/n),sin((x+2*PI*k)/n)**],n) =
     [**cos x,sin x**];

  theorem :: COMPTRIG:74
   for z be Element of F_Complex
   for n,k be Nat st n <> 0 holds
    z = (power F_Complex).([**(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 Element of F_Complex;
   let n be non empty Nat;
   mode CRoot of n,x -> Element of F_Complex means
:: COMPTRIG:def 2
    (power F_Complex).(it,n) = x;
  end;

  theorem :: COMPTRIG:75
     for x be Element of F_Complex
   for n be non empty 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:76
     for x be Element of F_Complex
   for v be CRoot of 1,x holds
    v = x;

  theorem :: COMPTRIG:77
     for n be non empty Nat
   for v be CRoot of n,0.F_Complex holds
    v = 0.F_Complex;

  theorem :: COMPTRIG:78
     for n be non empty Nat
   for x be Element of F_Complex
   for v be CRoot of n,x st v = 0.F_Complex holds
    x = 0.F_Complex;