The Mizar article:

Trigonometric Form of Complex Numbers

by
Robert Milewski

Received July 21, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: COMPTRIG
[ 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;
 definitions RFUNCT_2;
 theorems AXIOMS, XREAL_0, REAL_1, REAL_2, NAT_1, SQUARE_1, PREPOWER, POWER,
      BINARITH, ABSVALUE, RELAT_1, FUNCT_1, RFUNCT_2, PARTFUN1, FCONT_1,
      FCONT_2, CARD_1, TOPREAL3, RLVECT_1, VECTSP_1, GROUP_1, RCOMP_1, FDIFF_1,
      ROLLE, COMPLEX1, SIN_COS, SIN_COS2, COMPLFLD, HAHNBAN1, POLYNOM2,
      TOPREAL5, JORDAN6, XBOOLE_0, XCMPLX_0, XCMPLX_1, ARYTM_0;
 schemes NAT_1;

begin

  scheme Regr_without_0 { P[Nat] } :
   P[1]
  provided
   A1: ex k be non empty Nat st P[k] and
   A2: for k be non empty Nat st k <> 1 & P[k]
    ex n be non empty Nat st n < k & P[n]
  proof
  defpred R[Nat] means P[$1+1];
   consider t be non empty Nat such that
    A3: P[t] by A1;
   consider s be Nat such that
    A4: t = s+1 by NAT_1:22;
   A5: ex k be Nat st R[k] by A3,A4;
   A6: now let k be Nat;
    assume that
     A7: k <> 0 and
     A8: R[k];
    reconsider k1=k+1 as non empty Nat;
      k > 0 by A7,NAT_1:19;
    then k+1 > 0+1 by REAL_1:53;
    then consider n be non empty Nat such that
     A9: n < k1 and
     A10: P[n] by A2,A8;
    consider l be Nat such that
     A11: n = l+1 by NAT_1:22;
    take l;
    thus l < k by A9,A11,AXIOMS:24;
    thus R[l] by A10,A11;
   end;
   R[0] from Regr(A5,A6);
   hence thesis;
  end;

canceled 2;

  theorem Th3:
   for z be Element of COMPLEX holds
    Re z >= -|.z.|
   proof
    let z be Element of COMPLEX;
      0 <= (Im z)^2 by SQUARE_1:72;
    then (Re z)^2+0 <= (Re z)^2 + (Im z)^2 by REAL_1:55;
    then 0 <= (Re z)^2 & (Re z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72;
    then sqrt(Re z)^2 <= sqrt((Re z)^2 + (Im z)^2) by SQUARE_1:94;
    then sqrt(Re z)^2 <= |.z.| by COMPLEX1:def 16;
    then -sqrt(Re z)^2 >= -|.z.| by REAL_1:50;
    then Re z >= -abs(Re z) & -abs(Re z) >= -|.z.| by ABSVALUE:11,SQUARE_1:91;
    hence thesis by AXIOMS:22;
   end;

  theorem Th4:
   for z be Element of COMPLEX holds
    Im z >= -|.z.|
   proof
    let z be Element of COMPLEX;
      0 <= (Re z)^2 by SQUARE_1:72;
    then (Im z)^2+0 <= (Re z)^2 + (Im z)^2 by REAL_1:55;
    then 0 <= (Im z)^2 & (Im z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72;
    then sqrt(Im z)^2 <= sqrt((Re z)^2 + (Im z)^2) by SQUARE_1:94;
    then sqrt(Im z)^2 <= |.z.| by COMPLEX1:def 16;
    then -sqrt(Im z)^2 >= -|.z.| by REAL_1:50;
    then Im z >= -abs(Im z) & -abs(Im z) >= -|.z.| by ABSVALUE:11,SQUARE_1:91;
    hence thesis by AXIOMS:22;
   end;

  theorem Th5:
   for z be Element of F_Complex holds
    Re z >= -|.z.|
   proof
    let z be Element of F_Complex;
    consider z1 be Element of COMPLEX such that
     A1: z = z1 and
     A2: Re z = Re z1 by HAHNBAN1:def 3;
    consider z2 be Element of COMPLEX such that
     A3: z = z2 and
     A4: |.z.| = |.z2.| by COMPLFLD:def 3;
    thus thesis by A1,A2,A3,A4,Th3;
   end;

  theorem
     for z be Element of F_Complex holds
    Im z >= -|.z.|
   proof
    let z be Element of F_Complex;
    consider z1 be Element of COMPLEX such that
     A1: z = z1 and
     A2: Im z = Im z1 by HAHNBAN1:def 4;
    consider z2 be Element of COMPLEX such that
     A3: z = z2 and
     A4: |.z.| = |.z2.| by COMPLFLD:def 3;
    thus thesis by A1,A2,A3,A4,Th4;
   end;

  theorem Th7:
   for z be Element of F_Complex holds
    |.z.|^2 = (Re z)^2 + (Im z)^2
   proof
    let z be Element of F_Complex;
    consider z1 be Element of COMPLEX such that
     A1: z = z1 and
     A2: Re z = Re z1 by HAHNBAN1:def 3;
    consider z2 be Element of COMPLEX such that
     A3: z = z2 and
     A4: Im z = Im z2 by HAHNBAN1:def 4;
    consider z3 be Element of COMPLEX such that
     A5: z = z3 and
     A6: |.z.| = |.z3.| by COMPLFLD:def 3;
    thus |.z.|^2 = |.z.|*|.z.| by SQUARE_1:def 3
       .= |.z3*z3.| by A6,COMPLEX1:151
       .= (Re z)^2 + (Im z)^2 by A1,A2,A3,A4,A5,COMPLEX1:154;
   end;

  theorem Th8:
   for x1,x2,y1,y2 be Real holds
    [**x1,x2**] = [**y1,y2**] implies x1 = y1 & x2 = y2
   proof
    let x1,x2,y1,y2 be Real;
    assume [**x1,x2**] = [**y1,y2**];
    then [*x1,x2*] = [**y1,y2**] by HAHNBAN1:def 1
       .= [*y1,y2*] by HAHNBAN1:def 1;
    hence thesis by ARYTM_0:12;
   end;

  theorem Th9:
   for z be Element of F_Complex holds
    z = [**Re z,Im z**]
   proof
    let z be Element of F_Complex;
    reconsider z1=z as Element of COMPLEX by COMPLFLD:def 1;
    thus z = [*Re z1,Im z1*] by COMPLEX1:8
       .= [**Re z1,Im z1**] by HAHNBAN1:def 1
       .= [**Re z,Im z1**] by HAHNBAN1:def 3
       .= [**Re z,Im z**] by HAHNBAN1:def 4;
   end;

L0: 0c = [*0,0*] by ARYTM_0:def 7,COMPLEX1:def 6;
L1: 1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7;

  theorem Th10:
   0.F_Complex = [**0,0**] by L0,COMPLFLD:9,HAHNBAN1:def 1;

 Lm1:
   0.F_Complex = the Zero of F_Complex by RLVECT_1:def 2;

canceled;

  theorem Th12:
   for L be unital (non empty HGrStr)
   for x be Element of L holds
    (power L).(x,1) = x
   proof
    let L be unital (non empty HGrStr);
    let x be Element of L;
      0+1 = 1;
    hence (power L).(x,1) = (power L).(x,0) * x by GROUP_1:def 7
       .= 1.L * x by GROUP_1:def 7
       .= x by GROUP_1:def 4;
   end;

  theorem
     for L be unital (non empty HGrStr)
   for x be Element of L holds
    (power L).(x,2) = x*x
   proof
    let L be unital (non empty HGrStr);
    let x be Element of L;
      1+1 = 2;
    hence (power L).(x,2) = (power L).(x,1) * x by GROUP_1:def 7
       .= x * x by Th12;
   end;

  theorem Th14:
   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
   proof
    let L be add-associative right_zeroed right_complementable
             right-distributive unital (non empty doubleLoopStr);
    let n be Nat;
    assume n > 0;
    then n >= 0+1 by NAT_1:38;
    then A1: n-1 >= 0 by REAL_1:84;
      n = n+-1+1 by XCMPLX_1:139
     .= n-1+1 by XCMPLX_0:def 8
     .= n-'1+1 by A1,BINARITH:def 3;
    hence (power L).(0.L,n) = (power L).(0.L,n-'1)*0.L by GROUP_1:def 7
       .= 0.L by VECTSP_1:36;
   end;

  theorem Th15:
   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)
   proof
    let L be associative commutative unital (non empty HGrStr);
    let x,y be Element of L;
    defpred P[Nat] means
     (power L).(x*y,$1) = (power L).(x,$1) * (power L).(y,$1);
    (power L).(x*y,0) = 1.L by GROUP_1:def 7
       .= 1.L * 1.L by GROUP_1:def 4
       .= (power L).(x,0) * 1.L by GROUP_1:def 7
       .= (power L).(x,0) * (power L).(y,0) by GROUP_1:def 7;
    then
    A1: P[0];
    A2: now let n be Nat;
     assume P[n];
     then (power L).(x*y,n+1) = (power L).(x,n) * (power L).(y,n) * (x*y) by
GROUP_1:def 7
        .= (power L).(x,n) * ((power L).(y,n) * (x*y)) by VECTSP_1:def 16
        .= (power L).(x,n) * (x*((power L).(y,n)*y)) by VECTSP_1:def 16
        .= (power L).(x,n) * (x*(power L).(y,n+1)) by GROUP_1:def 7
        .= (power L).(x,n)*x * (power L).(y,n+1) by VECTSP_1:def 16
        .= (power L).(x,n+1) * (power L).(y,n+1) by GROUP_1:def 7;
      hence P[n+1];
    end;
    thus for n be Nat holds P[n] from Ind(A1,A2);
   end;

  theorem Th16:
   for x be Real st x > 0
   for n be Nat holds
    (power F_Complex).([**x,0**],n) = [**x to_power n,0**]
   proof
    let x be Real;
    assume A1: x > 0;
    defpred P[Nat] means
      (power F_Complex).([**x,0**],$1) = [**x to_power $1,0**];
    (power F_Complex).([**x,0**],0) = 1.F_Complex by GROUP_1:def 7
       .= [*1,0*] by COMPLFLD:10,POLYNOM2:3,L1
       .= [**1,0**] by HAHNBAN1:def 1
       .= [**x to_power 0,0**] by POWER:29;
     then
A2:   P[0];
    A3: now let n be Nat;
     assume P[n];
     then (power F_Complex).([**x,0**],n+1) = [**x to_power n,0**]*[**x,0**]
                                                            by GROUP_1:def 7
        .= [**(x to_power n)*x-0*0,(x to_power n)*0+0*x**] by HAHNBAN1:11
        .= [**(x to_power n)*(x to_power 1),0**] by POWER:30
        .= [**x to_power (n+1),0**] by A1,POWER:32;
      hence P[n+1];
    end;
    thus for n be Nat holds P[n] from Ind(A2,A3);
   end;

  theorem Th17:
   for x be real number
   for n be Nat st x >= 0 & n <> 0 holds
    (n-root x) to_power n = x
   proof
    let x be real number;
    let n be Nat;
    assume that
     A1: x >= 0 and
     A2: n <> 0;
    A3: n > 0 by A2,NAT_1:19;
    then A4: n >= 0+1 by NAT_1:38;
    reconsider n1=n as Rational;
    per cases by A1;
     suppose A5: x > 0;
        n-root x = n -Root x by A1,A4,POWER:def 1;
      then A6: n-root x > 0 by A4,A5,PREPOWER:def 3;
      hence (n-root x) to_power n = (n-root x) #R n by POWER:def 2
         .= (n-root x) #Q n1 by A6,PREPOWER:88
         .= (n-root x) |^ n by A6,PREPOWER:60
         .= x by A1,A4,POWER:5;
     suppose A7: x = 0;
      hence (n-root x) to_power n = 0 to_power n by A4,POWER:6
         .= x by A3,A7,POWER:def 2;
   end;

begin

canceled 2;

  theorem Th20:
   PI+PI/2 = 3/2*PI & 3/2*PI+PI/2 = 2*PI & 3/2*PI - PI = PI/2
   proof
    thus PI+PI/2 = (2/2)*PI + 1*(PI/2)
       .= (2*PI)/2 + 1*(PI/2) by XCMPLX_1:75
       .= 2*(PI/2) + 1*(PI/2) by XCMPLX_1:75
       .= (2 + 1)*(PI/2) by XCMPLX_1:8
       .= (3*PI)/2 by XCMPLX_1:75
       .= 3/2*PI by XCMPLX_1:75;
    thus 3/2*PI + PI/2 = 3*PI/2 + 1*PI/2 by XCMPLX_1:75
       .= (3*PI+1*PI)/2 by XCMPLX_1:63
       .= ((3+1)*PI)/2 by XCMPLX_1:8
       .= 4/2*PI by XCMPLX_1:75
       .= 2*PI;
    thus 3/2*PI - PI = 3/2*PI - 2/2*PI
       .= (3/2 - 2/2)*PI by XCMPLX_1:40
       .= (3-2)/2*PI
       .= 1*PI/2 by XCMPLX_1:75
       .= PI/2;
   end;

  theorem Th21:
   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
   proof
    thus A1: 0 < PI/2
    proof
       PI in ].0, 4.[ by SIN_COS:def 30;
     then 0 < PI & PI < 4 by JORDAN6:45;
     then 0/2 < PI/2 by REAL_1:73;
     hence 0 < PI/2;
    end;
    thus A2: PI/2 < PI
    proof
       0 + PI/2 < PI/2 + PI/2 by A1,REAL_1:53;
     hence PI/2 < PI by XCMPLX_1:66;
    end;
    hence A3: 0 < PI by A1,AXIOMS:22;
    then A4: 0-PI/2 < PI-PI/2 by REAL_1:54;
      PI/2 + PI/2 = PI by XCMPLX_1:66;
    then PI - PI/2 = PI/2 by XCMPLX_1:26;
    hence -PI/2 < PI/2 by A4,XCMPLX_1:150;
      0 + PI < PI + PI by A3,REAL_1:53;
    hence A5: PI < 2*PI by XCMPLX_1:11;
      0+PI/2 < PI+PI/2 by A3,REAL_1:53;
    hence PI/2 < 3/2*PI by Th20;
      0 = -0;
    hence -PI/2 < 0 by A1,REAL_1:50;
    thus 0 < 2*PI by A1,A2,A5,AXIOMS:22;
      PI/2+PI/2 < PI+PI/2 by A2,REAL_1:53;
    hence A6: PI < 3/2*PI by Th20,XCMPLX_1:66;
    hence 3/2*PI < 2*PI by Th20,REAL_1:53;
    thus 0 < 3/2*PI by A1,A2,A6,AXIOMS:22;
   end;

  theorem Th22:
   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.[
   proof
    let a,b,c,x be real number;
    assume that
     A1: x in ].a,c.[ and
     A2: not x in ].a,b.[ and
     A3: not x = b;
    A4: a < x & x < c by A1,JORDAN6:45;
      x <= a or x >= b by A2,JORDAN6:45;
    then x > b by A1,A3,JORDAN6:45,REAL_1:def 5;
    hence x in ].b,c.[ by A4,JORDAN6:45;
   end;

  theorem Th23:
   for x be Real st x in ].0,PI.[ holds sin.x > 0
   proof
    let x be Real;
    assume A1: x in ].0,PI.[;
      PI/2 + PI/2 = PI by XCMPLX_1:66;
    then A2: PI - PI/2 = PI/2 by XCMPLX_1:26;
    per cases by A1,Th22;
     suppose x in ].0,PI/2.[;
      then 0 < x & x < PI/2 by JORDAN6:45;
      then 0-x < 0 & -x > -PI/2 by REAL_1:50,REAL_2:105;
      then -x < 0 & -x > -PI/2 by XCMPLX_1:150;
      then -x+PI/2 < 0+PI/2 & -x+PI/2 > -PI/2+PI/2 by REAL_1:53;
      then PI/2-x < PI/2 & PI/2+ -x > PI/2-PI/2 by XCMPLX_0:def 8;
      then PI/2-x < PI/2 & PI/2-x > PI/2-PI/2 by XCMPLX_0:def 8;
      then 0 < PI/2-x & PI/2-x < PI/2 by XCMPLX_1:14;
      then PI/2-x in ].0,PI/2.[ by JORDAN6:45;
      then cos.(PI/2-x) > 0 by SIN_COS:85;
      hence sin.x > 0 by SIN_COS:83;
     suppose x=PI/2;
      hence sin.x > 0 by SIN_COS:81;
     suppose x in ].PI/2,PI.[;
      then PI/2 < x & x < PI by JORDAN6:45;
      then PI/2-PI/2 < x-PI/2 & x-PI/2 < PI-PI/2 by REAL_1:54;
      then 0 < x-PI/2 & x-PI/2 < PI-PI/2 by XCMPLX_1:14;
      then x-PI/2 in ].0,PI/2.[ by A2,JORDAN6:45;
      then cos.(x-PI/2) > 0 by SIN_COS:85;
      then cos.(-(PI/2-x)) > 0 by XCMPLX_1:143;
      then cos.(PI/2-x) > 0 by SIN_COS:33;
      hence sin.x > 0 by SIN_COS:83;
   end;

  theorem Th24:
   for x be real number st x in [.0,PI.] holds sin.x >= 0
   proof
    let x be real number;
    assume x in [.0,PI.];
    then 0 <= x & x <= PI by TOPREAL5:1;
    then x = 0 or x = PI or (0 < x & x < PI) by REAL_1:def 5;
    then x = 0 or x = PI or x in ].0,PI.[ by JORDAN6:45;
    hence sin.x >= 0 by Th23,SIN_COS:33,81;
   end;

  theorem Th25:
   for x be Real st x in ].PI,2*PI.[ holds sin.x < 0
   proof
    let x be Real;
    assume x in ].PI,2*PI.[;
    then PI < x & x < 2*PI by JORDAN6:45;
    then PI-PI < x-PI & x-PI < 2*PI-PI by REAL_1:54;
    then 0 < x-PI & x-PI < 2*PI+-PI by XCMPLX_0:def 8,XCMPLX_1:14;
    then 0 < x-PI & x-PI < PI by XCMPLX_1:184;
    then A1: x-PI in ].0,PI.[ by JORDAN6:45;
      sin.(x-PI) = sin.(-(PI-x)) by XCMPLX_1:143
       .= -sin.(PI-x) by SIN_COS:33
       .= -sin.(PI+-x) by XCMPLX_0:def 8
       .= --sin.(-x) by SIN_COS:83
       .= -sin.x by SIN_COS:33;
    then -sin.x > 0 by A1,Th23;
    hence sin.x < 0 by REAL_1:66;
   end;

  theorem Th26:
   for x be real number st x in [.PI,2*PI.] holds sin.x <= 0
   proof
    let x be real number;
    assume x in [.PI,2*PI.];
    then PI <= x & x <= 2*PI by TOPREAL5:1;
    then x = PI or x = 2*PI or (PI < x & x < 2*PI) by REAL_1:def 5;
    then x = PI or x = 2*PI or x in ].PI,2*PI.[ by JORDAN6:45;
    hence sin.x <= 0 by Th25,SIN_COS:81;
   end;

reserve x for Real;

  theorem Th27:
   x in ].-PI/2,PI/2.[ implies cos.x > 0
   proof
    assume x in ].-PI/2,PI/2.[;
    then -PI/2 < x & x < PI/2 by JORDAN6:45;
    then -PI/2+PI/2 < x+PI/2 & x+PI/2 < PI/2+PI/2 by REAL_1:53;
    then 0 < x+PI/2 & x+PI/2 < PI by XCMPLX_0:def 6,XCMPLX_1:66;
    then A1: x+PI/2 in ].0,PI.[ by JORDAN6:45;
      sin.(x+PI/2) = cos.x by SIN_COS:83;
    hence cos.x > 0 by A1,Th23;
   end;

  theorem Th28:
   for x be real number st x in [.-PI/2,PI/2.] holds cos.x >= 0
   proof
    let x be real number;
    assume x in [.-PI/2,PI/2.];
    then -PI/2 <= x & x <= PI/2 by TOPREAL5:1;
    then x = -PI/2 or x = PI/2 or (-PI/2 < x & x < PI/2) by REAL_1:def 5;
    then x = -PI/2 or x = PI/2 or x in ].-PI/2,PI/2.[ by JORDAN6:45;
    hence cos.x >= 0 by Th27,SIN_COS:33,81;
   end;

  theorem Th29:
   x in ].PI/2,3/2*PI.[ implies cos.x < 0
   proof
    assume x in ].PI/2,3/2*PI.[;
    then PI/2 < x & x < 3/2*PI by JORDAN6:45;
    then PI/2+PI/2 < x+PI/2 & x+PI/2 < 3/2*PI+PI/2 by REAL_1:53;
    then PI < x+PI/2 & x+PI/2 < 3/2*PI+PI/2 by XCMPLX_1:66;
    then A1: x+PI/2 in ].PI,2*PI.[ by Th20,JORDAN6:45;
      sin.(x+PI/2) = cos.x by SIN_COS:83;
    hence cos.x < 0 by A1,Th25;
   end;

  theorem Th30:
   for x be real number st x in [.PI/2,3/2*PI.] holds cos.x <= 0
   proof
    let x be real number;
    assume x in [.PI/2,3/2*PI.];
    then PI/2 <= x & x <= 3/2*PI by TOPREAL5:1;
    then x = PI/2 or x = 3/2*PI or (PI/2 < x & x < 3/2*PI) by REAL_1:def 5;
    then x = PI/2 or x = 3/2*PI or x in ].PI/2,3/2*PI.[ by JORDAN6:45;
    hence cos.x <= 0 by Th20,Th29,SIN_COS:81;
   end;

  theorem Th31:
   x in ].3/2*PI,2*PI.[ implies cos.x > 0
   proof
    assume x in ].3/2*PI,2*PI.[;
    then 3/2*PI < x & x < 2*PI by JORDAN6:45;
    then 3/2*PI-PI < x-PI & x-PI < 2*PI-PI by REAL_1:54;
    then PI/2 < x-PI & x-PI < 2*PI+-PI by Th20,XCMPLX_0:def 8;
    then PI/2 < x-PI & x-PI < PI by XCMPLX_1:184;
    then PI/2 < x-PI & x-PI < 3/2*PI by Th21,AXIOMS:22;
    then A1: x-PI in ].PI/2,3/2*PI.[ by JORDAN6:45;
      cos.(x-PI) = cos.(-(PI-x)) by XCMPLX_1:143
       .= cos.(PI-x) by SIN_COS:33
       .= cos.(PI+-x) by XCMPLX_0:def 8
       .= -cos.(-x) by SIN_COS:83
       .= -cos.x by SIN_COS:33;
    then -cos.x < -0 by A1,Th29;
    hence cos.x > 0 by REAL_1:50;
   end;

  theorem Th32:
   for x be real number st x in [.3/2*PI,2*PI.] holds cos.x >= 0
   proof
    let x be real number;
    assume x in [.3/2*PI,2*PI.];
    then 3/2*PI <= x & x <= 2*PI by TOPREAL5:1;
    then x = 3/2*PI or x = 2*PI or (3/2*PI < x & x < 2*PI)
                                                            by REAL_1:def 5;
    then x = 3/2*PI or x = 2*PI or x in ].3/2*PI,2*PI.[ by JORDAN6:45;
    hence cos.x >= 0 by Th20,Th31,SIN_COS:81;
   end;

  theorem Th33:
   for x be real number st 0 <= x & x < 2*PI & sin x = 0 holds
    x = 0 or x = PI
   proof
    let x be real number;
    assume that
     A1: 0 <= x and
     A2: x < 2*PI and
     A3: sin x = 0;
      sin.x = 0 by A3,SIN_COS:def 21;
    then not x in ].0,PI.[ & not x in ].PI,2*PI.[ by Th23,Th25;
    then x = 0 or x >= PI & PI >= x by A1,A2,JORDAN6:45;
    hence x = 0 or x = PI by AXIOMS:21;
   end;

  theorem Th34:
   for x be real number st 0 <= x & x < 2*PI & cos x = 0 holds
    x = PI/2 or x = 3/2*PI
   proof
    let x be real number;
    assume that
     A1: 0 <= x and
     A2: x < 2*PI and
     A3: cos x = 0;
    A4: cos.x = 0 by A3,SIN_COS:def 23;
    then not x in ].-PI/2,PI/2.[ & not x in ].PI/2,3/2*PI.[ by Th27,Th29;
    then (-PI/2 >= x or x >= PI/2) & (PI/2 >= x or x >= 3/2*PI) by JORDAN6:45;
    then x = PI/2 or x = 3/2*PI or x > 3/2* PI
                                          by A1,Th21,REAL_1:def 5;
    then x = PI/2 or x = 3/2*PI or x in ].3/2* PI,2*PI.[ by A2,JORDAN6:45;
    hence x = PI/2 or x = 3/2*PI by A4,Th31;
   end;

  theorem Th35:
   sin is_increasing_on ].-PI/2,PI/2.[
   proof
    A1: sin is_differentiable_on ].-PI/2,PI/2.[
    proof
       ].-PI/2,PI/2.[ is open by RCOMP_1:25;
     hence sin is_differentiable_on ].-PI/2,PI/2.[ by FDIFF_1:34,SIN_COS:73;
    end;
      for x be Real st x in ].-PI/2,PI/2.[ holds diff(sin,x) > 0
    proof
     let x be Real;
     assume x in ].-PI/2,PI/2.[;
     then 0 < cos.x by Th27;
     hence diff(sin,x) > 0 by SIN_COS:73;
    end;
    hence thesis by A1,Th21,ROLLE:9;
   end;

  theorem Th36:
   sin is_decreasing_on ].PI/2,3/2*PI.[
   proof
    A1: sin is_differentiable_on ].PI/2,3/2*PI.[
    proof
       ].PI/2,3/2*PI.[ is open by RCOMP_1:25;
     hence sin is_differentiable_on ].PI/2,3/2*PI.[ by FDIFF_1:34,SIN_COS:73;
    end;
      for x be Real st x in ].PI/2,3/2*PI.[ holds diff(sin,x) < 0
    proof
     let x be Real;
     assume x in ].PI/2,3/2*PI.[;
     then 0 > cos.x by Th29;
     hence diff(sin,x) < 0 by SIN_COS:73;
    end;
    hence thesis by A1,Th21,ROLLE:10;
   end;

  theorem Th37:
   cos is_decreasing_on ].0,PI.[
   proof
    A1: cos is_differentiable_on ].0,PI.[
    proof
       ].0,PI.[ is open by RCOMP_1:25;
     hence cos is_differentiable_on ].0,PI.[ by FDIFF_1:34,SIN_COS:72;
    end;
      for x be Real st x in ].0,PI.[ holds diff(cos,x) < 0
    proof
     let x be Real;
     assume A2: x in ].0,PI.[;
     A3: diff(cos,x) = -sin.x by SIN_COS:72;
       0 < sin.x by A2,Th23;
     then 0-sin.x < 0 by REAL_2:105;
     hence diff(cos,x) < 0 by A3,XCMPLX_1:150;
    end;
    hence thesis by A1,Th21,ROLLE:10;
   end;

  theorem Th38:
   cos is_increasing_on ].PI,2*PI.[
   proof
    A1: cos is_differentiable_on ].PI,2*PI.[
    proof
       ].PI,2*PI.[ is open by RCOMP_1:25;
     hence cos is_differentiable_on ].PI,2*PI.[ by FDIFF_1:34,SIN_COS:72;
    end;
      for x be Real st x in ].PI,2*PI.[ holds diff(cos,x) > 0
    proof
     let x be Real;
     assume A2: x in ].PI,2*PI.[;
     A3: diff(cos,x) = -sin.x by SIN_COS:72;
       0 > sin.x by A2,Th25;
     then 0-sin.x > 0 by SQUARE_1:11;
     hence diff(cos,x) > 0 by A3,XCMPLX_1:150;
    end;
    hence thesis by A1,Th21,ROLLE:9;
   end;

  theorem
     sin is_increasing_on [.-PI/2,PI/2.]
   proof
    let r1,r2 be Real;
    assume that
     A1: r1 in [.-PI/2,PI/2.] /\ dom sin and
     A2: r2 in [.-PI/2,PI/2.] /\ dom sin and
     A3: r1 < r2;
    A4: r1 in [.-PI/2,PI/2.] & r1 in dom sin &
     r2 in [.-PI/2,PI/2.] & r2 in dom sin by A1,A2,XBOOLE_0:def 3;
    then A5: -PI/2 <= r1 & r1 <= PI/2 & -PI/2 <= r2 & r2 <= PI/2 by TOPREAL5:1;
    set r3 = (r1+r2)/2;
      abs(sin r3 ) <= 1 by SIN_COS:30;
    then abs(sin.r3 ) <= 1 by SIN_COS:def 21;
    then A6: sin.r3 >= -1 & sin.r3 <= 1 by ABSVALUE:12;
      abs(sin r2 ) <= 1 by SIN_COS:30;
    then abs(sin.r2 ) <= 1 by SIN_COS:def 21;
    then A7: sin.r2 >= -1 by ABSVALUE:12;
    A8: r1 < r3 & r3 < r2 by A3,TOPREAL3:3;
    then -PI/2 < r3 & r3 < PI/2 by A5,AXIOMS:22;
    then r3 in ].-PI/2,PI/2.[ & r3 in dom sin by JORDAN6:45,SIN_COS:27;
    then A9: r3 in ].-PI/2,PI/2.[ /\ dom sin by XBOOLE_0:def 3;
      now per cases by A5,REAL_1:def 5;
     suppose A10: -PI/2 < r1;
      then A11: -PI/2 < r2 by A3,AXIOMS:22;
        now per cases by A5,REAL_1:def 5;
       suppose A12: r2 < PI/2;
        then r1 < PI/2 by A3,AXIOMS:22;
        then r1 in ].-PI/2,PI/2.[ & r2 in ].-PI/2,PI/2.[
        by A10,A11,A12,JORDAN6:45;
        then r1 in ].-PI/2,PI/2.[ /\ dom sin & r2 in ].-PI/2,PI/2.[
        /\ dom sin by A4,XBOOLE_0:def 3;
        hence sin.r2 > sin.r1 by A3,Th35,RFUNCT_2:def 2;
       suppose A13: r2 = PI/2;
        then r1 in ].-PI/2,PI/2.[ by A3,A10,JORDAN6:45;
        then r1 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 3;
        then A14: sin.r3 > sin.r1 by A8,A9,Th35,RFUNCT_2:def 2;
        assume sin.r2 <= sin.r1;
        hence contradiction by A6,A13,A14,AXIOMS:22,SIN_COS:81;
      end;
      hence sin.r2 > sin.r1;
     suppose A15: -PI/2 = r1;
        now per cases by A5,REAL_1:def 5;
       suppose r2 < PI/2;
        then r2 in ].-PI/2,PI/2.[ by A3,A15,JORDAN6:45;
        then r2 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 3;
        then A16: sin.r2 > sin.r3 by A8,A9,Th35,RFUNCT_2:def 2;
        assume sin.r2 <= sin.r1;
        then sin.r2 <= -1 by A15,SIN_COS:33,81;
        hence contradiction by A6,A7,A16,AXIOMS:21;
       suppose r2 = PI/2;
        then sin.r2 = 1 & sin.r1 = -1 by A15,SIN_COS:33,81;
        hence sin.r2 > sin.r1;
      end;
      hence sin.r2 > sin.r1;
    end;
    hence sin.r2 > sin.r1;
   end;

  theorem
     sin is_decreasing_on [.PI/2,3/2*PI.]
   proof
    let r1,r2 be Real;
    assume that
     A1: r1 in [.PI/2,3/2*PI.] /\ dom sin and
     A2: r2 in [.PI/2,3/2*PI.] /\ dom sin and
     A3: r1 < r2;
    A4: r1 in [.PI/2,3/2*PI.] & r1 in dom sin &
     r2 in [.PI/2,3/2*PI.] & r2 in dom sin by A1,A2,XBOOLE_0:def 3;
    then A5: PI/2 <= r1 & r1 <= 3/2*PI & PI/2 <= r2 & r2 <= 3/2*PI by TOPREAL5:
1;
      abs(sin r1 ) <= 1 by SIN_COS:30;
    then abs(sin.r1 ) <= 1 by SIN_COS:def 21;
    then A6: sin.r1 >= -1 by ABSVALUE:12;
    set r3 = (r1+r2)/2;
      abs(sin r3 ) <= 1 by SIN_COS:30;
    then abs(sin.r3 ) <= 1 by SIN_COS:def 21;
    then A7: sin.r3 >= -1 & sin.r3 <= 1 by ABSVALUE:12;
      abs(sin r2 ) <= 1 by SIN_COS:30;
    then abs(sin.r2 ) <= 1 by SIN_COS:def 21;
    then A8: sin.r2 <= 1 by ABSVALUE:12;
    A9: r1 < r3 & r3 < r2 by A3,TOPREAL3:3;
    then PI/2 < r3 & r3 < 3/2*PI by A5,AXIOMS:22;
    then r3 in ].PI/2,3/2*PI.[ & r3 in dom sin by JORDAN6:45,SIN_COS:27;
    then A10: r3 in ].PI/2,3/2*PI.[ /\ dom sin by XBOOLE_0:def 3;
      now per cases by A5,REAL_1:def 5;
     suppose A11: PI/2 < r1;
      then A12: PI/2 < r2 by A3,AXIOMS:22;
        now per cases by A5,REAL_1:def 5;
       suppose A13: r2 < 3/2*PI;
        then r1 < 3/2*PI by A3,AXIOMS:22;
        then r1 in ].PI/2,3/2*PI.[ & r2 in
 ].PI/2,3/2*PI.[ by A11,A12,A13,JORDAN6:45;
        then r1 in ].PI/2,3/2*PI.[ /\ dom sin &
         r2 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3;
        hence sin.r2 < sin.r1 by A3,Th36,RFUNCT_2:def 3;
       suppose A14: r2 = 3/2*PI;
        then r1 in ].PI/2,3/2*PI.[ by A3,A11,JORDAN6:45;
        then r1 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3;
        then A15: sin.r3 < sin.r1 by A9,A10,Th36,RFUNCT_2:def 3;
        assume sin.r2 >= sin.r1;
        hence contradiction by A6,A7,A14,A15,Th20,AXIOMS:21,SIN_COS:81;
      end;
      hence sin.r2 < sin.r1;
     suppose A16: PI/2 = r1;
        now per cases by A5,REAL_1:def 5;
       suppose r2 < 3/2*PI;
        then r2 in ].PI/2,3/2*PI.[ by A3,A16,JORDAN6:45;
        then r2 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3;
        then A17: sin.r2 < sin.r3 by A9,A10,Th36,RFUNCT_2:def 3;
        assume sin.r2 >= sin.r1;
        hence contradiction by A7,A8,A16,A17,AXIOMS:21,SIN_COS:81;
       suppose r2 = 3/2*PI;
        hence sin.r2 < sin.r1 by A16,Th20,SIN_COS:81;
      end;
      hence sin.r2 < sin.r1;
    end;
    hence sin.r2 < sin.r1;
   end;

  theorem Th41:
   cos is_decreasing_on [.0,PI.]
   proof
    let r1,r2 be Real;
    assume that
     A1: r1 in [.0,PI.] /\ dom cos and
     A2: r2 in [.0,PI.] /\ dom cos and
     A3: r1 < r2;
    A4: r1 in [.0,PI.] & r1 in dom cos & r2 in [.0,PI.] & r2 in dom cos
                                                       by A1,A2,XBOOLE_0:def 3;
    then A5: 0 <= r1 & r1 <= PI & 0 <= r2 & r2 <= PI by TOPREAL5:1;
      abs(cos r1) <= 1 by SIN_COS:30;
    then abs(cos.r1) <= 1 by SIN_COS:def 23;
    then A6: cos.r1 >= -1 by ABSVALUE:12;
    set r3 = (r1+r2)/2;
      abs(cos r3) <= 1 by SIN_COS:30;
    then abs(cos.r3) <= 1 by SIN_COS:def 23;
    then A7: cos.r3 >= -1 & cos.r3 <= 1 by ABSVALUE:12;
      abs(cos r2) <= 1 by SIN_COS:30;
    then abs(cos.r2) <= 1 by SIN_COS:def 23;
    then A8: cos.r2 <= 1 by ABSVALUE:12;
    A9: r1 < r3 & r3 < r2 by A3,TOPREAL3:3;
    then 0 < r3 & r3 < PI by A5,AXIOMS:22;
    then r3 in ].0,PI.[ & r3 in dom cos by JORDAN6:45,SIN_COS:27;
    then A10: r3 in ].0,PI.[ /\ dom cos by XBOOLE_0:def 3;
      now per cases by A4,TOPREAL5:1;
     suppose A11: 0 < r1;
      then A12: 0 < r2 by A3,AXIOMS:22;
        now per cases by A5,REAL_1:def 5;
       suppose A13: r2 < PI;
        then r1 < PI by A3,AXIOMS:22;
        then r1 in ].0,PI.[ & r2 in ].0,PI.[ by A11,A12,A13,JORDAN6:45;
        then r1 in ].0,PI.[ /\ dom cos & r2 in ].0,PI.[ /\ dom cos
                                                          by A4,XBOOLE_0:def 3;
        hence cos.r2 < cos.r1 by A3,Th37,RFUNCT_2:def 3;
       suppose A14: r2 = PI;
        then r1 in ].0,PI.[ by A3,A11,JORDAN6:45;
        then r1 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 3;
        then A15: cos.r3 < cos.r1 by A9,A10,Th37,RFUNCT_2:def 3;
        assume cos.r2 >= cos.r1;
        hence contradiction by A6,A7,A14,A15,AXIOMS:21,SIN_COS:81;
      end;
      hence cos.r2 < cos.r1;
     suppose A16: 0 = r1;
        now per cases by A5,REAL_1:def 5;
       suppose r2 < PI;
        then r2 in ].0,PI.[ by A3,A16,JORDAN6:45;
        then r2 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 3;
        then A17: cos.r2 < cos.r3 by A9,A10,Th37,RFUNCT_2:def 3;
        assume cos.r2 >= cos.r1;
        hence contradiction by A7,A8,A16,A17,AXIOMS:21,SIN_COS:33;
       suppose r2 = PI;
        hence cos.r2 < cos.r1 by A16,SIN_COS:33,81;
      end;
      hence cos.r2 < cos.r1;
    end;
    hence cos.r2 < cos.r1;
   end;

  theorem Th42:
   cos is_increasing_on [.PI,2*PI.]
   proof
    let r1,r2 be Real;
    assume that
     A1: r1 in [.PI,2*PI.] /\ dom cos and
     A2: r2 in [.PI,2*PI.] /\ dom cos and
     A3: r1 < r2;
    A4: r1 in [.PI,2*PI.] & r1 in dom cos & r2 in [.PI,2*PI.] & r2 in
 dom cos by A1,A2,XBOOLE_0:def 3;
    then A5: PI <= r1 & r1 <= 2*PI & PI <= r2 & r2 <= 2*PI by TOPREAL5:1;
    set r3 = (r1+r2)/2;
      abs(cos r3 ) <= 1 by SIN_COS:30;
    then abs(cos.r3 ) <= 1 by SIN_COS:def 23;
    then A6: cos.r3 >= -1 & cos.r3 <= 1 by ABSVALUE:12;
      abs(cos r2 ) <= 1 by SIN_COS:30;
    then abs(cos.r2 ) <= 1 by SIN_COS:def 23;
    then A7: cos.r2 >= -1 by ABSVALUE:12;
    A8: r1 < r3 & r3 < r2 by A3,TOPREAL3:3;
    then PI < r3 & r3 < 2*PI by A5,AXIOMS:22;
    then r3 in ].PI,2*PI.[ & r3 in dom cos by JORDAN6:45,SIN_COS:27;
    then A9: r3 in ].PI,2*PI.[ /\ dom cos by XBOOLE_0:def 3;
      now per cases by A5,REAL_1:def 5;
     suppose A10: PI < r1;
      then A11: PI < r2 by A3,AXIOMS:22;
        now per cases by A5,REAL_1:def 5;
       suppose A12: r2 < 2*PI;
        then r1 < 2*PI by A3,AXIOMS:22;
        then r1 in ].PI,2*PI.[ & r2 in ].PI,2*PI.[ by A10,A11,A12,JORDAN6:45;
        then r1 in ].PI,2*PI.[ /\ dom cos & r2 in ].PI,2*PI.[ /\ dom cos
                                                          by A4,XBOOLE_0:def 3;
        hence cos.r2 > cos.r1 by A3,Th38,RFUNCT_2:def 2;
       suppose A13: r2 = 2*PI;
        then r1 in ].PI,2*PI.[ by A3,A10,JORDAN6:45;
        then r1 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 3;
        then A14: cos.r3 > cos.r1 by A8,A9,Th38,RFUNCT_2:def 2;
        assume cos.r2 <= cos.r1;
        hence contradiction by A6,A13,A14,AXIOMS:22,SIN_COS:81;
      end;
      hence cos.r2 > cos.r1;
     suppose A15: PI = r1;
        now per cases by A5,REAL_1:def 5;
       suppose r2 < 2*PI;
        then r2 in ].PI,2*PI.[ by A3,A15,JORDAN6:45;
        then r2 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 3;
        then A16: cos.r2 > cos.r3 by A8,A9,Th38,RFUNCT_2:def 2;
        assume cos.r2 <= cos.r1;
        hence contradiction by A6,A7,A15,A16,AXIOMS:21,SIN_COS:81;
       suppose r2 = 2*PI;
        hence cos.r2 > cos.r1 by A15,SIN_COS:81;
      end;
      hence cos.r2 > cos.r1;
    end;
    hence cos.r2 > cos.r1;
   end;

  theorem Th43:
   sin is_continuous_on REAL &
   for x,y be real number holds
    sin is_continuous_on [.x,y.] & sin is_continuous_on ].x,y.[
   proof
    thus A1: sin is_continuous_on REAL by FDIFF_1:33,SIN_COS:73;
    let x,y be real number;
    thus thesis by A1,FCONT_1:17;
   end;

  theorem Th44:
   cos is_continuous_on REAL &
   for x,y be real number holds
    cos is_continuous_on [.x,y.] & cos is_continuous_on ].x,y.[
   proof
    thus A1: cos is_continuous_on REAL by FDIFF_1:33,SIN_COS:72;
    let x,y be real number;
    thus thesis by A1,FCONT_1:17;
   end;

  theorem Th45:
    sin.x in [.-1,1 .] & cos.x in [.-1,1 .]
   proof
      abs(sin x) <= 1 & abs(cos x) <= 1 by SIN_COS:30;
    then abs(sin.x) <= 1 & abs(cos.x) <= 1 by SIN_COS:def 21,def 23;
    then -1 <= sin.x & sin.x <= 1 & -1 <= cos.x & cos.x <= 1 by ABSVALUE:12;
    hence thesis by TOPREAL5:1;
   end;

  theorem
     rng sin = [.-1,1 .]
   proof
      now let y be set;
     thus y in [.-1,1 .] implies ex x be set st x in dom sin & y = sin.x
     proof
      assume A1: y in [.-1,1 .];
      then reconsider y1=y as Real;
      A2: sin is_continuous_on [.-PI/2,PI/2 .] by Th43;
        y1 in [.-1,1 .] \/ [.1,sin.(-PI/2).] by A1,XBOOLE_0:def 2;
      then y1 in [.sin.(-PI/2),sin.(PI/2).] \/ [.sin.(PI/2),sin.(-PI/2).]
                                                            by SIN_COS:33,81;
      then consider x be Real such that
         x in [.-PI/2,PI/2 .] and
       A3: y1 = sin.x by A2,Th21,FCONT_2:16;
      take x;
        x in REAL;
      hence x in dom sin & y = sin.x by A3,SIN_COS:def 20;
     end;
     thus (ex x be set st x in dom sin & y = sin.x) implies y in [.-1,1 .]
     proof
      given x be set such that
       A4: x in dom sin and
       A5: y = sin.x;
      reconsider x1=x as Real by A4,SIN_COS:def 20;
        y = sin.x1 by A5;
      hence y in [.-1,1 .] by Th45;
     end;
    end;
    hence thesis by FUNCT_1:def 5;
   end;

  theorem
     rng cos = [.-1,1 .]
   proof
      now let y be set;
     thus y in [.-1,1 .] implies ex x be set st x in dom cos & y = cos.x
     proof
      assume A1: y in [.-1,1 .];
      then reconsider y1=y as Real;
      A2: cos is_continuous_on [.0,PI.] by Th44;
        y1 in [.cos.0,cos.PI.] \/ [.cos.PI,cos.0 .]
                                            by A1,SIN_COS:33,81,XBOOLE_0:def 2;
      then consider x be Real such that
         x in [.0,PI.] and
       A3: y1 = cos.x by A2,Th21,FCONT_2:16;
      take x;
        x in REAL;
      hence x in dom cos & y = cos.x by A3,SIN_COS:def 22;
     end;
     thus (ex x be set st x in dom cos & y = cos.x) implies y in [.-1,1 .]
     proof
      given x be set such that
       A4: x in dom cos and
       A5: y = cos.x;
      reconsider x1=x as Real by A4,SIN_COS:def 22;
        y = cos.x1 by A5;
      hence y in [.-1,1 .] by Th45;
     end;
    end;
    hence thesis by FUNCT_1:def 5;
   end;

  theorem
     rng (sin|[.-PI/2,PI/2.]) = [.-1,1 .]
   proof
    set sin1 = sin|[.-PI/2,PI/2.];
      now let y be set;
     thus y in [.-1,1 .] implies ex x be set st x in dom sin1 & y = sin1.x
     proof
      assume A1: y in [.-1,1 .];
      then reconsider y1=y as Real;
        sin is_continuous_on [.-PI/2,PI/2 .] by Th43;
      then A2: sin1 is_continuous_on [.-PI/2,PI/2 .] by FCONT_1:16;
        -PI/2 in [.-PI/2,PI/2.] & PI/2 in [.-PI/2,PI/2.] by Th21,TOPREAL5:1;
      then sin1.(PI/2) = sin.(PI/2) & sin1.(-PI/2) = sin.(-PI/2)
                                                               by FUNCT_1:72;
      then y1 in [.sin1.(-PI/2),sin1.(PI/2).] by A1,SIN_COS:33,81;
      then y1 in [.sin1.(-PI/2),sin1.(PI/2).]\/[.sin1.(PI/2),sin1.(-PI/2).]
                                                             by XBOOLE_0:def 2;
      then consider x be Real such that
       A3: x in [.-PI/2,PI/2 .] and
       A4: y1 = sin1.x by A2,Th21,FCONT_2:16;
      take x;
        x in REAL /\ [.-PI/2,PI/2 .] by A3,XBOOLE_0:def 3;
      then x in dom sin /\ [.-PI/2,PI/2 .] by SIN_COS:def 20;
      hence x in dom sin1 & y = sin1.x by A4,FUNCT_1:68;
     end;
     thus (ex x be set st x in dom sin1 & y = sin1.x) implies y in [.-1,1 .]
     proof
      given x be set such that
       A5: x in dom sin1 and
       A6: y = sin1.x;
        dom sin1 c= dom sin by FUNCT_1:76;
      then reconsider x1=x as Real by A5,SIN_COS:def 20;
        y = sin.x1 by A5,A6,FUNCT_1:70;
      hence y in [.-1,1 .] by Th45;
     end;
    end;
    hence thesis by FUNCT_1:def 5;
   end;

  theorem
     rng (sin|[.PI/2,3/2*PI.]) = [.-1,1 .]
   proof
    set sin1 = sin|[.PI/2,3/2*PI.];
      now let y be set;
     thus y in [.-1,1 .] implies ex x be set st x in dom sin1 & y = sin1.x
     proof
      assume A1: y in [.-1,1 .];
      then reconsider y1=y as Real;
        sin is_continuous_on [.PI/2,3/2*PI.] by Th43;
      then A2: sin1 is_continuous_on [.PI/2,3/2*PI.] by FCONT_1:16;
        PI/2 in [.PI/2,3/2*PI.] & 3/2*PI in [.PI/2,3/2*PI.] by Th21,TOPREAL5:1;
      then sin1.(PI/2) = sin.(PI/2) & sin1.(3/2*PI) = sin.(3/2*PI)
                                                               by FUNCT_1:72;
      then y1 in [.sin1.(PI/2),sin1.(3/2*PI).] \/
          [.sin1.(3/2*PI),sin1.(PI/2).] by A1,Th20,SIN_COS:81,XBOOLE_0:def 2;
      then consider x be Real such that
       A3: x in [.PI/2,3/2*PI.] and
       A4: y1 = sin1.x by A2,Th21,FCONT_2:16;
      take x;
        x in REAL /\ [.PI/2,3/2*PI.] by A3,XBOOLE_0:def 3;
      then x in dom sin /\ [.PI/2,3/2*PI.] by SIN_COS:def 20;
      hence x in dom sin1 & y = sin1.x by A4,FUNCT_1:68;
     end;
     thus (ex x be set st x in dom sin1 & y = sin1.x) implies y in [.-1,1 .]
     proof
      given x be set such that
       A5: x in dom sin1 and
       A6: y = sin1.x;
        dom sin1 c= dom sin by FUNCT_1:76;
      then reconsider x1=x as Real by A5,SIN_COS:def 20;
        y = sin.x1 by A5,A6,FUNCT_1:70;
      hence y in [.-1,1 .] by Th45;
     end;
    end;
    hence thesis by FUNCT_1:def 5;
   end;

  theorem Th50:
   rng (cos|[.0,PI.]) = [.-1,1 .]
   proof
    set cos1 = cos|[.0,PI.];
      now let y be set;
     thus y in [.-1,1 .] implies ex x be set st x in dom cos1 & y = cos1.x
     proof
      assume A1: y in [.-1,1 .];
      then reconsider y1=y as Real;
        cos is_continuous_on [.0,PI.] by Th44;
      then A2: cos1 is_continuous_on [.0,PI.] by FCONT_1:16;
        0 in [.0,PI.] & PI in [.0,PI.] by Th21,TOPREAL5:1;
      then cos1.0 = cos.0 & cos1.PI = cos.PI by FUNCT_1:72;
      then y1 in [.cos1.0,cos1.PI.] \/ [.cos1.PI,cos1.0 .]
                                            by A1,SIN_COS:33,81,XBOOLE_0:def 2;
      then consider x be Real such that
       A3: x in [.0,PI.] and
       A4: y1 = cos1.x by A2,Th21,FCONT_2:16;
      take x;
        x in REAL /\ [.0,PI.] by A3,XBOOLE_0:def 3;
      then x in dom cos /\ [.0,PI.] by SIN_COS:def 22;
      hence x in dom cos1 & y = cos1.x by A4,FUNCT_1:68;
     end;
     thus (ex x be set st x in dom cos1 & y = cos1.x) implies y in [.-1,1 .]
     proof
      given x be set such that
       A5: x in dom cos1 and
       A6: y = cos1.x;
        dom cos1 c= dom cos by FUNCT_1:76;
      then reconsider x1=x as Real by A5,SIN_COS:def 22;
        y = cos.x1 by A5,A6,FUNCT_1:70;
      hence y in [.-1,1 .] by Th45;
     end;
    end;
    hence thesis by FUNCT_1:def 5;
   end;

  theorem Th51:
   rng (cos|[.PI,2*PI.]) = [.-1,1 .]
   proof
    set cos1 = cos|[.PI,2*PI.];
      now let y be set;
     thus y in [.-1,1 .] implies ex x be set st x in dom cos1 & y = cos1.x
     proof
      assume A1: y in [.-1,1 .];
      then reconsider y1=y as Real;
        cos is_continuous_on [.PI,2*PI.] by Th44;
      then A2: cos1 is_continuous_on [.PI,2*PI.] by FCONT_1:16;
        PI in [.PI,2*PI.] & 2*PI in [.PI,2*PI.] by Th21,TOPREAL5:1;
      then cos1.PI = cos.PI & cos1.(2*PI) = cos.(2*PI) by FUNCT_1:72;
      then y1 in [.cos1.PI,cos1.(2*PI).] \/ [.cos1.(2*PI),cos1.PI.]
                                               by A1,SIN_COS:81,XBOOLE_0:def 2;
      then consider x be Real such that
       A3: x in [.PI,2*PI.] and
       A4: y1 = cos1.x by A2,Th21,FCONT_2:16;
      take x;
        x in REAL /\ [.PI,2*PI.] by A3,XBOOLE_0:def 3;
      then x in dom cos /\ [.PI,2*PI.] by SIN_COS:def 22;
      hence x in dom cos1 & y = cos1.x by A4,FUNCT_1:68;
     end;
     thus (ex x be set st x in dom cos1 & y = cos1.x) implies y in [.-1,1 .]
     proof
      given x be set such that
       A5: x in dom cos1 and
       A6: y = cos1.x;
        dom cos1 c= dom cos by FUNCT_1:76;
      then reconsider x1=x as Real by A5,SIN_COS:def 22;
        y = cos.x1 by A5,A6,FUNCT_1:70;
      hence y in [.-1,1 .] by Th45;
     end;
    end;
    hence thesis by FUNCT_1:def 5;
   end;

begin  :: Argument of Complex Number

  definition
   let z be Element of F_Complex;
   func Arg z -> Real means :Def1:
    z = [**|.z.|*cos it,|.z.|*sin it**] & 0 <= it & it < 2*PI
     if z <> 0.F_Complex
     otherwise it = 0;
   existence
   proof
    thus z <> 0.F_Complex implies ex r be Real st
     z = [**|.z.|*cos r,|.z.|*sin r**] & 0 <= r & r < 2*PI
    proof
     assume z <> 0.F_Complex;
     then A1: |.z.| <> 0 by COMPLFLD:94;
      A2: |.z.| >= 0 by COMPLFLD:95;
       Re z <= |.z.| by HAHNBAN1:18;
     then A3: Re z/|.z.| <= 1 by A1,A2,REAL_2:117;
     reconsider z1=z as Element of COMPLEX by COMPLFLD:def 1;
       now per cases;
      suppose A4: Im z >= 0;
       set 0PI = [.0,PI.];
       reconsider cos1 = cos|0PI as PartFunc of 0PI,REAL by PARTFUN1:43;
       reconsider cos1 as one-to-one PartFunc of 0PI,REAL by Th41,RFUNCT_2:82;
         now per cases;
        suppose Re z/|.z.| in dom (cos1");
         then cos1".(Re z/|.z.|) in 0PI by PARTFUN1:27;
         hence cos1".(Re z/|.z.|) is real number by XREAL_0:def 1;
        suppose not Re z/|.z.| in dom (cos1");
         hence cos1".(Re z/|.z.|) is real number by FUNCT_1:def 4;
       end;
       then reconsider r = cos1".(Re z/|.z.|) as Real by XREAL_0:def 1;
       take r;
         Re z >= -|.z.| by Th5;
       then -1 <= Re z/|.z.| by A1,A2,REAL_2:117;
       then A5: Re z/|.z.| in rng cos1 by A3,Th50,TOPREAL5:1;
       then Re z/|.z.| in dom (cos1") by FUNCT_1:55;
       then r in rng (cos1") by FUNCT_1:def 5;
       then r in dom cos1 by FUNCT_1:55;
       then A6: r in [.0,PI.] by RELAT_1:86;
       A7: cos r = cos.r by SIN_COS:def 23
          .= cos1.r by A6,FUNCT_1:72
          .= Re z/|.z.| by A5,FUNCT_1:57;
       then A8: Re z = |.z.|*cos r by A1,XCMPLX_1:88;
       A9: |.z.|^2 = (Re z)^2 + (Im z)^2 by Th7;
       A10: |.z.|^2 <> 0 by A1,SQUARE_1:73;
         0 <= r & r <= PI by A6,TOPREAL5:1;
       then (0 = r or 0 < r) & (r = PI or r < PI) by REAL_1:def 5;
       then r = 0 or r = PI or r in ].0,PI.[ by JORDAN6:45;
       then A11: sin.r >= 0 by Th23,SIN_COS:33,81;
         (cos.r)^2 + (sin.r)^2 = 1 by SIN_COS:31;
       then (sin.r)^2 = 1 - (cos.r)^2 by XCMPLX_1:26
          .= 1 - (Re z/|.z.|)^2 by A7,SIN_COS:def 23
          .= 1 - (Re z)^2/|.z.|^2 by SQUARE_1:69
          .= |.z.|^2/|.z.|^2 - (Re z)^2/|.z.|^2 by A10,XCMPLX_1:60
          .= (|.z.|^2 - (Re z)^2)/|.z.|^2 by XCMPLX_1:121
          .= (Im z)^2/|.z.|^2 by A9,XCMPLX_1:26
          .= ((Im z)/|.z.|)^2 by SQUARE_1:69;
       then sin.r = sqrt((Im z)/|.z.|)^2 by A11,SQUARE_1:89
          .= abs((Im z)/|.z.|) by SQUARE_1:91
          .= abs(Im z)/abs |.z.| by ABSVALUE:16
          .= abs(Im z)/|.z.| by HAHNBAN1:12;
       then abs(Im z) = |.z.|*sin.r by A1,XCMPLX_1:88;
       then A12: Im z = |.z.|*sin.r by A4,ABSVALUE:def 1
          .= |.z.|*sin r by SIN_COS:def 21;
         z1 = [*Re z1,Im z1*] by COMPLEX1:8
         .= [*Re z,Im z1*] by HAHNBAN1:def 3
         .= [*Re z,Im z*] by HAHNBAN1:def 4;
       hence z = [**|.z.|*cos r,|.z.|*sin r**] by A8,A12,HAHNBAN1:def 1;
       thus 0 <= r by A6,TOPREAL5:1;
         r <= PI by A6,TOPREAL5:1;
       hence r < 2*PI by Th21,AXIOMS:22;
      suppose A13: Im z < 0;
         now per cases;
        suppose Re z <> |.z.|;
         then A14: Re z/|.z.| <> 1 by XCMPLX_1:58;
         set 0PI = [.PI,2*PI.];
         reconsider cos1 = cos|0PI as PartFunc of 0PI,REAL by PARTFUN1:43;
         reconsider cos1 as one-to-one PartFunc of 0PI,REAL
                                                         by Th42,RFUNCT_2:82;
           now per cases;
          suppose Re z/|.z.| in dom (cos1");
           then cos1".(Re z/|.z.|) in 0PI by PARTFUN1:27;
           hence cos1".(Re z/|.z.|) is real number by XREAL_0:def 1;
          suppose not Re z/|.z.| in dom (cos1");
           hence cos1".(Re z/|.z.|) is real number by CARD_1:51,FUNCT_1:def 4;
         end;
         then reconsider r = cos1".(Re z/|.z.|) as Real by XREAL_0:def 1;
         take r;
           Re z >= -|.z.| by Th5;
         then -1 <= Re z/|.z.| by A1,A2,REAL_2:117;
         then A15: Re z/|.z.| in rng cos1 by A3,Th51,TOPREAL5:1;
         then A16: Re z/|.z.| in dom (cos1") by FUNCT_1:55;
         then r in rng (cos1") by FUNCT_1:def 5;
         then r in dom cos1 by FUNCT_1:55;
         then A17: r in [.PI,2*PI.] by RELAT_1:86;
         A18: cos r = cos.r by SIN_COS:def 23
            .= cos1.r by A17,FUNCT_1:72
            .= Re z/|.z.| by A15,FUNCT_1:57;
         then A19: Re z = |.z.|*cos r by A1,XCMPLX_1:88;
         A20: |.z.|^2 = (Re z)^2 + (Im z)^2 by Th7;
         A21: |.z.|^2 <> 0 by A1,SQUARE_1:73;
           PI <= r & r <= 2*PI by A17,TOPREAL5:1;
         then (PI = r or PI < r) & (r = 2*PI or r < 2*PI) by REAL_1:def 5;
         then r = PI or r = 2*PI or r in ].PI,2*PI.[ by JORDAN6:45;
         then A22: sin.r <= 0 by Th25,SIN_COS:81;
           (cos.r)^2 + (sin.r)^2 = 1 by SIN_COS:31;
         then (sin.r)^2 = 1 - (cos.r)^2 by XCMPLX_1:26
            .= 1 - (Re z/|.z.|)^2 by A18,SIN_COS:def 23
            .= 1 - (Re z)^2/|.z.|^2 by SQUARE_1:69
            .= |.z.|^2/|.z.|^2 - (Re z)^2/|.z.|^2 by A21,XCMPLX_1:60
            .= (|.z.|^2 - (Re z)^2)/|.z.|^2 by XCMPLX_1:121
            .= (Im z)^2/|.z.|^2 by A20,XCMPLX_1:26
            .= ((Im z)/|.z.|)^2 by SQUARE_1:69;
         then -sin.r = sqrt((Im z)/|.z.|)^2 by A22,SQUARE_1:90
            .= abs((Im z)/|.z.|) by SQUARE_1:91
            .= abs(Im z)/abs |.z.| by ABSVALUE:16
            .= abs(Im z)/|.z.| by HAHNBAN1:12;
         then sin.r = -(abs(Im z)/|.z.|);
         then sin.r = (-abs(Im z))/|.z.| by XCMPLX_1:188;
         then -abs(Im z) = |.z.|*sin.r by A1,XCMPLX_1:88;
         then A23: --Im z = |.z.|*sin.r by A13,ABSVALUE:def 1
            .= |.z.|*sin r by SIN_COS:def 21;
           z1 = [*Re z1,Im z1*] by COMPLEX1:8
           .= [*Re z,Im z1*] by HAHNBAN1:def 3
           .= [*Re z,Im z*] by HAHNBAN1:def 4;
         hence z = [**|.z.|*cos r,|.z.|*sin r**] by A19,A23,HAHNBAN1:def 1;
           PI <= r by A17,TOPREAL5:1;
         hence 0 <= r by Th21,AXIOMS:22;
         A24: r <> 2*PI
         proof
          A25: dom cos = REAL by SIN_COS:def 22;
          A26: cos1" is one-to-one by FUNCT_1:62;
            1 in rng cos1 by Th51,TOPREAL5:1;
          then A27: 1 in dom (cos1") by FUNCT_1:55;
          assume A28: r = 2*PI;
          A29: 2*PI in [.PI,2*PI.] by Th21,TOPREAL5:1;
          then A30: 2*PI in dom cos1 by A25,RELAT_1:86;
            cos1.(2*PI) = 1 by A29,FUNCT_1:72,SIN_COS:81;
          then cos1".1 = 2*PI by A30,FUNCT_1:54;
          hence contradiction by A14,A16,A26,A27,A28,FUNCT_1:def 8;
         end;
           r <= 2*PI by A17,TOPREAL5:1;
         hence r < 2*PI by A24,REAL_1:def 5;
        suppose A31: Re z = |.z.|;
         then (Re z)^2 = (Re z)^2 + (Im z)^2 by Th7;
         then (Re z)^2 - (Re z)^2 = (Im z)^2 by XCMPLX_1:26;
         then (Im z)^2 = 0 by XCMPLX_1:14;
         then A32: Im z = 0 by SQUARE_1:73;
         consider z2 be Element of COMPLEX such that
          A33: z = z2 and
          A34: Re z = Re z2 by HAHNBAN1:def 3;
         consider z3 be Element of COMPLEX such that
          A35: z = z3 and
          A36: Im z = Im z3 by HAHNBAN1:def 4;
         A37: z = [*Re z2,Im z3*] by A33,A35,COMPLEX1:8;
         reconsider r=0 as Real;
         take r;
         thus z = [**|.z.|*cos r,|.z.|*sin r**]
                           by A31,A32,A34,A36,A37,HAHNBAN1:def 1,SIN_COS:34;
         thus 0 <= r;
         thus r < 2*PI by Th21;
       end;
       hence thesis;
     end;
     hence thesis;
    end;
    thus thesis;
   end;
   uniqueness
   proof
      z <> 0.F_Complex implies for x,y be Real st
     z = [**|.z.|*cos x,|.z.|*sin x**] & 0 <= x & x < 2*PI &
     z = [**|.z.|*cos y,|.z.|*sin y**] & 0 <= y & y < 2*PI holds x = y
    proof
     assume z <> 0.F_Complex;
     then A38: |.z.| <> 0 by COMPLFLD:94;
     let x,y be Real;
     assume that
      A39: z = [**|.z.|*cos x,|.z.|*sin x**] and
      A40: 0 <= x and
      A41: x < 2*PI and
      A42: z = [**|.z.|*cos y,|.z.|*sin y**] and
      A43: 0 <= y and
      A44: y < 2*PI;
       [*|.z.|*cos x,|.z.|*sin x*] = [**|.z.|*cos y,|.z.|*sin y**]
                                                    by A39,A42,HAHNBAN1:def 1
        .= [*|.z.|*cos y,|.z.|*sin y*] by HAHNBAN1:def 1;
     then |.z.|*cos x = |.z.|*cos y & |.z.|*sin x = |.z.|*sin y by ARYTM_0:12
;
     then cos x = cos y & sin x = sin y by A38,XCMPLX_1:5;
     then A45: cos x = cos y & sin x = sin.y by SIN_COS:def 21;
     then cos x = cos.y & sin.x = sin.y by SIN_COS:def 21,def 23;
     then A46: cos.x = cos.y & sin.x = sin.y by SIN_COS:def 23;
     A47: dom cos = REAL by SIN_COS:def 22;
       now per cases;
      suppose x <= PI & y <= PI;
       then x in [.0,PI.] & y in [.0,PI.] by A40,A43,TOPREAL5:1;
       then A48: x in [.0,PI.] /\ dom cos & y in [.0,PI.] /\ dom cos
                                                   by A47,XBOOLE_0:def 3;
       assume x <> y;
       then x < y or y < x by AXIOMS:21;
       hence contradiction by A46,A48,Th41,RFUNCT_2:def 3;
      suppose x > PI & y > PI;
       then x in [.PI,2*PI.] & y in [.PI,2*PI.] by A41,A44,TOPREAL5:1;
       then A49: x in [.PI,2*PI.] /\ dom cos & y in [.PI,2*PI.] /\ dom cos
                                                          by A47,XBOOLE_0:def 3
;
       assume x <> y;
       then x < y or y < x by AXIOMS:21;
       hence contradiction by A46,A49,Th42,RFUNCT_2:def 2;
      suppose x <= PI & y > PI;
       then x in [.0,PI.] & y in ].PI,2*PI.[ by A40,A44,JORDAN6:45,TOPREAL5:1;
       then sin.x >= 0 & sin.y < 0 by Th24,Th25;
       hence x = y by A45,SIN_COS:def 21;
      suppose y <= PI & x > PI;
       then y in [.0,PI.] & x in ].PI,2*PI.[ by A41,A43,JORDAN6:45,TOPREAL5:1;
       then sin.y >= 0 & sin.x < 0 by Th24,Th25;
       hence x = y by A45,SIN_COS:def 21;
     end;
     hence x = y;
    end;
    hence thesis;
   end;
   consistency;
  end;

  theorem Th52:
   for z be Element of F_Complex holds
    0 <= Arg z & Arg z < 2*PI
   proof
    let z be Element of F_Complex;
      0 <= Arg z & Arg z < 2*PI or z = 0.F_Complex by Def1;
    hence thesis by Def1,Th21;
   end;

  theorem Th53:
   for x be Real st x >= 0 holds
    Arg [**x,0**] = 0
   proof
    let x be Real;
    assume A1: x >= 0;
    A2: 0 <= Arg [**x,0**] & Arg [**x,0**] < 2*PI by Th52;
    per cases by A1;
     suppose A3: x > -0;
      then [*x,0*] <> 0.F_Complex by ARYTM_0:12,L0,COMPLFLD:9;
      then A4: [**x,0**] <> 0.F_Complex by HAHNBAN1:def 1;
      then A5: |. [**x,0**] .| <> 0 by COMPLFLD:94;
        [**x,0**] = [**|. [**x,0**] .|*cos Arg [**x,0**],
                     |. [**x,0**] .|*sin Arg [**x,0**]**] by A4,Def1;
      then A6: |. [**x,0**] .|*cos Arg [**x,0**] = x &
               |. [**x,0**] .|*sin Arg [**x,0**] = 0 by Th8;
      then sin Arg [**x,0**] = 0 by A5,XCMPLX_1:6;
      then Arg [**x,0**] = 0 or |. [**x,0**] .|*-1 = x
                                                    by A2,A6,Th33,SIN_COS:82;
      then Arg [**x,0**] = 0 or -|. [**x,0**] .| = x by XCMPLX_1:180;
      then Arg [**x,0**] = 0 or |. [**x,0**] .| < 0 by A3,REAL_1:50;
      hence Arg [**x,0**] = 0 by COMPLFLD:95;
     suppose x = 0;
      then [**x,0**] = 0.F_Complex by L0,COMPLFLD:9,HAHNBAN1:def 1
;
      hence thesis by Def1;
   end;

  theorem Th54:
   for x be Real st x < 0 holds
    Arg [**x,0**] = PI
   proof
    let x be Real;
    assume A1: x < 0;
    A2: 0 <= Arg [**x,0**] & Arg [**x,0**] < 2*PI by Th52;
      [*x,0*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9;
    then A3: [**x,0**] <> 0.F_Complex by HAHNBAN1:def 1;
    then A4: |. [**x,0**] .| <> 0 by COMPLFLD:94;
      [**x,0**] = [**|. [**x,0**] .|*cos Arg [**x,0**],
                   |. [**x,0**] .|*sin Arg [**x,0**]**] by A3,Def1;
    then A5: |. [**x,0**] .|*cos Arg [**x,0**] = x &
             |. [**x,0**] .|*sin Arg [**x,0**] = 0 by Th8;
    then sin Arg [**x,0**] = 0 by A4,XCMPLX_1:6;
    then Arg [**x,0**] = PI or |. [**x,0**] .|*1 = x by A2,A5,Th33,SIN_COS:34;
    hence thesis by A1,COMPLFLD:95;
   end;

  theorem Th55:
   for x be Real st x > 0 holds
    Arg [**0,x**] = PI/2
   proof
    let x be Real;
    assume A1: x > 0;
    then A2: x > -0;
    A3: 0 <= Arg [**0,x**] & Arg [**0,x**] < 2*PI by Th52;
      [*0,x*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9;
    then A4: [**0,x**] <> 0.F_Complex by HAHNBAN1:def 1;
    then A5: |. [**0,x**] .| <> 0 by COMPLFLD:94;
      [**0,x**] = [**|. [**0,x**] .|*cos Arg [**0,x**],
                   |. [**0,x**] .|*sin Arg [**0,x**]**] by A4,Def1;
    then A6: |. [**0,x**] .|*cos Arg [**0,x**] = 0 &
             |. [**0,x**] .|*sin Arg [**0,x**] = x by Th8;
    then cos Arg [**0,x**] = 0 by A5,XCMPLX_1:6;
    then Arg [**0,x**] = PI/2 or |. [**0,x**] .|*-1 = x
                                               by A3,A6,Th20,Th34,SIN_COS:82;
    then Arg [**0,x**] = PI/2 or -|. [**0,x**] .| = x by XCMPLX_1:180;
    then Arg [**0,x**] = PI/2 or |. [**0,x**] .| < 0 by A2,REAL_1:50;
    hence thesis by COMPLFLD:95;
   end;

  theorem Th56:
   for x be Real st x < 0 holds
    Arg [**0,x**] = 3/2*PI
   proof
    let x be Real;
    assume A1: x < 0;
    A2: 0 <= Arg [**0,x**] & Arg [**0,x**] < 2*PI by Th52;
      [*0,x*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9;
    then A3: [**0,x**] <> 0.F_Complex by HAHNBAN1:def 1;
    then A4: |. [**0,x**] .| <> 0 by COMPLFLD:94;
      [**0,x**] = [**|. [**0,x**] .|*cos Arg [**0,x**],
                   |. [**0,x**] .|*sin Arg [**0,x**]**] by A3,Def1;
    then A5: |. [**0,x**] .|*cos Arg [**0,x**] = 0 &
             |. [**0,x**] .|*sin Arg [**0,x**] = x by Th8;
    then cos Arg [**0,x**] = 0 by A4,XCMPLX_1:6;
    then Arg [**0,x**] = 3/2*PI or |. [**0,x**] .|*1 = x
                                                    by A2,A5,Th34,SIN_COS:82;
    hence thesis by A1,COMPLFLD:95;
   end;

  theorem
     Arg 1_(F_Complex) = 0
   proof
      1_(F_Complex) = [**1,0**] by L1,COMPLFLD:10,HAHNBAN1:def 1;
    hence thesis by Th53;
   end;

  theorem
     Arg i_FC = PI/2 by Th55,HAHNBAN1:6;

  theorem Th59:
   for z be Element of F_Complex holds
    Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0
   proof
    let z be Element of F_Complex;
    thus Arg z in ].0,PI/2.[ implies Re z > 0 & Im z > 0
    proof
     assume A1: Arg z in ].0,PI/2.[;
     then A2: Arg z > 0 & Arg z < PI/2 by JORDAN6:45;
     then A3: z <> 0.F_Complex by Def1;
     then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1;
     then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15;
     A5: |.z.| > 0 by A3,COMPLFLD:96;
       cos Arg z > 0 by A1,SIN_COS:86;
     hence Re z > 0 by A4,A5,SQUARE_1:21;
       Arg z < PI by A2,Th21,AXIOMS:22;
     then Arg z in ].0,PI.[ by A2,JORDAN6:45;
     then sin.Arg z > 0 by Th23;
     then sin Arg z > 0 by SIN_COS:def 21;
     hence Im z > 0 by A4,A5,SQUARE_1:21;
    end;
    assume that
     A6: Re z > 0 and
     A7: Im z > 0;
      z = [**Re z,Im z**] by Th9;
    then A8: z <> 0.F_Complex by A6,Th8,Th10;
    then A9: |.z.| > 0 by COMPLFLD:96;
    A10: 0 <= Arg z & Arg z < 2*PI by Th52;
      z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1;
    then |.z.|*cos Arg z > 0 & |.z.|*sin Arg z > 0 by A6,A7,HAHNBAN1:15;
    then cos Arg z > 0 & sin Arg z > 0 by A9,SQUARE_1:23;
    then A11: cos.Arg z > 0 & sin.Arg z > 0 by SIN_COS:def 21,def 23;
    then not Arg z in [.PI,2*PI.] & not Arg z in [.PI/2,3/2*PI.] by Th26,Th30;
    then A12: PI/2 > Arg z or PI > Arg z & 3/2*PI < Arg z by A10,TOPREAL5:1;
      Arg z > 0 by A10,A11,REAL_1:def 5,SIN_COS:33;
    hence thesis by A12,Th21,AXIOMS:22,JORDAN6:45;
   end;

  theorem Th60:
   for z be Element of F_Complex holds
    Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0
   proof
    let z be Element of F_Complex;
    thus Arg z in ].PI/2,PI.[ implies Re z < 0 & Im z > 0
    proof
     assume A1: Arg z in ].PI/2,PI.[;
     then A2: Arg z > PI/2 & Arg z < PI by JORDAN6:45;
     then A3: z <> 0.F_Complex by Def1,Th21;
     then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1;
     then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15;
     A5: |.z.| > 0 by A3,COMPLFLD:96;
       PI/2 < Arg z & Arg z < PI by A1,JORDAN6:45;
     then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22;
     then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45;
     then cos.Arg z < 0 by Th29;
     then cos Arg z < 0 by SIN_COS:def 23;
     hence Re z < 0 by A4,A5,SQUARE_1:24;
       Arg z > 0 by A2,Th21,AXIOMS:22;
     then Arg z in ].0,PI.[ by A2,JORDAN6:45;
     then sin.Arg z > 0 by Th23;
     then sin Arg z > 0 by SIN_COS:def 21;
     hence Im z > 0 by A4,A5,SQUARE_1:21;
    end;
    assume that
     A6: Re z < 0 and
     A7: Im z > 0;
      z = [**Re z,Im z**] by Th9;
    then A8: z <> 0.F_Complex by A6,Th8,Th10;
    then A9: |.z.| > 0 by COMPLFLD:96;
    A10: 0 <= Arg z & Arg z < 2*PI by Th52;
      z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1;
    then |.z.|*cos Arg z < 0 & |.z.|*sin Arg z > 0 by A6,A7,HAHNBAN1:15;
    then cos Arg z < 0 & sin Arg z > 0 by A9,SQUARE_1:19,23;
    then cos.Arg z < 0 & sin.Arg z > 0 by SIN_COS:def 21,def 23;
    then not Arg z in [.PI,2*PI.] & not Arg z in [.-PI/2,PI/2.] by Th26,Th28;
    then Arg z < PI & (Arg z < -PI/2 or Arg z > PI/2) by A10,TOPREAL5:1;
    hence thesis by A10,Th21,AXIOMS:22,JORDAN6:45;
   end;

  theorem Th61:
   for z be Element of F_Complex holds
    Arg z in ].PI,3/2*PI.[ iff Re z < 0 & Im z < 0
   proof
    let z be Element of F_Complex;
    thus Arg z in ].PI,3/2*PI.[ implies Re z < 0 & Im z < 0
    proof
     assume A1: Arg z in ].PI,3/2*PI.[;
     then A2: Arg z > PI & Arg z < 3/2*PI by JORDAN6:45;
     then A3: z <> 0.F_Complex by Def1,Th21;
     then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1;
     then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15;
     A5: |.z.| > 0 by A3,COMPLFLD:96;
       PI < Arg z & Arg z < 3/2*PI by A1,JORDAN6:45;
     then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22;
     then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45;
     then cos.Arg z < 0 by Th29;
     then cos Arg z < 0 by SIN_COS:def 23;
     hence Re z < 0 by A4,A5,SQUARE_1:24;
       Arg z < 2*PI by A2,Th21,AXIOMS:22;
     then Arg z in ].PI,2*PI.[ by A2,JORDAN6:45;
     then sin.Arg z < 0 by Th25;
     then sin Arg z < 0 by SIN_COS:def 21;
     hence Im z < 0 by A4,A5,SQUARE_1:24;
    end;
    assume that
     A6: Re z < 0 and
     A7: Im z < 0;
      z = [**Re z,Im z**] by Th9;
    then A8: z <> 0.F_Complex by A6,Th8,Th10;
    then A9: |.z.| > 0 by COMPLFLD:96;
    A10: 0 <= Arg z & Arg z < 2*PI by Th52;
      z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1;
    then |.z.|*cos Arg z < 0 & |.z.|*sin Arg z < 0 by A6,A7,HAHNBAN1:15;
    then cos Arg z < 0 & sin Arg z < 0 by A9,SQUARE_1:19;
    then cos.Arg z < 0 & sin.Arg z < 0 by SIN_COS:def 21,def 23;
    then not Arg z in [.0,PI.] & not Arg z in [.-PI/2,PI/2.] &
     not Arg z in [.3/2*PI,2*PI.] by Th24,Th28,Th32;
    then Arg z > PI & (Arg z < -PI/2 or Arg z > PI/2) & Arg z < 3/2*PI
                                                                  by A10,
TOPREAL5:1;
    hence thesis by JORDAN6:45;
   end;

  theorem Th62:
   for z be Element of F_Complex holds
    Arg z in ].3/2*PI,2*PI.[ iff Re z > 0 & Im z < 0
   proof
    let z be Element of F_Complex;
    thus Arg z in ].3/2*PI,2*PI.[ implies Re z > 0 & Im z < 0
    proof
     assume A1: Arg z in ].3/2*PI,2*PI.[;
     then A2: Arg z > 3/2*PI & Arg z < 2*PI by JORDAN6:45;
     then A3: z <> 0.F_Complex by Def1,Th21;
     then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1;
     then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15;
     A5: |.z.| > 0 by A3,COMPLFLD:96;
       cos.Arg z > 0 by A1,Th31;
     then cos Arg z > 0 by SIN_COS:def 23;
     hence Re z > 0 by A4,A5,SQUARE_1:21;
       Arg z > PI by A2,Th21,AXIOMS:22;
     then Arg z in ].PI,2*PI.[ by A2,JORDAN6:45;
     then sin.Arg z < 0 by Th25;
     then sin Arg z < 0 by SIN_COS:def 21;
     hence Im z < 0 by A4,A5,SQUARE_1:24;
    end;
    assume that
     A6: Re z > 0 and
     A7: Im z < 0;
      z = [**Re z,Im z**] by Th9;
    then A8: z <> 0.F_Complex by A6,Th8,Th10;
    then A9: |.z.| > 0 by COMPLFLD:96;
    A10: 0 <= Arg z & Arg z < 2*PI by Th52;
      z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1;
    then |.z.|*cos Arg z > 0 & |.z.|*sin Arg z < 0 by A6,A7,HAHNBAN1:15;
    then cos Arg z > 0 & sin Arg z < 0 by A9,SQUARE_1:19,23;
    then cos.Arg z > 0 & sin.Arg z < 0 by SIN_COS:def 21,def 23;
    then not Arg z in [.0,PI.] & not Arg z in [.PI/2,3/2*PI.] by Th24,Th30;
    then Arg z > PI & (Arg z < PI/2 or Arg z > 3/2*PI) by A10,TOPREAL5:1;
    hence thesis by A10,Th21,AXIOMS:22,JORDAN6:45;
   end;

  theorem Th63:
   for z be Element of F_Complex st Im z > 0 holds
    sin Arg z > 0
   proof
    let z be Element of F_Complex;
    assume A1: Im z > 0;
      Re z < 0 or Re z = 0 or Re z > 0;
    then Re z < 0 or Re z > 0 or z = [**0,Im z**] by Th9;
    then Arg z in ].PI/2,PI.[ or Arg z in ].0,PI/2.[ or Arg z = PI/2
                                                        by A1,Th55,Th59,Th60;
    then PI/2 < Arg z & Arg z < PI or 0 < Arg z & Arg z < PI/2 or
         Arg z = PI/2 by JORDAN6:45;
    then 0 < Arg z & Arg z < PI by Th21,AXIOMS:22;
    then Arg z in ].0,PI.[ by JORDAN6:45;
    then sin.Arg z > 0 by Th23;
    hence thesis by SIN_COS:def 21;
   end;

  theorem Th64:
   for z be Element of F_Complex st Im z < 0 holds
    sin Arg z < 0
   proof
    let z be Element of F_Complex;
    assume A1: Im z < 0;
      Re z < 0 or Re z = 0 or Re z > 0;
    then Re z < 0 or Re z > 0 or z = [**0,Im z**] by Th9;
    then Arg z in ].PI,3/2*PI.[ or Arg z in ].3/2*PI,2*PI.[ or
     Arg z = 3/2*PI by A1,Th56,Th61,Th62;
    then PI < Arg z & Arg z < 3/2*PI or 3/2*PI < Arg z & Arg z < 2*PI or
         Arg z = 3/2*PI by JORDAN6:45;
    then PI < Arg z & Arg z < 2*PI by Th21,AXIOMS:22;
    then Arg z in ].PI,2*PI.[ by JORDAN6:45;
    then sin.Arg z < 0 by Th25;
    hence thesis by SIN_COS:def 21;
   end;

  theorem
     for z be Element of F_Complex st Im z >= 0 holds
    sin Arg z >= 0
   proof
    let z be Element of F_Complex;
    assume Im z >= 0;
    then Im z > 0 or Im z = 0;
    then sin Arg z > 0 or z = [**Re z,0**] & (Re z >= 0 or Re z < 0)
                                                                by Th9,Th63;
    hence thesis by Th53,Th54,SIN_COS:34,82;
   end;

  theorem
     for z be Element of F_Complex st Im z <= 0 holds
    sin Arg z <= 0
   proof
    let z be Element of F_Complex;
    assume Im z <= 0;
    then Im z < 0 or Im z = 0;
    then sin Arg z < 0 or z = [**Re z,0**] & (Re z >= 0 or Re z < 0)
                                                                by Th9,Th64;
    hence thesis by Th53,Th54,SIN_COS:34,82;
   end;

  theorem Th67:
   for z be Element of F_Complex st Re z > 0 holds
    cos Arg z > 0
   proof
    let z be Element of F_Complex;
    assume A1: Re z > 0;
      Im z < 0 or Im z = 0 or Im z > 0;
    then Im z < 0 or Im z > 0 or z = [**Re z,0**] by Th9;
    then Arg z in ].0,PI/2.[ or Arg z in ].3/2*PI,2*PI.[ or Arg z = 0
                                                        by A1,Th53,Th59,Th62;
    then cos.Arg z > 0 by Th31,SIN_COS:33,85;
    hence thesis by SIN_COS:def 23;
   end;

  theorem Th68:
   for z be Element of F_Complex st Re z < 0 holds
    cos Arg z < 0
   proof
    let z be Element of F_Complex;
    assume A1: Re z < 0;
      Im z < 0 or Im z = 0 or Im z > 0;
    then Im z < 0 or Im z > 0 or z = [**Re z,0**] by Th9;
    then Arg z in ].PI/2,PI.[ or Arg z in ].PI,3/2*PI.[ or Arg z = PI
                                                        by A1,Th54,Th60,Th61;
    then PI/2 < Arg z & Arg z < PI or PI < Arg z & Arg z < 3/2*PI or
         Arg z = PI by JORDAN6:45;
    then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22;
    then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45;
    then cos.Arg z < 0 by Th29;
    hence thesis by SIN_COS:def 23;
   end;

  theorem
     for z be Element of F_Complex st Re z >= 0 holds
    cos Arg z >= 0
   proof
    let z be Element of F_Complex;
    assume Re z >= 0;
    then Re z > 0 or Re z = 0;
    then cos Arg z > 0 or z = [**0,Im z**] & (Im z > 0 or Im z < 0 or Im z = 0
)
                                                  by Th9,Th67;
    then cos Arg z > 0 or Arg z = PI/2 or Arg z = 3/2*PI or Arg z = 0
                                                    by Def1,Th10,Th55,Th56;
    hence thesis by Th20,SIN_COS:34,82;
   end;

  theorem
     for z be Element of F_Complex st Re z <= 0 &
    z <> 0.F_Complex holds
    cos Arg z <= 0
   proof
    let z be Element of F_Complex;
    assume that
     A1: Re z <= 0 and
     A2: z <> 0.F_Complex;
      Re z < 0 or Re z = 0 by A1;
    then cos Arg z < 0 or z = [**0,Im z**] & (Im z >= 0 or Im z < 0)
                                                                by Th9,Th68;
    then cos Arg z < 0 or z = [**0,Im z**] & (Im z > 0 or Im z < 0)
                                                    by A2,Th10,REAL_1:def 5;
    hence thesis by Th20,Th55,Th56,SIN_COS:82;
   end;

  theorem Th71:
   for n be Nat holds
    (power F_Complex).([**cos x,sin x**],n) = [**cos (n*x),sin (n*x)**]
   proof
     defpred P[Nat] means
     (power F_Complex).([**cos x,sin x**],$1) = [**cos ($1*x),sin ($1*x)**];
    (power F_Complex).([**cos x,sin x**],0) = 1.F_Complex by GROUP_1:def 7
       .= [*1,0*] by L1,COMPLFLD:10,POLYNOM2:3
       .= [**cos (0*x),sin (0*x)**] by HAHNBAN1:def 1,SIN_COS:34;
    then A1: P[0];
    A2: now let n be Nat;
     assume P[n];
     then (power F_Complex).([**cos x,sin x**],n+1) =
           [**cos(n*x),sin(n*x)**]*[**cos x,sin x**] by GROUP_1:def 7
        .= [**cos(n*x)*cos x - sin(n*x)*sin x,cos(n*x)*sin x+cos x*sin(n*x)**]
                                                               by HAHNBAN1:11
        .= [**cos(n*x+x),cos(n*x)*sin x+cos x*sin(n*x)**] by SIN_COS:80
        .= [**cos(n*x+1*x),sin(n*x+1*x)**] by SIN_COS:80
        .= [**cos((n+1)*x),sin(n*x+1*x)**] by XCMPLX_1:8
        .= [**cos((n+1)*x),sin((n+1)*x)**] by XCMPLX_1:8;
      hence P[n+1];
    end;
    thus for n be Nat holds P[n] from Ind(A1,A2);
   end;

  theorem
     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)**]
   proof
    let z be Element of F_Complex;
    let n be Nat;
    assume A1: z <> 0.F_Complex or n <> 0;
    per cases by A1,NAT_1:18;
     suppose A2: z <> 0.F_Complex;
      then A3: |.z.| > 0 by COMPLFLD:96;
      thus (power F_Complex).(z,n) =
            (power F_Complex).([**|.z.|*cos Arg z-0*sin Arg z,
                               |.z.|*sin Arg z+cos Arg z*0**],n) by A2,Def1
         .= (power F_Complex).([**|.z.|,0**]*[**cos Arg z,sin Arg z**],n)
                                                               by HAHNBAN1:11
         .= (power F_Complex).([**|.z.|,0**],n)*
            (power F_Complex).([**cos Arg z,sin Arg z**],n) by Th15
         .= (power F_Complex).([**|.z.|,0**],n)*
            [**cos (n*Arg z),sin (n*Arg z)**] by Th71
         .= [**|.z.| to_power n,0**]*[**cos (n*Arg z),sin (n*Arg z)**]
                                                                   by A3,Th16
         .= [**(|.z.| to_power n)*cos(n*Arg z)-0*sin (n*Arg z),
             (|.z.| to_power n)*sin(n*Arg z)+0*cos(n*Arg z)**] by HAHNBAN1:11
         .= [**(|.z.| to_power n)*cos(n*Arg z),
               (|.z.| to_power n)*sin(n*Arg z)**];
     suppose A4: z = 0.F_Complex & n > 0;
      hence (power F_Complex).(z,n) = [**0*cos(n*Arg z),0*sin(n*Arg z)**]
                                                              by Th10,Th14
      .= [**0*cos(n*Arg z),(|.z.| to_power n)*sin(n*Arg z)**]
                                        by A4,Lm1,COMPLFLD:93,POWER:def 2
      .= [**(|.z.| to_power n)*cos(n*Arg z),(|.z.| to_power n)*sin(n*Arg z)**]
                                        by A4,Lm1,COMPLFLD:93,POWER:def 2;
   end;

  theorem Th73:
   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**]
   proof
    let n,k be Nat;
    assume A1: n <> 0;
    thus (power F_Complex).([**cos((x+2*PI*k)/n),sin((x+2*PI*k)/n)**],n) =
          [**cos(n*((x+2*PI*k)/n)),sin(n*((x+2*PI*k)/n))**] by Th71
       .= [**cos(x+2*PI*k),sin(n*((x+2*PI*k)/n))**] by A1,XCMPLX_1:88
       .= [**cos(x+2*PI*k),sin(x+2*PI*k)**] by A1,XCMPLX_1:88
       .= [**cos.(x+2*PI*k),sin(x+2*PI*k)**] by SIN_COS:def 23
       .= [**cos.(x+2*PI*k),sin.(x+2*PI*k)**] by SIN_COS:def 21
       .= [**cos.(x+2*PI*k),sin.x**] by SIN_COS2:10
       .= [**cos.x,sin.x**] by SIN_COS2:11
       .= [**cos.x,sin x**] by SIN_COS:def 21
       .= [**cos x,sin x**] by SIN_COS:def 23;
   end;

  theorem Th74:
   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)
   proof
    let z be Element of F_Complex;
    let n,k be Nat;
    assume A1: n <> 0;
    then A2: n > 0 by NAT_1:19;
    then A3: n >= 0+1 by NAT_1:38;
    per cases;
     suppose A4: z <> 0.F_Complex;
      then A5: |.z.| > 0 by COMPLFLD:96;
      then n-root |.z.| = n -Root |.z.| by A3,POWER:def 1;
      then A6: n-root |.z.| > 0 by A3,A5,PREPOWER:def 3;
      thus (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n),
                               (n-root |.z.|)*sin((Arg z+2*PI*k)/n)**],n) =
          (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n)-
          0*sin((Arg z+2*PI*k)/n),(n-root |.z.|)*sin((Arg z+2*PI*k)/n)+
          0*cos((Arg z+2*PI*k)/n)**],n)
       .= (power F_Complex).([**n-root |.z.|,0**]*
          [**cos((Arg z+2*PI*k)/n),sin((Arg z+2*PI*k)/n)**],n) by HAHNBAN1:11
       .= (power F_Complex).([**n-root |.z.|,0**],n)*(power F_Complex).
          ([**cos((Arg z+2*PI*k)/n),sin((Arg z+2*PI*k)/n)**],n) by Th15
       .= (power F_Complex).([**n-root |.z.|,0**],n)*[**cos Arg z,sin Arg z**]
                                                                   by A1,Th73
       .= [**(n-root |.z.|) to_power n,0**]*[**cos Arg z,sin Arg z**]
         by A6,Th16

       .= [**|.z.|,0**]*[**cos Arg z,sin Arg z**] by A1,A5,Th17
       .= [**|.z.|*cos Arg z-0*sin Arg z,|.z.|*sin Arg z+0*cos Arg z**]
                                                               by HAHNBAN1:11
       .= z by A4,Def1;
     suppose A7: z = 0.F_Complex;
      then |.z.| = 0 by COMPLFLD:9,93,def 1;
      hence (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n),
                               (n-root |.z.|)*sin((Arg z+2*PI*k)/n)**],n) =
          (power F_Complex).([**0*cos((Arg z+2*PI*k)/n),
                      (n-root 0)*sin((Arg z+2*PI*k)/n)**],n) by A3,POWER:6
       .= (power F_Complex).([**0,0*sin((Arg z+2*PI*k)/n)**],n) by A3,POWER:6
       .= z by A2,A7,Th10,Th14;
   end;

  definition
   let x be Element of F_Complex;
   let n be non empty Nat;
   mode CRoot of n,x -> Element of F_Complex means :Def2:
    (power F_Complex).(it,n) = x;
   existence
   proof
    take [**(n-root |.x.|)*cos((Arg x+2*PI*0)/n),
                (n-root |.x.|)*sin((Arg x+2*PI*0)/n)**];
    thus thesis by Th74;
   end;
  end;

  theorem
     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
   proof
    let x be Element of F_Complex;
    let n be non empty Nat;
    let k be Nat;
      (power F_Complex).([**(n-root |.x.|)*cos((Arg x+2*PI*k)/n),
     (n-root |.x.|)*sin((Arg x+2*PI*k)/n)**],n) = x by Th74;
    hence thesis by Def2;
   end;

  theorem
     for x be Element of F_Complex
   for v be CRoot of 1,x holds
    v = x
   proof
    let x be Element of F_Complex;
    let v be CRoot of 1,x;
      (power F_Complex).(v,1) = x by Def2;
    hence v = x by Th12;
   end;

  theorem
     for n be non empty Nat
   for v be CRoot of n,0.F_Complex holds
    v = 0.F_Complex
   proof
    let n be non empty Nat;
    let v be CRoot of n,0.F_Complex;
    defpred P[Nat] means (power F_Complex).(v,$1) = 0.F_Complex;
    A1: ex n be non empty Nat st P[n]
    proof
     take n;
     thus thesis by Def2;
    end;
    A2: now let k be non empty Nat;
     assume that
      A3: k <> 1 and
      A4: P[k];
     consider t be Nat such that
      A5: k = t+1 by NAT_1:22;
       k >= 1 by RLVECT_1:99;
     then t+1 > 0+1 by A3,A5,REAL_1:def 5;
     then A6: t > 0 by AXIOMS:24;
     reconsider t as non empty Nat by A3,A5,CARD_1:51;
     take t;
     thus t < k by A5,NAT_1:38;
       (power F_Complex).(v,k) = (power F_Complex).(v,t)*v by A5,GROUP_1:def 7;
     then (power F_Complex).(v,t) = 0.F_Complex or v = 0.F_Complex
                                                           by A4,VECTSP_1:44;
     hence P[t] by A6,Th14;
    end;
    P[1] from Regr_without_0(A1,A2);
    hence thesis by Th12;
   end;

  theorem
     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
   proof
    let n be non empty Nat;
    let x be Element of F_Complex;
    let v be CRoot of n,x;
     A1: n >= 0 & n <> 0 by NAT_1:18;
    assume v = 0.F_Complex;
    then (power F_Complex).(0.F_Complex,n) = x by Def2;
    hence thesis by A1,Th14;
   end;


Back to top